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 : Semiring 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 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : Module A P'
inst_20 : Module B P'
inst_21 : IsScalarTower R A P'
inst_22 : IsScalarTower R B P'
inst_23 : SMulCommClass A B P'
inst_24 : AddCommMonoid Q'
inst_25 : Module R Q'
inst_26 : Module B P
inst_27 : IsScalarTower R B P
inst_28 : SMulCommClass A B P
x_1 : B
x_2 : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ Eq.{uP + 1} (α := P) (((lift (x_1 • x_2) : M ⊗[R] N →ₗ[A] P) : (a : M ⊗[R] N) → P) (x ⊗ₜ[R] y) : P)
    ((HSMul.hSMul (α := B) (β := M ⊗[R] N →ₗ[A] P) ((RingHom.id B : (a : B) → B) x_1 : B)
            (lift x_2 : M ⊗[R] N →ₗ[A] P) :
          (a : M ⊗[R] N) → P)
        (x ⊗ₜ[R] y) :
      P)

Tactic:
simp only [lift_tmul, smul_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply, TensorProduct.AlgebraTensorModule.lift_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Eq (α := M →ₗ[R] N →ₗ[R] M ⊗[R] N) (mk R R M N) (TensorProduct.mk R M N)

Tactic:
rfl

Premises used: LinearMap.mk₂, LinearMap.mk₂'ₛₗ, TensorProduct.AlgebraTensorModule.mk, LinearMap.mk₂', TensorProduct.mk, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f : M →ₗ[A] P
g : N →ₗ[R] Q
m : M
n : N
⊢ Eq (α := P ⊗[R] Q) (((map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : (a : M ⊗[R] N) → P ⊗[R] Q) (m ⊗ₜ[R] n) : P ⊗[R] Q)
    ((f : (a : M) → P) m ⊗ₜ[R] (g : (a : N) → Q) n : 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
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] N) (map LinearMap.id LinearMap.id : M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (LinearMap.id : M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
ext fun _ _ => rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
inst_15 : AddCommMonoid P'
inst_16 : Module R P'
inst_17 : Module A P'
inst_18 : IsScalarTower R A P'
inst_19 : AddCommMonoid Q'
inst_20 : Module R Q'
f₂ : P →ₗ[A] P'
f₁ : M →ₗ[A] P
g₂ : Q →ₗ[R] Q'
g₁ : N →ₗ[R] Q
⊢ Eq (α := M ⊗[R] N →ₗ[A] P' ⊗[R] Q') (map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) : M ⊗[R] N →ₗ[A] P' ⊗[R] Q')
    ((map f₂ g₂ : P ⊗[R] Q →ₗ[A] P' ⊗[R] Q') ∘ₗ (map f₁ g₁ : M ⊗[R] N →ₗ[A] P ⊗[R] Q) : M ⊗[R] N →ₗ[A] P' ⊗[R] Q')

Tactic:
ext fun _ _ => rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] N) (map 1 1 : M ⊗[R] N →ₗ[A] M ⊗[R] N) (1 : M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
map_id

Premises used: TensorProduct.AlgebraTensorModule.map_id
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
f₁ f₂ : M →ₗ[A] M
g₁ g₂ : N →ₗ[R] N
⊢ map (f₁ * f₂) (g₁ * g₂) =
    HMul.hMul (α := M ⊗[R] N →ₗ[A] M ⊗[R] N) (β := M ⊗[R] N →ₗ[A] M ⊗[R] N) (map f₁ g₁ : M ⊗[R] N →ₗ[A] M ⊗[R] N)
      (map f₂ g₂ : M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
map_comp _ _ _ _

Premises used: TensorProduct.AlgebraTensorModule.map_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
a :
  ∀ (x : M) (x_1 : N),
    Eq (α := P ⊗[R] Q)
      (((((curry (map (f₁ + f₂) g) : M →ₗ[A] N →ₗ[R] P ⊗[R] Q) : (a : M) → N →ₗ[R] P ⊗[R] Q) x : N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
      (((((curry
                      (HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q)
                        (map f₁ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q) (map f₂ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                    M →ₗ[A] N →ₗ[R] P ⊗[R] Q) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
⊢ map (f₁ + f₂) g =
    HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (map f₁ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)
      (map f₂ g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
a :
  ∀ (x : M) (x_1 : N),
    Eq (α := P ⊗[R] Q)
      (((((curry (map f (g₁ + g₂)) : M →ₗ[A] N →ₗ[R] P ⊗[R] Q) : (a : M) → N →ₗ[R] P ⊗[R] Q) x : N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
      (((((curry
                      (HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q)
                        (map f g₁ : M ⊗[R] N →ₗ[A] P ⊗[R] Q) (map f g₂ : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                    M →ₗ[A] N →ₗ[R] P ⊗[R] Q) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
⊢ map f (g₁ + g₂) =
    HAdd.hAdd (α := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) (map f g₁ : M ⊗[R] N →ₗ[A] P ⊗[R] Q)
      (map f g₂ : M ⊗[R] N →ₗ[A] P ⊗[R] Q)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid Q
inst_14 : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
a :
  ∀ (x : M) (x_1 : N),
    Eq (α := P ⊗[R] Q)
      (((((curry (map f (r • g)) : M →ₗ[A] N →ₗ[R] P ⊗[R] Q) : (a : M) → N →ₗ[R] P ⊗[R] Q) x : N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
      (((((curry (HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                    M →ₗ[A] N →ₗ[R] P ⊗[R] Q) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
⊢ map f (r • g) = HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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_1 : Semiring 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 : IsScalarTower R A M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : AddCommMonoid P
inst_12 : Module R P
inst_13 : Module A P
inst_14 : IsScalarTower R A P
inst_15 : AddCommMonoid Q
inst_16 : Module R Q
inst_17 : Module B P
inst_18 : IsScalarTower R B P
inst_19 : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
a :
  ∀ (x : M) (x_1 : N),
    Eq (α := P ⊗[R] Q)
      (((((curry (map (b • f) g) : M →ₗ[A] N →ₗ[R] P ⊗[R] Q) : (a : M) → N →ₗ[R] P ⊗[R] Q) x : N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
      (((((curry (HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) b (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)) :
                    M →ₗ[A] N →ₗ[R] P ⊗[R] Q) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
⊢ map (b • f) g = HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) b (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)

Tactic:
ext
-- 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 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ map f g = TensorProduct.map f g

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
f : N →ₗ[R] Q
⊢ Eq (α := (a : M ⊗[R] N) → M ⊗[R] Q)
    (⇑(((lTensor A M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] Q) : (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[A] M ⊗[R] Q) f :
          M ⊗[R] N →ₗ[A] M ⊗[R] Q) :
      (a : M ⊗[R] N) → M ⊗[R] Q)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] Q)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
f : N →ₗ[R] Q
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] Q)
    ((↑R :
        {S : Type uA} →
          {M : Type (max uM uN)} →
            {M₂ : Type (max uM uQ)} →
              [inst : Semiring R] →
                [inst_11 : Semiring S] →
                  [inst_12 : AddCommMonoid M] →
                    [inst_13 : AddCommMonoid M₂] →
                      [inst_14 : Module R M] →
                        [inst_15 : Module R M₂] →
                          [inst_16 : Module S M] →
                            [inst_17 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := A)
      (((lTensor A M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] Q) : (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[A] M ⊗[R] Q) f))
    (LinearMap.lTensor M f)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, Quotient.liftOn', AddCon.liftOn, LinearMap.lTensor, TensorProduct.map, TensorProduct, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
f : N →ₗ[R] Q
m : M
n : N
⊢ Eq (α := M ⊗[R] Q)
    (((((lTensor A M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] Q) : (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[A] M ⊗[R] Q) f :
            M ⊗[R] N →ₗ[A] M ⊗[R] Q) :
          (a : M ⊗[R] N) → M ⊗[R] Q)
        (m ⊗ₜ[R] n) :
      M ⊗[R] Q)
    (m ⊗ₜ[R] (f : (a : N) → Q) n : M ⊗[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
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (((lTensor A M : (N →ₗ[R] N) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : N →ₗ[R] N) → M ⊗[R] N →ₗ[A] M ⊗[R] N)
        LinearMap.id :
      M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (LinearMap.id : M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
ext fun _ _ => rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
Q : Type uQ
Q' : Type uQ'
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid Q
inst_10 : Module R Q
inst_11 : AddCommMonoid Q'
inst_12 : Module R Q'
f₂ : Q →ₗ[R] Q'
f₁ : N →ₗ[R] Q
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] Q')
    (((lTensor A M : (N →ₗ[R] Q') →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] Q') : (a : N →ₗ[R] Q') → M ⊗[R] N →ₗ[A] M ⊗[R] Q')
        (f₂ ∘ₗ f₁) :
      M ⊗[R] N →ₗ[A] M ⊗[R] Q')
    (((lTensor A M : (Q →ₗ[R] Q') →ₗ[R] M ⊗[R] Q →ₗ[A] M ⊗[R] Q') : (a : Q →ₗ[R] Q') → M ⊗[R] Q →ₗ[A] M ⊗[R] Q') f₂ ∘ₗ
        ((lTensor A M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] Q) : (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[A] M ⊗[R] Q) f₁ :
      M ⊗[R] N →ₗ[A] M ⊗[R] Q')

Tactic:
ext fun _ _ => rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (((lTensor A M : (N →ₗ[R] N) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : N →ₗ[R] N) → M ⊗[R] N →ₗ[A] M ⊗[R] N) 1) 1

Tactic:
map_id

Premises used: TensorProduct.AlgebraTensorModule.map_id, TensorProduct.AlgebraTensorModule.map, 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 : Semiring 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
f₁ f₂ : N →ₗ[R] N
⊢ ((lTensor A M : (N →ₗ[R] N) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : N →ₗ[R] N) → M ⊗[R] N →ₗ[A] M ⊗[R] N) (f₁ * f₂) =
    HMul.hMul (α := M ⊗[R] N →ₗ[A] M ⊗[R] N) (β := M ⊗[R] N →ₗ[A] M ⊗[R] N)
      (((lTensor A M : (N →ₗ[R] N) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : N →ₗ[R] N) → M ⊗[R] N →ₗ[A] M ⊗[R] N) f₁ :
        M ⊗[R] N →ₗ[A] M ⊗[R] N)
      (((lTensor A M : (N →ₗ[R] N) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : N →ₗ[R] N) → M ⊗[R] N →ₗ[A] M ⊗[R] N) f₂ :
        M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
lTensor_comp _ _

Premises used: TensorProduct.AlgebraTensorModule.lTensor_comp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
f : M →ₗ[A] P
⊢ Eq (α := (a : M ⊗[R] N) → P ⊗[R] N)
    (⇑(((rTensor R N : (M →ₗ[A] P) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] N) : (a : M →ₗ[A] P) → M ⊗[R] N →ₗ[A] P ⊗[R] N) f :
          M ⊗[R] N →ₗ[A] P ⊗[R] N) :
      (a : M ⊗[R] N) → P ⊗[R] N)
    (⇑(LinearMap.rTensor N
          ((↑R :
              {S : Type uA} →
                {M : Type uM} →
                  {M₂ : Type uP} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f)) :
      (a : M ⊗[R] N) → P ⊗[R] N)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
f : M →ₗ[A] P
⊢ Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] N)
    ((↑R :
        {S : Type uA} →
          {M : Type (max uM uN)} →
            {M₂ : Type (max uN uP)} →
              [inst : Semiring R] →
                [inst_13 : Semiring S] →
                  [inst_14 : AddCommMonoid M] →
                    [inst_15 : AddCommMonoid M₂] →
                      [inst_16 : Module R M] →
                        [inst_17 : Module R M₂] →
                          [inst_18 : Module S M] →
                            [inst_19 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := A)
      (((rTensor R N : (M →ₗ[A] P) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] N) : (a : M →ₗ[A] P) → M ⊗[R] N →ₗ[A] P ⊗[R] N) f))
    (LinearMap.rTensor N
      ((↑R :
          {S : Type uA} →
            {M : Type uM} →
              {M₂ : Type uP} →
                [inst : Semiring R] →
                  [inst_13 : Semiring S] →
                    [inst_14 : AddCommMonoid M] →
                      [inst_15 : AddCommMonoid M₂] →
                        [inst_16 : Module R M] →
                          [inst_17 : Module R M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f))

Tactic:
rfl

Premises used: LinearMap.restrictScalars, Quotient.liftOn', AddCon.liftOn, TensorProduct.map, TensorProduct, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, rfl, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
f : M →ₗ[A] P
m : M
n : N
⊢ Eq (α := P ⊗[R] N)
    (((((rTensor R N : (M →ₗ[A] P) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] N) : (a : M →ₗ[A] P) → M ⊗[R] N →ₗ[A] P ⊗[R] N) f :
            M ⊗[R] N →ₗ[A] P ⊗[R] N) :
          (a : M ⊗[R] N) → P ⊗[R] N)
        (m ⊗ₜ[R] n) :
      P ⊗[R] N)
    ((f : (a : M) → P) m ⊗ₜ[R] n : P ⊗[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 uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (((rTensor R N : (M →ₗ[A] M) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : M →ₗ[A] M) → M ⊗[R] N →ₗ[A] M ⊗[R] N)
        LinearMap.id :
      M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (LinearMap.id : M ⊗[R] N →ₗ[A] M ⊗[R] N)

Tactic:
ext fun _ _ => rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
P' : Type uP'
inst : CommSemiring R
inst_1 : Semiring 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
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : Module A P
inst_12 : IsScalarTower R A P
inst_13 : AddCommMonoid P'
inst_14 : Module R P'
inst_15 : Module A P'
inst_16 : IsScalarTower R A P'
f₂ : P →ₗ[A] P'
f₁ : M →ₗ[A] P
⊢ Eq (α := M ⊗[R] N →ₗ[A] P' ⊗[R] N)
    (((rTensor R N : (M →ₗ[A] P') →ₗ[R] M ⊗[R] N →ₗ[A] P' ⊗[R] N) : (a : M →ₗ[A] P') → M ⊗[R] N →ₗ[A] P' ⊗[R] N)
        (f₂ ∘ₗ f₁) :
      M ⊗[R] N →ₗ[A] P' ⊗[R] N)
    (((rTensor R N : (P →ₗ[A] P') →ₗ[R] P ⊗[R] N →ₗ[A] P' ⊗[R] N) : (a : P →ₗ[A] P') → P ⊗[R] N →ₗ[A] P' ⊗[R] N) f₂ ∘ₗ
        ((rTensor R N : (M →ₗ[A] P) →ₗ[R] M ⊗[R] N →ₗ[A] P ⊗[R] N) : (a : M →ₗ[A] P) → M ⊗[R] N →ₗ[A] P ⊗[R] N) f₁ :
      M ⊗[R] N →ₗ[A] P' ⊗[R] N)

Tactic:
ext fun _ _ => rfl

Premises used: TensorProduct.AlgebraTensorModule.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : Semiring 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
⊢ Eq (α := M ⊗[R] N →ₗ[A] M ⊗[R] N)
    (((rTensor R N : (M →ₗ[A] M) →ₗ[R] M ⊗[R] N →ₗ[A] M ⊗[R] N) : (a : M →ₗ[A] M) → M ⊗[R] N →ₗ[A] M ⊗[R] N) 1) 1

Tactic:
map_id

Premises used: TensorProduct.AlgebraTensorModule.map_id, TensorProduct.AlgebraTensorModule.map, TensorProduct.AlgebraTensorModule.lift