awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    x
have zero : Membership.mem (γ := Subring (A ⊗[R] B))
  (Subring.closure
    (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪ Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
  0
Tactic: induction x with
  | zero => exact zero_mem _
  | tmul x y =>
    convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _
    · simp
    · exact mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))
  | add x y _ _ => exact add_mem ‹_› ‹_›
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
zero :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    0
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    x
have tmul : ∀ (x : A) (y : B),
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    (x ⊗ₜ[R] y)
Tactic: induction x with
  | zero => exact zero_mem _
  | tmul x y =>
    convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _
    · simp
    · exact mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))
  | add x y _ _ => exact add_mem ‹_› ‹_›
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
zero :
  Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    0
tmul :
  ∀ (x : A) (y : B),
    Membership.mem (γ := Subring (A ⊗[R] B))
      (Subring.closure
        (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
          Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
      (x ⊗ₜ[R] y)
⊢ Membership.mem (γ := Subring (A ⊗[R] B))
    (Subring.closure
      (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
        Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
    x
have add : ∀ (x y : A ⊗[R] B),
  Membership.mem (γ := Subring (A ⊗[R] B))
      (Subring.closure
        (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
          Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
      x →
    Membership.mem (γ := Subring (A ⊗[R] B))
        (Subring.closure
          (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
            Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
        y →
      Membership.mem (γ := Subring (A ⊗[R] B))
        (Subring.closure
          (Set.range (ι := A) (⇑includeLeft : (a : A) → A ⊗[R] B) ∪
            Set.range (ι := B) (⇑includeRight : (a : B) → A ⊗[R] B)))
        (x + y)
Tactic: induction x with
  | zero => exact zero_mem _
  | tmul x y =>
    convert_to (Algebra.TensorProduct.includeLeftRingHom (R := R) x) *
      (Algebra.TensorProduct.includeRight y) ∈ _
    · simp
    · exact mul_mem (Subring.subset_closure (.inl ⟨x, rfl⟩))
        (Subring.subset_closure (.inr ⟨_, rfl⟩))
  | add x y _ _ => exact add_mem ‹_› ‹_›
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
⊢ Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A ((fun (x : B) ↦ 1 ⊗ₜ[R] x) '' s)) ⊤
have suffices : Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A (↑(Subalgebra.map includeRight ⊤) : Set (A ⊗[R] B))) ⊤
Tactic: suffices h : adjoin A ((⊤ : Subalgebra R B).map (includeRight (A := A)) : Set (A ⊗[R] B)) = ⊤ by
    simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set B
hs : Eq (α := Subalgebra R B) (adjoin R s) ⊤
⊢ Eq (α := Subalgebra A (A ⊗[R] B)) (adjoin A (↑(Subalgebra.map includeRight ⊤) : Set (A ⊗[R] B))) ⊤
have rw : LE.le (α := Submodule A (A ⊗[R] B))
  (Submodule.span A
    (↑(LinearMap.range (R := R) (M := B) (τ₁₂ := RingHom.id R)
          ((TensorProduct.mk R A B : (a : A) → B →ₗ[R] A ⊗[R] B) 1)) :
      Set (A ⊗[R] B)))
  ((Subalgebra.toSubmodule : (a : Subalgebra A (A ⊗[R] B)) → Submodule A (A ⊗[R] B))
    (adjoin A (↑(AlgHom.range includeRight) : Set (A ⊗[R] B))))
Tactic: rw [← Algebra.toSubmodule_eq_top, ← top_le_iff, Algebra.map_top, ← Submodule.baseChange_top,
    Submodule.baseChange_eq_span, Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
⊢ Function.Injective (α := M) (β := S ⊗[R] M)
    (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
have apply : Function.RightInverse (α := S ⊗[R] M) (β := M)
  (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
  (⇑(LinearMap.liftBaseChange S LinearMap.id) : (a : S ⊗[R] M) → M)
Tactic: apply Function.RightInverse.injective (g := LinearMap.liftBaseChange S LinearMap.id)
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : B
⊢ Eq (α := A ⊗[R] B →ₗ[A] A ⊗[R] B) (LinearMap.baseChange A ((lmul R B : (a : B) → Module.End R B) f))
    ((lmul A (A ⊗[R] B) : (a : A ⊗[R] B) → Module.End A (A ⊗[R] B)) (1 ⊗ₜ[R] f))
have a : ∀ (i : B),
  Eq (α := A ⊗[R] B)
    ((((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B : (a : B) → Module.End R B) f)) :
                A →ₗ[A] B →ₗ[R] A ⊗[R] B) :
              (a : A) → B →ₗ[R] A ⊗[R] B)
            1 :
          (a : B) → A ⊗[R] B)
        i :
      A ⊗[R] B)
    ((((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B) : (a : A ⊗[R] B) → Module.End A (A ⊗[R] B)) (1 ⊗ₜ[R] f)) :
                A →ₗ[A] B →ₗ[R] A ⊗[R] B) :
              (a : A) → B →ₗ[R] A ⊗[R] B)
            1 :
          (a : B) → A ⊗[R] B)
        i :
      A ⊗[R] B)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
r t : A
⊢ HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (r + t)
      (AlgHom.toLinearMap (Algebra.lsmul R R M)) =
    HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
        (AlgHom.toLinearMap (Algebra.lsmul R R M)) +
      HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) t
        (AlgHom.toLinearMap (Algebra.lsmul R R M))
have h : ∀ (x : B) (x_1 : M),
  Eq (α := M)
    ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (r + t)
                  (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)
    ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
                    (AlgHom.toLinearMap (Algebra.lsmul R R M)) +
                  HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) t
                    (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
n : R
r : A
⊢ HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (n • r)
      (AlgHom.toLinearMap (Algebra.lsmul R R M)) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) n : R)
      (HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
        (AlgHom.toLinearMap (Algebra.lsmul R R M)))
have h : ∀ (x : B) (x_1 : M),
  Eq (α := M)
    ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (n • r)
                  (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)
    ((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) n : R)
                  (HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
                    (AlgHom.toLinearMap (Algebra.lsmul R R M))) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (x * y) • m = x • y • m
have refine_1 : (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_1 : (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
⊢ (x * y) • m = x • y • m
have refine_2 : ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_1 : (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
refine_2 : ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)
⊢ (x * y) • m = x • y • m
have refine_3 : ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
have refine_1 : HMul.hMul (α := A ⊗[R] B) 0 0 • m = HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) 0 m)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_1 : HMul.hMul (α := A ⊗[R] B) 0 0 • m = HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) 0 m)
⊢ (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
have refine_1₁ : ∀ (x : A) (y : B),
  HMul.hMul (α := A ⊗[R] B) 0 (x ⊗ₜ[R] y) • m =
    HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_1 : HMul.hMul (α := A ⊗[R] B) 0 0 • m = HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) 0 m)
refine_1₁ :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) 0 (x ⊗ₜ[R] y) • m =
      HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m)
⊢ (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
have refine_1₂ : ∀ (x y : A ⊗[R] B),
  (0 * x) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (x • m) →
    (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m) →
      (0 * (x + y)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((x + y) • m)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)
have refine_2 : ∀ (x : A) (y : B),
  HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) 0 • m =
    HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (HSMul.hSMul (α := A ⊗[R] B) 0 m)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_2 :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) 0 • m =
      HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (HSMul.hSMul (α := A ⊗[R] B) 0 m)
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)
have refine_2₁ : ∀ (x : A) (y : B) (x_1 : A) (y_1 : B),
  HMul.hMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) (x ⊗ₜ[R] y) • m =
    HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) (HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_2 :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) 0 • m =
      HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (HSMul.hSMul (α := A ⊗[R] B) 0 m)
refine_2₁ :
  ∀ (x : A) (y : B) (x_1 : A) (y_1 : B),
    HMul.hMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) (x ⊗ₜ[R] y) • m =
      HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) (HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m)
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)
have refine_2₂ : ∀ (x y : A ⊗[R] B),
  (∀ (x_1 : A) (y : B), (x_1 ⊗ₜ[R] y * x) • m = HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y) (x • m)) →
    (∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)) →
      ∀ (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * (x + y)) • m = HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) ((x + y) • m)
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m
have refine_3 : ∀ (x y : A ⊗[R] B),
  (x * 0) • m = x • HSMul.hSMul (α := A ⊗[R] B) 0 m →
    (y * 0) • m = y • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((x + y) * 0) • m = (x + y) • HSMul.hSMul (α := A ⊗[R] B) 0 m
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_3 :
  ∀ (x y : A ⊗[R] B),
    (x * 0) • m = x • HSMul.hSMul (α := A ⊗[R] B) 0 m →
      (y * 0) • m = y • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((x + y) * 0) • m = (x + y) • HSMul.hSMul (α := A ⊗[R] B) 0 m
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m
have refine_3₁ : ∀ (x : A) (y : B) (x_1 y_1 : A ⊗[R] B),
  (x_1 * x ⊗ₜ[R] y) • m = x_1 • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m →
    (y_1 * x ⊗ₜ[R] y) • m = y_1 • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m →
      ((x_1 + y_1) * x ⊗ₜ[R] y) • m = (x_1 + y_1) • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_3 :
  ∀ (x y : A ⊗[R] B),
    (x * 0) • m = x • HSMul.hSMul (α := A ⊗[R] B) 0 m →
      (y * 0) • m = y • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((x + y) * 0) • m = (x + y) • HSMul.hSMul (α := A ⊗[R] B) 0 m
refine_3₁ :
  ∀ (x : A) (y : B) (x_1 y_1 : A ⊗[R] B),
    (x_1 * x ⊗ₜ[R] y) • m = x_1 • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m →
      (y_1 * x ⊗ₜ[R] y) • m = y_1 • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m →
        ((x_1 + y_1) * x ⊗ₜ[R] y) • m = (x_1 + y_1) • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m
have refine_3₂ : ∀ (x y : A ⊗[R] B),
  (∀ (x_1 y : A ⊗[R] B),
      (x_1 * x) • m = x_1 • x • m → (y * x) • m = y • x • m → ((x_1 + y) * x) • m = (x_1 + y) • x • m) →
    (∀ (x y_1 : A ⊗[R] B),
        (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m) →
      ∀ (x_1 y_1 : A ⊗[R] B),
        (x_1 * (x + y)) • m = x_1 • (x + y) • m →
          (y_1 * (x + y)) • m = y_1 • (x + y) • m → ((x_1 + y_1) * (x + y)) • m = (x_1 + y_1) • (x + y) • m
Tactic: refine TensorProduct.induction_on y ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a₁ : A
b₁ : B
a₂ : A
b₂ : B
⊢ HMul.hMul (α := A ⊗[R] B) (a₂ ⊗ₜ[R] b₂) (a₁ ⊗ₜ[R] b₁) • m =
    HSMul.hSMul (α := A ⊗[R] B) (a₂ ⊗ₜ[R] b₂) (HSMul.hSMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) m)
have refine_2 : Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((a₂ * a₁) ⊗ₜ[R] (b₂ * b₁)) : M →ₗ[R] M) : (a : M) → M) m : M)
  ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a₂ ⊗ₜ[R] b₂) : M →ₗ[R] M) : (a : M) → M)
      ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a₁ ⊗ₜ[R] b₁) : M →ₗ[R] M) : (a : M) → M) m : M) :
    M)
Tactic: simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * z) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (z • m)
hw : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * w) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (w • m)
a : A
b : B
⊢ (a ⊗ₜ[R] b * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) ((z + w) • m)
have refine_2 : Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b * (z + w)) : M →ₗ[R] M) : (a : M) → M) m : M)
  ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M)
      ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M) m : M) :
    M)
Tactic: simp only [(· • ·)] at hz hw ⊢