awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x y : M₁ ⊗[R] M₂
h_1 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x)
h_2 : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x + y))
have add₁ : motive
  (HAdd.hAdd (α := M) (β := M) ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x : M)
    ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y : M))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
have zero₁ : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) 0)
Tactic: induction y with
  | zero => rwa [map_zero]
  | tmul _ _ =>
    rw [TensorProduct.lift.tmul]
    apply tmul
  | add _ _ _ _ =>
    rw [map_add]
    apply add <;> assumption
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
zero₁ : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) 0)
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
have tmul₁ : ∀ (x : M₁) (y : M₂), motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y))
Tactic: induction y with
  | zero => rwa [map_zero]
  | tmul _ _ =>
    rw [TensorProduct.lift.tmul]
    apply tmul
  | add _ _ _ _ =>
    rw [map_add]
    apply add <;> assumption
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
zero₁ : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) 0)
tmul₁ : ∀ (x : M₁) (y : M₂), motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y))
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
have add₁ : ∀ (x y : M₁ ⊗[R] M₂),
  motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) x) →
    motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y) →
      motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x + y))
Tactic: induction y with
  | zero => rwa [map_zero]
  | tmul _ _ =>
    rw [TensorProduct.lift.tmul]
    apply tmul
  | add _ _ _ _ =>
    rw [map_add]
    apply add <;> assumption
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M) ((e : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y) : M)
      ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
⊢ TensorProduct.lift f = (↑e : M₁ ⊗[R] M₂ →ₗ[R] M)
have a : ∀ (x : M₁) (y : M₂),
  Eq.{u_4 + 1} (α := M)
    (((((AlgebraTensorModule.curry (TensorProduct.lift f) : M₁ →ₗ[R] M₂ →ₗ[R] M) : (a : M₁) → M₂ →ₗ[R] M) x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        y :
      M)
    (((((AlgebraTensorModule.curry (↑e : M₁ ⊗[R] M₂ →ₗ[R] M) : M₁ →ₗ[R] M₂ →ₗ[R] M) : (a : M₁) → M₂ →ₗ[R] M) x :
            M₂ →ₗ[R] M) :
          (a : M₂) → M)
        y :
      M)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he :
  ∀ (x : M₁) (y : M₂),
    Eq.{u_4 + 1} (α := M) ((e : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y) : M)
      ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y : M)
⊢ IsTensorProduct f
have this : TensorProduct.lift f = (↑e : M₁ ⊗[R] M₂ →ₗ[R] M)
Tactic: have : TensorProduct.lift f = e := by
    ext x y
    simp [he]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
⊢ hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)
have zero : HPow.hPow (β := ℕ) (hf.map hf i j) 0 = hf.map hf (HPow.hPow (β := ℕ) i 0) (HPow.hPow (β := ℕ) j 0)
Tactic: induction n with
  | zero => simp
  | succ n ih => simp only [pow_succ, ih, hf.map_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
zero : HPow.hPow (β := ℕ) (hf.map hf i j) 0 = hf.map hf (HPow.hPow (β := ℕ) i 0) (HPow.hPow (β := ℕ) j 0)
⊢ hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)
have succ : ∀ (n : ℕ) (ih : hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)),
  hf.map hf i j ^ (n + 1) = hf.map hf (i ^ (n + 1)) (j ^ (n + 1))
Tactic: induction n with
  | zero => simp
  | succ n ih => simp only [pow_succ, ih, hf.map_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
⊢ HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
have change : Eq (α := M₁ ⊗[R] M₂)
  ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
      (HSMul.hSMul (β := M₁₂) s ((hf.equiv.toAddEquiv.toEquiv : (a : M₁ ⊗[R] M₂) → M₁₂) (y ⊗ₜ[R] x) : M₁₂)) :
    M₁ ⊗[R] M₂)
  (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
Tactic: change hf.equiv.symm (s • _) = _
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        (HSMul.hSMul (β := M₁₂) s ((hf.equiv.toAddEquiv.toEquiv : (a : M₁ ⊗[R] M₂) → M₁₂) (y ⊗ₜ[R] x) : M₁₂)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
have dsimp : Eq (α := M₁ ⊗[R] M₂)
  ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
      (HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x : M₁₂)) :
    M₁ ⊗[R] M₂)
  (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        (HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x : M₁₂)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
have rw : Eq (α := M₁ ⊗[R] M₂)
  ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
      ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) (s • x)) :
    M₁ ⊗[R] M₂)
  (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
Tactic: rw [← map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this_1 : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂ ⊗[R] M₁
⊢ AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) x)
have zero : AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
    (HSMul.hSMul (β := M₂ ⊗[R] M₁) s 0) =
  HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
    (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) 0)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this_1 : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂ ⊗[R] M₁
zero :
  AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
      (HSMul.hSMul (β := M₂ ⊗[R] M₁) s 0) =
    HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) 0)
⊢ AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) x)
have tmul : ∀ (x : M₂) (y : M₁),
  AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
      (HSMul.hSMul (β := M₂ ⊗[R] M₁) s (x ⊗ₜ[R] y)) =
    HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (x ⊗ₜ[R] y))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R : Type u_9
S : Type u_10
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₁₂
inst_7 : AddCommMonoid M₂₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module S M₂
inst_11 : IsScalarTower R S M₂
inst_12 : Module R M₃
inst_13 : Module S M₃
inst_14 : IsScalarTower R S M₃
inst_15 : Module R M₁₂
inst_16 : Module S M₁₂
inst_17 : IsScalarTower R S M₁₂
inst_18 : Module R M₂₃
inst_19 : Module S M₂₃
inst_20 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁ ⊗[R] M₂₃)
    ((assocAux f hf g hg : (a : M₁₂ ⊗[S] M₃) → M₁ ⊗[R] M₂₃)
        ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x₁ : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x₂ ⊗ₜ[S] x₃) :
      M₁ ⊗[R] M₂₃)
    (x₁ ⊗ₜ[R] (((g : (a : M₂) → M₃ →ₗ[S] M₂₃) x₂ : M₃ →ₗ[S] M₂₃) : (a : M₃) → M₂₃) x₃ : M₁ ⊗[R] M₂₃)
have this : Eq (α := M₁ ⊗[R] M₂)
  ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂) ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x₁ : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x₂) :
    M₁ ⊗[R] M₂)
  (x₁ ⊗ₜ[R] x₂ : M₁ ⊗[R] M₂)
Tactic: have : hf.equiv.symm (f x₁ x₂) = x₁ ⊗ₜ x₂ := hf.equiv_symm_apply _ _
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂
y : M₃
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨x, rfl⟩ := hf.equiv.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁
z : M₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have this : HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z : M₁₂) =
  (((f : (a : M₁) → M₂ →ₗ[S] M₁₂) (t • x) : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z
Tactic: have : t • (f x) z = f (t • x) z := by simp