awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ha :
  ∀ (x : ULift.{u₂, u_5} S),
    Eq.{u_5 + 1} (α := S)
      (ULift.down.{u₂, u_5}
        ((AlgHom.comp (lmul' (ULift.{u₁, u_4} R)) includeLeft : (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S) x))
      (ULift.down.{u₂, u_5}
        ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
              (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
                (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                  ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                    ULift.{u_8, u_5} (S ⊗[R] S)))
              includeLeft :
            (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
          x))
⊢ Eq (α := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
    (lmul' (ULift.{u₁, u_4} R))
    (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
      (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
        ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R] ULift.{u_8, u_5} (S ⊗[R] S)))
have hb : ∀ (x : ULift.{u₂, u_5} S),
  Eq.{u_5 + 1} (α := S)
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (AlgHom.restrictScalars (ULift.{u₁, u_4} R) (S := ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R)))
            includeRight :
          (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
        x))
    (ULift.down.{u₂, u_5}
      ((AlgHom.comp (B := ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S)
            (AlgHom.restrictScalars (ULift.{u₁, u_4} R)
              (AlgHom.comp (AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R))
                (↑(AlgEquiv.symm (uliftEquiv R (ULift.{u₁, u_4} R) S S)) :
                  ULift.{u₂, u_5} S ⊗[ULift.{u₁, u_4} R] ULift.{u₂, u_5} S →ₐ[ULift.{u₁, u_4} R]
                    ULift.{u_8, u_5} (S ⊗[R] S))))
            includeRight :
          (a : ULift.{u₂, u_5} S) → ULift.{u₂, u_5} S)
        x))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
⊢ A ⊗[R] B[M] ≃ₐ[A] (A ⊗[R] B)[M]
have refine_1 : Eq (α := (A ⊗[R] B)[M] →ₐ[A] (A ⊗[R] B)[M])
  (AlgHom.comp
    (Algebra.TensorProduct.lift
        (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
        (mapAlgHom M includeRight) sorry :
      A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
    (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M]))
  (AlgHom.id A (A ⊗[R] B)[M])
Tactic: refine .ofAlgHom
    (Algebra.TensorProduct.lift
      ((IsScalarTower.toAlgHom A (A ⊗[R] B) _).comp Algebra.TensorProduct.includeLeft)
      (mapAlgHom _ Algebra.TensorProduct.includeRight) fun p n ↦ .all ..)
      tensorEquiv.invFun ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_1 :
  Eq (α := (A ⊗[R] B)[M] →ₐ[A] (A ⊗[R] B)[M])
    (AlgHom.comp
      (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯ :
        A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
      (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M]))
    (AlgHom.id A (A ⊗[R] B)[M])
⊢ A ⊗[R] B[M] ≃ₐ[A] (A ⊗[R] B)[M]
have refine_2 : Eq (α := A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
  (AlgHom.comp tensorEquiv.invFun
      (Algebra.TensorProduct.lift
        (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
        (mapAlgHom M includeRight) sorry) :
    A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
  (AlgHom.id A (A ⊗[R] B[M]) : A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
Tactic: refine .ofAlgHom
    (Algebra.TensorProduct.lift
      ((IsScalarTower.toAlgHom A (A ⊗[R] B) _).comp Algebra.TensorProduct.includeLeft)
      (mapAlgHom _ Algebra.TensorProduct.includeRight) fun p n ↦ .all ..)
      tensorEquiv.invFun ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
⊢ Eq (α := (A ⊗[R] B)[M] →ₐ[A] (A ⊗[R] B)[M])
    (AlgHom.comp
      (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯ :
        A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
      (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M]))
    (AlgHom.id A (A ⊗[R] B)[M])
have refine_1 : Eq (α := (A ⊗[R] B)[M] →ₗ[A] (A ⊗[R] B)[M])
  (AlgHom.toLinearMap
    (AlgHom.comp
      (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) sorry :
        A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
      (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])))
  (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]))
Tactic: apply AlgHom.toLinearMap_injective
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
⊢ Eq (α := (A ⊗[R] B)[M] →ₗ[A] (A ⊗[R] B)[M])
    (AlgHom.toLinearMap
      (AlgHom.comp
        (Algebra.TensorProduct.lift
            (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
            (mapAlgHom M includeRight) ⋯ :
          A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
        (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])))
    (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]))
have refine_1 : ∀ (x : M) (x_1 : B) (m : M),
  Eq (α := A ⊗[R] B)
    ((((((AlgebraTensorModule.curry
                        (AlgHom.toLinearMap
                            (AlgHom.comp
                              (Algebra.TensorProduct.lift
                                  (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M])
                                    includeLeft)
                                  (mapAlgHom M includeRight) sorry :
                                A ⊗[R] B[M] →ₐ[A] (A ⊗[R] B)[M])
                              (tensorEquiv.invFun : (A ⊗[R] B)[M] →ₐ[A] A ⊗[R] B[M])) ∘ₗ
                          lsingle x) :
                      A →ₗ[A] B →ₗ[R] (A ⊗[R] B)[M]) :
                    (a : A) → B →ₗ[R] (A ⊗[R] B)[M])
                  1 :
                (a : B) → (A ⊗[R] B)[M])
              x_1 :
            (A ⊗[R] B)[M]) :
          (a : M) → A ⊗[R] B)
        m :
      A ⊗[R] B)
    ((((((AlgebraTensorModule.curry (AlgHom.toLinearMap (AlgHom.id A (A ⊗[R] B)[M]) ∘ₗ lsingle x) :
                      A →ₗ[A] B →ₗ[R] (A ⊗[R] B)[M]) :
                    (a : A) → B →ₗ[R] (A ⊗[R] B)[M])
                  1 :
                (a : B) → (A ⊗[R] B)[M])
              x_1 :
            (A ⊗[R] B)[M]) :
          (a : M) → A ⊗[R] B)
        m :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
⊢ Eq (α := A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
    (AlgHom.comp tensorEquiv.invFun
        (Algebra.TensorProduct.lift
          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
          (mapAlgHom M includeRight) ⋯) :
      A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
    (AlgHom.id A (A ⊗[R] B[M]) : A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M])
have refine_2 : Eq (α := B[M] →ₐ[R] A ⊗[R] B[M])
  (AlgHom.comp (B := A ⊗[R] B[M])
    (AlgHom.restrictScalars R
      (AlgHom.comp tensorEquiv.invFun
          (Algebra.TensorProduct.lift
            (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
            (mapAlgHom M includeRight) sorry) :
        A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
    includeRight)
  (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
⊢ Eq (α := B[M] →ₐ[R] A ⊗[R] B[M])
    (AlgHom.comp (B := A ⊗[R] B[M])
      (AlgHom.restrictScalars R
        (AlgHom.comp tensorEquiv.invFun
            (Algebra.TensorProduct.lift
              (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
              (mapAlgHom M includeRight) ⋯) :
          A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
      includeRight)
    (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight)
have refine_2 : Eq (α := B[M] →ₗ[R] A ⊗[R] B[M])
  (AlgHom.toLinearMap
    (AlgHom.comp (B := A ⊗[R] B[M])
      (AlgHom.restrictScalars R
        (AlgHom.comp tensorEquiv.invFun
            (Algebra.TensorProduct.lift
              (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
              (mapAlgHom M includeRight) sorry) :
          A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
      includeRight))
  (AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight))
Tactic: apply AlgHom.toLinearMap_injective
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
⊢ Eq (α := B[M] →ₗ[R] A ⊗[R] B[M])
    (AlgHom.toLinearMap
      (AlgHom.comp (B := A ⊗[R] B[M])
        (AlgHom.restrictScalars R
          (AlgHom.comp tensorEquiv.invFun
              (Algebra.TensorProduct.lift
                (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
                (mapAlgHom M includeRight) ⋯) :
            A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
        includeRight))
    (AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight))
have refine_2 : ∀ (x : M) (x_1 : B),
  Eq (α := A ⊗[R] B[M])
    ((AlgHom.toLinearMap
              (AlgHom.comp (B := A ⊗[R] B[M])
                (AlgHom.restrictScalars R
                  (AlgHom.comp tensorEquiv.invFun
                      (Algebra.TensorProduct.lift
                        (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
                        (mapAlgHom M includeRight) sorry) :
                    A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
                includeRight) ∘ₗ
            lsingle x :
          (a : B) → A ⊗[R] B[M])
        x_1 :
      A ⊗[R] B[M])
    (((AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight) ∘ₗ
              lsingle x :
            B →ₗ[R] A ⊗[R] B[M]) :
          (a : B) → A ⊗[R] B[M])
        x_1 :
      A ⊗[R] B[M])
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommMonoid M
a : A
p : R[M]
⊢ (scalarTensorEquiv R A : (a : A ⊗[R] R[M]) → A[M]) (a ⊗ₜ[R] p) =
    HSMul.hSMul (β := A[M]) a ((mapAlgHom M (ofId R A) : (a : R[M]) → A[M]) p : A[M])
have hfg : ∀ (m : M),
  Eq.{u_4 + 1} (α := A) ((((scalarTensorEquiv R A : (a : A ⊗[R] R[M]) → A[M]) (a ⊗ₜ[R] p) : A[M]) : (a : M) → A) m : A)
    ((HSMul.hSMul (β := A[M]) a ((mapAlgHom M (ofId R A) : (a : R[M]) → A[M]) p : A[M]) : (a : M) → A) m : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommMonoid M
a : A
p : R[M]
m : M
⊢ Eq.{u_4 + 1} (α := A) ((((scalarTensorEquiv R A : (a : A ⊗[R] R[M]) → A[M]) (a ⊗ₜ[R] p) : A[M]) : (a : M) → A) m : A)
    ((HSMul.hSMul (β := A[M]) a ((mapAlgHom M (ofId R A) : (a : R[M]) → A[M]) p : A[M]) : (a : M) → A) m : A)
have hfg : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : M) → R) m : R) a =
  HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) ((p : (a : M) → R) m : R) : A)
Tactic: simp [scalarTensorEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
x : A[M]
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] x) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M])
have zero : Eq (α := B[M])
  (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
        (a : S ⊗[R] A[M]) → B[M])
      (1 ⊗ₜ[R] 0) :
    B[M])
  ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) 0 : B[M])
Tactic: induction x using induction_linear
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
x : A[M]
zero :
  Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] 0) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) 0 : B[M])
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] x) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M])
have add : ∀ (x y : A[M]),
  Eq (α := B[M])
      (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
            (a : S ⊗[R] A[M]) → B[M])
          (1 ⊗ₜ[R] x) :
        B[M])
      ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M]) →
    Eq (α := B[M])
        (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
              (a : S ⊗[R] A[M]) → B[M])
            (1 ⊗ₜ[R] y) :
          B[M])
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) y : B[M]) →
      Eq (α := B[M])
        (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
              (a : S ⊗[R] A[M]) → B[M])
            (1 ⊗ₜ[R] (x + y)) :
          B[M])
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (x + y) : B[M])
Tactic: induction x using induction_linear
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
x : A[M]
zero :
  Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] 0) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) 0 : B[M])
add :
  ∀ (x y : A[M]),
    Eq (α := B[M])
        (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
              (a : S ⊗[R] A[M]) → B[M])
            (1 ⊗ₜ[R] x) :
          B[M])
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M]) →
      Eq (α := B[M])
          (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) :
                  S ⊗[R] A[M] ≃ₗ[S] B[M]) :
                (a : S ⊗[R] A[M]) → B[M])
              (1 ⊗ₜ[R] y) :
            B[M])
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) y : B[M]) →
        Eq (α := B[M])
          (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) :
                  S ⊗[R] A[M] ≃ₗ[S] B[M]) :
                (a : S ⊗[R] A[M]) → B[M])
              (1 ⊗ₜ[R] (x + y)) :
            B[M])
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (x + y) : B[M])
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] x) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M])
have single : ∀ (m : M) (r : A),
  Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] single m r) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (single m r) : B[M])
Tactic: induction x using induction_linear
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
s : σ
n : N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) (X s ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0 : S ⊗[R] N)
have rw : Eq (α := S ⊗[R] N) (coeff d (X s) ⊗ₜ[R] n) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
Tactic: rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : Eq (α := S ⊗[R] N) (coeff d (X s) ⊗ₜ[R] n) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) (X s ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0 : S ⊗[R] N)
have rw₁ : Eq (α := S ⊗[R] N) ((if Finsupp.single s 1 = d then 1 else 0) ⊗ₜ[R] n) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
Tactic: rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : Eq (α := S ⊗[R] N) (coeff d (X s) ⊗ₜ[R] n) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
rw₁ :
  Eq (α := S ⊗[R] N) ((if Finsupp.single s 1 = d then 1 else 0) ⊗ₜ[R] n)
    (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) (X s ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0 : S ⊗[R] N)
have rw₂ : Eq (α := S ⊗[R] N) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
Tactic: rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
e : σ →₀ ℕ
r : R
n : N
d : σ →₀ ℕ
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N)
            ((monomial e : (a : R) → MvPolynomial σ R) r ⊗ₜ[R] n) :
          Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if e = d then r • n else 0
have rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d ((monomial e : (a : R) → MvPolynomial σ R) r)) n = if e = d then r • n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
e : σ →₀ ℕ
r : R
n : N
d : σ →₀ ℕ
rw :
  HSMul.hSMul.{u, v, v} (α := R) (coeff d ((monomial e : (a : R) → MvPolynomial σ R) r)) n = if e = d then r • n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N)
            ((monomial e : (a : R) → MvPolynomial σ R) r ⊗ₜ[R] n) :
          Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if e = d then r • n else 0
have rw₁ : (if e = d then r else 0) • n = if e = d then r • n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
e : σ →₀ ℕ
r : R
n : N
d : σ →₀ ℕ
rw :
  HSMul.hSMul.{u, v, v} (α := R) (coeff d ((monomial e : (a : R) → MvPolynomial σ R) r)) n = if e = d then r • n else 0
rw₁ : (if e = d then r else 0) • n = if e = d then r • n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N)
            ((monomial e : (a : R) → MvPolynomial σ R) r ⊗ₜ[R] n) :
          Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if e = d then r • n else 0
have rw₂ : (if e = d then r • n else HSMul.hSMul.{u, v, v} (α := R) 0 n) = if e = d then r • n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]