awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid P
inst_15 : Module A P
inst_16 : AddCommMonoid P'
inst_17 : Module A P'
inst_18 : AddCommMonoid Q
inst_19 : Module R Q
inst_20 : CommSemiring S
inst_21 : Module S M
inst_22 : Module S P
inst_23 : Algebra S B
inst_24 : IsScalarTower S B M
inst_25 : SMulCommClass R S M
inst_26 : SMulCommClass S R M
x : M
x_1 : P
x_2 : Q
⊢ Eq (α := M ⊗[S] P ⊗[R] Q)
    (((((((curry
                          (curry
                            ((lift
                                  (lift
                                    ((↑lflip :
                                          (P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q) ∘ₗ
                                        compr₂ (mk S B M P) (mk R B (M ⊗[S] P) Q) :
                                      M →ₗ[B] Q →ₗ[R] P →ₗ[S] M ⊗[S] P ⊗[R] Q)) :
                                M ⊗[R] Q ⊗[S] P →ₗ[B] M ⊗[S] P ⊗[R] Q) ∘ₗ
                              (lift
                                  (lift
                                    ((↑lflip :
                                          (Q →ₗ[R] P →ₗ[S] M ⊗[R] Q ⊗[S] P) →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P) ∘ₗ
                                        compr₂ (mk R B M Q) (mk S B (M ⊗[R] Q) P) :
                                      M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[R] Q ⊗[S] P)) :
                                M ⊗[S] P ⊗[R] Q →ₗ[B] M ⊗[R] Q ⊗[S] P))) :
                        M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                      (a : M) → P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
                    x :
                  P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                (a : P) → Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
              x_1 :
            Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
          (a : Q) → M ⊗[S] P ⊗[R] Q)
        x_2 :
      M ⊗[S] P ⊗[R] Q)
    (((((((curry (curry LinearMap.id) : M →ₗ[B] P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                      (a : M) → P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
                    x :
                  P →ₗ[S] Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
                (a : P) → Q →ₗ[R] M ⊗[S] P ⊗[R] Q)
              x_1 :
            Q →ₗ[R] M ⊗[S] P ⊗[R] Q) :
          (a : Q) → M ⊗[S] P ⊗[R] Q)
        x_2 :
      M ⊗[S] P ⊗[R] Q)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
B : Type uB
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module B M
inst_6 : IsScalarTower R B M
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
inst_10 : CommSemiring S
inst_11 : Module S M
inst_12 : Module S P
inst_13 : Algebra S B
inst_14 : IsScalarTower S B M
inst_15 : SMulCommClass R S M
inst_16 : SMulCommClass S R M
m : M
p : P
q : Q
⊢ Eq (α := M ⊗[R] Q ⊗[S] P)
    (((rightComm R S B M P Q : M ⊗[S] P ⊗[R] Q ≃ₗ[B] M ⊗[R] Q ⊗[S] P) : (a : M ⊗[S] P ⊗[R] Q) → M ⊗[R] Q ⊗[S] P)
        (m ⊗ₜ[S] p ⊗ₜ[R] q) :
      M ⊗[R] Q ⊗[S] P)
    (m ⊗ₜ[R] q ⊗ₜ[S] p : M ⊗[R] Q ⊗[S] P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
B : Type uB
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module B M
inst_6 : IsScalarTower R B M
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
inst_10 : CommSemiring S
inst_11 : Module S M
inst_12 : Module S P
inst_13 : Algebra S B
inst_14 : IsScalarTower S B M
inst_15 : SMulCommClass R S M
inst_16 : SMulCommClass S R M
⊢ Eq (α := M ⊗[R] Q ⊗[S] P ≃ₗ[B] M ⊗[S] P ⊗[R] Q)
    (LinearEquiv.symm (rightComm R S B M P Q) : M ⊗[R] Q ⊗[S] P ≃ₗ[B] M ⊗[S] P ⊗[R] Q)
    (rightComm S R B M Q P : M ⊗[R] Q ⊗[S] P ≃ₗ[B] M ⊗[S] P ⊗[R] Q)

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.AlgebraTensorModule.rightComm, TensorProduct, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
B : Type uB
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module B M
inst_6 : IsScalarTower R B M
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : Module R Q
inst_10 : CommSemiring S
inst_11 : Module S M
inst_12 : Module S P
inst_13 : Algebra S B
inst_14 : IsScalarTower S B M
inst_15 : SMulCommClass R S M
inst_16 : SMulCommClass S R M
m : M
p : P
q : Q
⊢ Eq (α := M ⊗[S] P ⊗[R] Q)
    (((LinearEquiv.symm (rightComm R S B M P Q) : M ⊗[R] Q ⊗[S] P ≃ₗ[B] M ⊗[S] P ⊗[R] Q) :
          (a : M ⊗[R] Q ⊗[S] P) → M ⊗[S] P ⊗[R] Q)
        (m ⊗ₜ[R] q ⊗ₜ[S] p) :
      M ⊗[S] P ⊗[R] Q)
    (m ⊗ₜ[S] p ⊗ₜ[R] q : M ⊗[S] P ⊗[R] Q)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
M : Type uM
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R Q
inst_6 : Module R P
⊢ Eq (α := M ⊗[R] P ⊗[R] Q ≃ₗ[R] M ⊗[R] Q ⊗[R] P) (rightComm R R R M P Q : M ⊗[R] P ⊗[R] Q ≃ₗ[R] M ⊗[R] Q ⊗[R] P)
    (TensorProduct.rightComm R M P Q : M ⊗[R] P ⊗[R] Q ≃ₗ[R] M ⊗[R] Q ⊗[R] P)

Tactic:
rfl

Premises used: TensorProduct.rightComm, TensorProduct.AlgebraTensorModule.rightComm, TensorProduct.lift, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid P
inst_15 : Module A P
inst_16 : AddCommMonoid Q
inst_17 : Module R Q
inst_18 : Module R P
inst_19 : IsScalarTower R A P
inst_20 : Algebra A B
inst_21 : IsScalarTower A B M
inst_22 : CommSemiring S
inst_23 : Algebra R S
inst_24 : Algebra S B
inst_25 : Module S M
inst_26 : Module S N
inst_27 : IsScalarTower R S M
inst_28 : SMulCommClass A S M
inst_29 : SMulCommClass S A M
inst_30 : IsScalarTower S B M
inst_31 : IsScalarTower R S N
m : M
n : N
p : P
q : Q
⊢ Eq (α := M ⊗[A] P ⊗[S] (N ⊗[R] Q))
    (((tensorTensorTensorComm R S A B M N P Q : M ⊗[S] N ⊗[A] (P ⊗[R] Q) ≃ₗ[B] M ⊗[A] P ⊗[S] (N ⊗[R] Q)) :
          (a : M ⊗[S] N ⊗[A] (P ⊗[R] Q)) → M ⊗[A] P ⊗[S] (N ⊗[R] Q))
        (m ⊗ₜ[S] n ⊗ₜ[A] (p ⊗ₜ[R] q)) :
      M ⊗[A] P ⊗[S] (N ⊗[R] Q))
    (m ⊗ₜ[A] p ⊗ₜ[S] (n ⊗ₜ[R] q) : M ⊗[A] P ⊗[S] (N ⊗[R] Q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid P
inst_15 : Module A P
inst_16 : AddCommMonoid Q
inst_17 : Module R Q
inst_18 : Module R P
inst_19 : IsScalarTower R A P
inst_20 : Algebra A B
inst_21 : IsScalarTower A B M
inst_22 : CommSemiring S
inst_23 : Algebra R S
inst_24 : Algebra S B
inst_25 : Module S M
inst_26 : Module S N
inst_27 : IsScalarTower R S M
inst_28 : SMulCommClass A S M
inst_29 : SMulCommClass S A M
inst_30 : IsScalarTower S B M
inst_31 : IsScalarTower R S N
⊢ Eq (α := M ⊗[A] P ⊗[S] (N ⊗[R] Q) ≃ₗ[B] M ⊗[S] N ⊗[A] (P ⊗[R] Q))
    (LinearEquiv.symm (tensorTensorTensorComm R S A B M N P Q) :
      M ⊗[A] P ⊗[S] (N ⊗[R] Q) ≃ₗ[B] M ⊗[S] N ⊗[A] (P ⊗[R] Q))
    (tensorTensorTensorComm R A S B M P N Q : M ⊗[A] P ⊗[S] (N ⊗[R] Q) ≃ₗ[B] M ⊗[S] N ⊗[A] (P ⊗[R] Q))

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
inst_12 : AddCommMonoid N
inst_13 : Module R N
inst_14 : AddCommMonoid P
inst_15 : Module A P
inst_16 : AddCommMonoid Q
inst_17 : Module R Q
inst_18 : Module R P
inst_19 : IsScalarTower R A P
inst_20 : Algebra A B
inst_21 : IsScalarTower A B M
inst_22 : CommSemiring S
inst_23 : Algebra R S
inst_24 : Algebra S B
inst_25 : Module S M
inst_26 : Module S N
inst_27 : IsScalarTower R S M
inst_28 : SMulCommClass A S M
inst_29 : SMulCommClass S A M
inst_30 : IsScalarTower S B M
inst_31 : IsScalarTower R S N
m : M
n : N
p : P
q : Q
⊢ Eq (α := M ⊗[S] N ⊗[A] (P ⊗[R] Q))
    (((LinearEquiv.symm (tensorTensorTensorComm R S A B M N P Q) :
            M ⊗[A] P ⊗[S] (N ⊗[R] Q) ≃ₗ[B] M ⊗[S] N ⊗[A] (P ⊗[R] Q)) :
          (a : M ⊗[A] P ⊗[S] (N ⊗[R] Q)) → M ⊗[S] N ⊗[A] (P ⊗[R] Q))
        (m ⊗ₜ[A] p ⊗ₜ[S] (n ⊗ₜ[R] q)) :
      M ⊗[S] N ⊗[A] (P ⊗[R] Q))
    (m ⊗ₜ[S] n ⊗ₜ[A] (p ⊗ₜ[R] q) : M ⊗[S] N ⊗[A] (P ⊗[R] Q))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : Module R Q
inst_8 : Module R P
⊢ Eq (α := M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] P ⊗[R] (N ⊗[R] Q))
    (tensorTensorTensorComm R R R R M N P Q : M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] P ⊗[R] (N ⊗[R] Q))
    (TensorProduct.tensorTensorTensorComm R M N P Q : M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] P ⊗[R] (N ⊗[R] Q))

Tactic:
rfl

Premises used: TensorProduct.AlgebraTensorModule.tensorTensorTensorComm, TensorProduct.congr, TensorProduct.map, TensorProduct.AlgebraTensorModule.congr, TensorProduct.tensorTensorTensorComm, TensorProduct.assoc, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.assoc, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
m : ULift.{u_1, uM} M
n : ULift.{u_2, uN} N
⊢ Eq (α := M ⊗[R] N)
    (ULift.down
      (((LinearEquiv.symm (uliftEquiv R A M N) :
            ULift.{u_1, uM} M ⊗[ULift.{u_4, uR} R] ULift.{u_2, uN} N ≃ₗ[A] ULift.{u_3, max uN uM} (M ⊗[R] N)) :
          (a : ULift.{u_1, uM} M ⊗[ULift.{u_4, uR} R] ULift.{u_2, uN} N) → ULift.{u_3, max uN uM} (M ⊗[R] N))
        (m ⊗ₜ[ULift.{u_4, uR} R] n)))
    (m.down ⊗ₜ[R] n.down)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : AddCommMonoid N
inst_8 : Module R N
m : M
n : N
⊢ Eq (α := ULift.{u_2, uM} M ⊗[ULift.{u_3, uR} R] ULift.{u_1, uN} N)
    (((uliftEquiv R A M N :
            ULift.{u_4, max uN uM} (M ⊗[R] N) ≃ₗ[A] ULift.{u_2, uM} M ⊗[ULift.{u_3, uR} R] ULift.{u_1, uN} N) :
          (a : ULift.{u_4, max uN uM} (M ⊗[R] N)) → ULift.{u_2, uM} M ⊗[ULift.{u_3, uR} R] ULift.{u_1, uN} N)
        { down := m ⊗ₜ[R] n } :
      ULift.{u_2, uM} M ⊗[ULift.{u_3, uR} R] ULift.{u_1, uN} N)
    ({ down := m } ⊗ₜ[ULift.{u_3, uR} R] { down := n } : ULift.{u_2, uM} M ⊗[ULift.{u_3, uR} R] ULift.{u_1, uN} N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
f : M →ₗ[R] N
a : A
x : M
⊢ Eq (α := A ⊗[R] N) ((baseChange A f : (a : A ⊗[R] M) → A ⊗[R] N) (a ⊗ₜ[R] x) : A ⊗[R] N)
    (a ⊗ₜ[R] (f : (a : M) → N) x : A ⊗[R] N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
f : M →ₗ[R] N
⊢ Eq (α := (a : A ⊗[R] M) → A ⊗[R] N) (⇑(baseChange A f) : (a : A ⊗[R] M) → A ⊗[R] N)
    (⇑(lTensor A f) : (a : A ⊗[R] M) → A ⊗[R] N)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
f g : M →ₗ[R] N
a :
  ∀ (x : M),
    Eq (α := A ⊗[R] N)
      ((((AlgebraTensorModule.curry (baseChange A (f + g)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
            (a : M) → A ⊗[R] N)
          x :
        A ⊗[R] N)
      ((((AlgebraTensorModule.curry (HAdd.hAdd (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)) :
                  A →ₗ[A] M →ₗ[R] A ⊗[R] N) :
                (a : A) → M →ₗ[R] A ⊗[R] N)
              1 :
            (a : M) → A ⊗[R] N)
          x :
        A ⊗[R] N)
⊢ baseChange A (f + g) = HAdd.hAdd (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
f g : M →ₗ[R] N
x : M
⊢ Eq (α := A ⊗[R] N)
    ((((AlgebraTensorModule.curry (baseChange A (f + g)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
    ((((AlgebraTensorModule.curry (HAdd.hAdd (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] N) :
              (a : A) → M →ₗ[R] A ⊗[R] N)
            1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)

Tactic:
simp [baseChange_eq_ltensor, -baseChange_tmul]

Premises used: LinearMap.baseChange_eq_ltensor, LinearMap.baseChange_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
a :
  ∀ (x : M),
    Eq (α := A ⊗[R] N)
      ((((AlgebraTensorModule.curry (baseChange A 0) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
            (a : M) → A ⊗[R] N)
          x :
        A ⊗[R] N)
      ((((AlgebraTensorModule.curry 0 : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 : (a : M) → A ⊗[R] N)
          x :
        A ⊗[R] N)
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
x : M
⊢ Eq (α := A ⊗[R] N)
    ((((AlgebraTensorModule.curry (baseChange A 0) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
    ((((AlgebraTensorModule.curry 0 : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 : (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
r : R
f : M →ₗ[R] N
a :
  ∀ (x : M),
    Eq (α := A ⊗[R] N)
      ((((AlgebraTensorModule.curry (baseChange A (r • f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
            (a : M) → A ⊗[R] N)
          x :
        A ⊗[R] N)
      ((((AlgebraTensorModule.curry (HSMul.hSMul (β := A ⊗[R] M →ₗ[A] A ⊗[R] N) r (baseChange A f)) :
                  A →ₗ[A] M →ₗ[R] A ⊗[R] N) :
                (a : A) → M →ₗ[R] A ⊗[R] N)
              1 :
            (a : M) → A ⊗[R] N)
          x :
        A ⊗[R] N)
⊢ baseChange A (r • f) = HSMul.hSMul (β := A ⊗[R] M →ₗ[A] A ⊗[R] N) r (baseChange A f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
r : R
f : M →ₗ[R] N
x : M
⊢ Eq (α := A ⊗[R] N)
    ((((AlgebraTensorModule.curry (baseChange A (r • f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
    ((((AlgebraTensorModule.curry (HSMul.hSMul (β := A ⊗[R] M →ₗ[A] A ⊗[R] N) r (baseChange A f)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] N) :
              (a : A) → M →ₗ[R] A ⊗[R] N)
            1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
a :
  ∀ (x : M),
    Eq (α := A ⊗[R] M)
      ((((AlgebraTensorModule.curry (baseChange A id) : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 :
            (a : M) → A ⊗[R] M)
          x :
        A ⊗[R] M)
      ((((AlgebraTensorModule.curry id : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M)
          x :
        A ⊗[R] M)
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A id) id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
x : M
⊢ Eq (α := A ⊗[R] M)
    ((((AlgebraTensorModule.curry (baseChange A id) : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 :
          (a : M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((((AlgebraTensorModule.curry id : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M)
        x :
      A ⊗[R] M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
a :
  ∀ (x : M),
    Eq (α := A ⊗[R] P)
      ((((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] P) : (a : A) → M →ₗ[R] A ⊗[R] P)
              1 :
            (a : M) → A ⊗[R] P)
          x :
        A ⊗[R] P)
      ((((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f) : A →ₗ[A] M →ₗ[R] A ⊗[R] P) :
                (a : A) → M →ₗ[R] A ⊗[R] P)
              1 :
            (a : M) → A ⊗[R] P)
          x :
        A ⊗[R] P)
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] P) (baseChange A (g ∘ₗ f)) (baseChange A g ∘ₗ baseChange A f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x : M
⊢ Eq (α := A ⊗[R] P)
    ((((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] P) : (a : A) → M →ₗ[R] A ⊗[R] P) 1 :
          (a : M) → A ⊗[R] P)
        x :
      A ⊗[R] P)
    ((((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f) : A →ₗ[A] M →ₗ[R] A ⊗[R] P) :
              (a : A) → M →ₗ[R] A ⊗[R] P)
            1 :
          (a : M) → A ⊗[R] P)
        x :
      A ⊗[R] P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
A : Type u_7
B : Type u_8
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
f : M →ₗ[R] N
a :
  ∀ (x : M),
    Eq (α := B ⊗[A] (A ⊗[R] N))
      ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (baseChange B (baseChange A f)) :
                          B →ₗ[B] A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N)) :
                        (a : B) → A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N))
                      1) :
                  A →ₗ[A] M →ₗ[R] B ⊗[A] (A ⊗[R] N)) :
                (a : A) → M →ₗ[R] B ⊗[A] (A ⊗[R] N))
              1 :
            (a : M) → B ⊗[A] (A ⊗[R] N))
          x :
        B ⊗[A] (A ⊗[R] N))
      ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            (((↑(LinearEquiv.symm (cancelBaseChange R A B B N)) : B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) :
                                B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) ∘ₗ
                              (baseChange B f ∘ₗ (↑(cancelBaseChange R A B B M) : B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] M) :
                                B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] N)) :
                          B →ₗ[B] A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N)) :
                        (a : B) → A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N))
                      1) :
                  A →ₗ[A] M →ₗ[R] B ⊗[A] (A ⊗[R] N)) :
                (a : A) → M →ₗ[R] B ⊗[A] (A ⊗[R] N))
              1 :
            (a : M) → B ⊗[A] (A ⊗[R] N))
          x :
        B ⊗[A] (A ⊗[R] N))
⊢ Eq (α := B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[A] (A ⊗[R] N)) (baseChange B (baseChange A f))
    (((↑(LinearEquiv.symm (cancelBaseChange R A B B N)) : B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) :
        B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) ∘ₗ
      (baseChange B f ∘ₗ (↑(cancelBaseChange R A B B M) : B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] M) :
        B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] N))

Tactic:
ext