awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
⊢ map f (r • g) = HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
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)
have a : Eq (α := P ⊗[R] Q)
  ((((TensorProduct.curry
                ((↑R :
                    {S : Type uA} →
                      {M : Type (max uM uN)} →
                        {M₂ : Type (max uP uQ)} →
                          [inst : Semiring R] →
                            [inst_15 : Semiring S] →
                              [inst_16 : AddCommMonoid M] →
                                [inst_17 : AddCommMonoid M₂] →
                                  [inst_18 : Module R M] →
                                    [inst_19 : Module R M₂] →
                                      [inst_20 : Module S M] →
                                        [inst_21 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (map f (r • g) : M ⊗[R] N →ₗ[A] 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)
  ((((TensorProduct.curry
                ((↑R :
                    {S : Type uA} →
                      {M : Type (max uM uN)} →
                        {M₂ : Type (max uP uQ)} →
                          [inst : Semiring R] →
                            [inst_15 : Semiring S] →
                              [inst_16 : AddCommMonoid M] →
                                [inst_17 : AddCommMonoid M₂] →
                                  [inst_18 : Module R M] →
                                    [inst_19 : Module R M₂] →
                                      [inst_20 : Module S M] →
                                        [inst_21 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) r (map f g : M ⊗[R] N →ₗ[A] 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)
Tactic: simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
    smul_apply, tmul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
⊢ map (b • f) g = HSMul.hSMul (β := M ⊗[R] N →ₗ[A] P ⊗[R] Q) b (map f g : M ⊗[R] N →ₗ[A] P ⊗[R] Q)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
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 Q
inst_15 : Module R Q
inst_16 : Algebra A B
inst_17 : IsScalarTower A B M
f : N →ₗ[R] Q
⊢ Eq (α := M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] Q)
    ((((lTensor B M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[B] M ⊗[R] Q) : (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[B] M ⊗[R] Q) f :
          M ⊗[R] N →ₗ[B] M ⊗[R] Q) ∘ₗ
        ((↑(cancelBaseChange R A B M N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) :
      M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] Q)
    ((↑(cancelBaseChange R A B M Q) : M ⊗[A] (A ⊗[R] Q) →ₗ[B] M ⊗[R] Q) ∘ₗ
        ((lTensor B M : (A ⊗[R] N →ₗ[A] A ⊗[R] Q) →ₗ[A] M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q)) :
            (a : A ⊗[R] N →ₗ[A] A ⊗[R] Q) → M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q))
          (((lTensor A A : (N →ₗ[R] Q) →ₗ[R] A ⊗[R] N →ₗ[A] A ⊗[R] Q) : (a : N →ₗ[R] Q) → A ⊗[R] N →ₗ[A] A ⊗[R] Q) f) :
      M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] Q)
have a : ∀ (x : M) (x_1 : N),
  Eq (α := M ⊗[R] Q)
    ((((curry
                  (((curry
                          ((((lTensor B M : (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[B] M ⊗[R] Q) :
                                  (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[B] M ⊗[R] Q)
                                f :
                              M ⊗[R] N →ₗ[B] M ⊗[R] Q) ∘ₗ
                            ((↑(cancelBaseChange R A B M N) : M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N) :
                              M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[R] N)) :
                        M →ₗ[B] A ⊗[R] N →ₗ[A] M ⊗[R] Q) :
                      (a : M) → A ⊗[R] N →ₗ[A] M ⊗[R] Q)
                    x) :
                A →ₗ[A] N →ₗ[R] M ⊗[R] Q) :
              (a : A) → N →ₗ[R] M ⊗[R] Q)
            1 :
          (a : N) → M ⊗[R] Q)
        x_1 :
      M ⊗[R] Q)
    ((((curry
                  (((curry
                          ((↑(cancelBaseChange R A B M Q) : M ⊗[A] (A ⊗[R] Q) →ₗ[B] M ⊗[R] Q) ∘ₗ
                            ((lTensor B M : (A ⊗[R] N →ₗ[A] A ⊗[R] Q) →ₗ[A] M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q)) :
                                (a : A ⊗[R] N →ₗ[A] A ⊗[R] Q) → M ⊗[A] (A ⊗[R] N) →ₗ[B] M ⊗[A] (A ⊗[R] Q))
                              (((lTensor A A : (N →ₗ[R] Q) →ₗ[R] A ⊗[R] N →ₗ[A] A ⊗[R] Q) :
                                  (a : N →ₗ[R] Q) → A ⊗[R] N →ₗ[A] A ⊗[R] Q)
                                f)) :
                        M →ₗ[B] A ⊗[R] N →ₗ[A] M ⊗[R] Q) :
                      (a : M) → A ⊗[R] N →ₗ[A] M ⊗[R] Q)
                    x) :
                A →ₗ[A] N →ₗ[R] M ⊗[R] Q) :
              (a : A) → N →ₗ[R] M ⊗[R] Q)
            1 :
          (a : N) → M ⊗[R] Q)
        x_1 :
      M ⊗[R] Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
n : N
q : Q
a b : A
⊢ Eq (α := A ⊗[R] (N ⊗[R] Q))
    ((LinearEquiv.symm (distribBaseChange R A N Q) : (a : A ⊗[R] N ⊗[A] (A ⊗[R] Q)) → A ⊗[R] (N ⊗[R] Q))
        (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q)) :
      A ⊗[R] (N ⊗[R] Q))
    ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q) : A ⊗[R] (N ⊗[R] Q))
have apply : Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
  ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
      ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
    A ⊗[R] N ⊗[A] (A ⊗[R] Q))
  (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))
Tactic: apply ((distribBaseChange R A N Q).apply_eq_iff_symm_apply.mp ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid Q
inst_6 : Module R Q
n : N
q : Q
a b : A
⊢ Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
        ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
      A ⊗[R] N ⊗[A] (A ⊗[R] Q))
    (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))
have rw : Eq (α := A ⊗[R] N ⊗[A] (A ⊗[R] Q))
  ((LinearEquiv.toAddEquiv (distribBaseChange R A N Q) : (a : A ⊗[R] (N ⊗[R] Q)) → A ⊗[R] N ⊗[A] (A ⊗[R] Q))
      ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) :
    A ⊗[R] N ⊗[A] (A ⊗[R] Q))
  ((b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q) : A ⊗[R] N ⊗[A] (A ⊗[R] Q))
Tactic: rw [tmul_eq_smul_one_tmul b, ← smul_tmul, smul_tmul', mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Eq (α := A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) (cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N)
    (TensorProduct.lid A (A ⊗[R] N) : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N)
have h : ∀ (x : A ⊗[A] (A ⊗[R] N)),
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : A
y : A ⊗[R] N
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
have h : Eq (α := A ⊗[R] N)
  (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] 0) :
    A ⊗[R] N)
  ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] 0) : A ⊗[R] N)
Tactic: induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : A
y : A ⊗[R] N
h :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] 0) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] 0) : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
have h₁ : ∀ (a : A) (m : N),
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] (a ⊗ₜ[R] m)) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (a ⊗ₜ[R] m)) : A ⊗[R] N)
Tactic: induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : A
y : A ⊗[R] N
h :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] 0) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] 0) : A ⊗[R] N)
h₁ :
  ∀ (a : A) (m : N),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] (a ⊗ₜ[R] m)) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (a ⊗ₜ[R] m)) : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
have h₂ : ∀ (x y : A ⊗[R] N)
  (hx :
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] x) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] x) : A ⊗[R] N))
  (hy :
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] y) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)),
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] (x + y)) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] (x + y)) : A ⊗[R] N)
Tactic: induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
x : A ⊗[A] (A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)
have h : Eq (α := A ⊗[R] N)
  (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
  ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
Tactic: induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul b y =>
    induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
  | add x y hx hy => simp [hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
x : A ⊗[A] (A ⊗[R] N)
h :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)
have h₁ : ∀ (b : A) (y : A ⊗[R] N),
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
        (b ⊗ₜ[A] y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
Tactic: induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul b y =>
    induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
  | add x y hx hy => simp [hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type uR
A : Type uA
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid N
inst_4 : Module R N
x : A ⊗[A] (A ⊗[R] N)
h :
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) 0)
h₁ :
  ∀ (b : A) (y : A ⊗[R] N),
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N)
          (b ⊗ₜ[A] y) :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (b ⊗ₜ[A] y) : A ⊗[R] N)
⊢ Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N)
have h₂ : ∀ (x y : A ⊗[A] (A ⊗[R] N))
  (hx :
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) x : A ⊗[R] N))
  (hy :
    Eq (α := A ⊗[R] N)
      (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) y :
        A ⊗[R] N)
      ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) y : A ⊗[R] N)),
  Eq (α := A ⊗[R] N)
    (((cancelBaseChange R A A A N : A ⊗[A] (A ⊗[R] N) ≃ₗ[A] A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (x + y) :
      A ⊗[R] N)
    ((TensorProduct.lid A (A ⊗[R] N) : (a : A ⊗[A] (A ⊗[R] N)) → A ⊗[R] N) (x + y) : A ⊗[R] N)
Tactic: induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul b y =>
    induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]
  | add x y hx hy => simp [hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
⊢ baseChange A (f + g) = HAdd.hAdd (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
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
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A 0) 0
have 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)
Tactic: ext