[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] N →ₗ[R] P
src✝ : M ⊗[R] N →ₗ[R] P := TensorProduct.lift (↑R f)
c : A
x : M
y : N
⊢ ↑(comp (TensorProduct.lift (↑R f)) (↑(Algebra.lsmul R R (M ⊗[R] N)) c)) (x ⊗ₜ[R] y) =
    ↑(comp (↑(Algebra.lsmul R R P) c) (TensorProduct.lift (↑R f))) (x ⊗ₜ[R] y)
[PROOFSTEP]
simp only [comp_apply, Algebra.lsmul_coe, smul_tmul', lift.tmul, coe_restrictScalars, f.map_smul, smul_apply]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝¹ x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ ↑(lift (x✝¹ + x✝)) (x ⊗ₜ[R] y) = ↑(lift x✝¹ + lift x✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
simp only [lift_tmul, add_apply]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝¹ : B
x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ ↑(AddHom.toFun { toFun := lift, map_add' := (_ : ∀ (x x_1 : M →ₗ[A] N →ₗ[R] P), lift (x + x_1) = lift x + lift x_1) }
          (x✝¹ • x✝))
      (x ⊗ₜ[R] y) =
    ↑(↑(RingHom.id B) x✝¹ •
          AddHom.toFun
            { toFun := lift, map_add' := (_ : ∀ (x x_1 : M →ₗ[A] N →ₗ[R] P), lift (x + x_1) = lift x + lift x_1) } x✝)
      (x ⊗ₜ[R] y)
[PROOFSTEP]
simp only [lift_tmul, smul_apply, RingHom.id_apply]
  -- porting note: new `B` argument
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map (f₁ + f₂) g)) x✝¹) x✝ = ↑(↑(curry (map f₁ g + map f₂ g)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, add_tmul]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map f (g₁ + g₂))) x✝¹) x✝ = ↑(↑(curry (map f g₁ + map f g₂)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, tmul_add]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map f (r • g) = r • map f g
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map f (r • g))) x✝¹) x✝ = ↑(↑(curry (r • map f g)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, smul_apply, tmul_smul]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (b • f) g = b • map f g
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map (b • f) g)) x✝¹) x✝ = ↑(↑(curry (b • map f g)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, smul_apply, smul_tmul']
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ comp (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q)))))
      (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q)))) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case a.h.a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ↑(↑(curry
              (↑(curry
                    (comp (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q)))))
                      (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q))))))
                x✝²))
          x✝¹)
      x✝ =
    ↑(↑(curry (↑(curry LinearMap.id) x✝²)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ comp (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q))))
      (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q))))) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case a.a.h.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ↑(↑(↑(curry
                  (curry
                    (comp (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q))))
                      (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q))))))))
              x✝²)
          x✝¹)
      x✝ =
    ↑(↑(↑(curry (curry LinearMap.id)) x✝²) x✝¹) x✝
[PROOFSTEP]
rfl
