awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update (β := s) f i m₁) + φ (r, update (β := s) f i m₂) = φ (r, update (β := s) f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst_8 : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R),
    φ (r, update (β := s) f i (r' • f i)) = φ (r' * r, f)
x_1 y_1 : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x_1 y_1
x y : FreeAddMonoid (R × ((i : ι) → s i))
⊢ Eq.{u_10 + 1} (α := F)
    ((((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → F) → FreeAddMonoid (R × ((i : ι) → s i)) →+ F) φ :
            FreeAddMonoid (R × ((i : ι) → s i)) →+ F) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → F)
        (x + y) :
      F)
    ((((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → F) → FreeAddMonoid (R × ((i : ι) → s i)) →+ F) φ :
            FreeAddMonoid (R × ((i : ι) → s i)) →+ F) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → F)
        (y + x) :
      F)
have simp_rw : HAdd.hAdd (α := F) (β := F)
    ((((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → F) → FreeAddMonoid (R × ((i : ι) → s i)) →+ F) φ :
            FreeAddMonoid (R × ((i : ι) → s i)) →+ F) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → F)
        x :
      F)
    ((((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → F) → FreeAddMonoid (R × ((i : ι) → s i)) →+ F) φ :
            FreeAddMonoid (R × ((i : ι) → s i)) →+ F) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → F)
        y :
      F) =
  HAdd.hAdd (α := F) (β := F)
    ((((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → F) → FreeAddMonoid (R × ((i : ι) → s i)) →+ F) φ :
            FreeAddMonoid (R × ((i : ι) → s i)) →+ F) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → F)
        y :
      F)
    ((((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → F) → FreeAddMonoid (R × ((i : ι) → s i)) →+ F) φ :
            FreeAddMonoid (R × ((i : ι) → s i)) →+ F) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → F)
        x :
      F)
Tactic: simp_rw [map_add, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R (s := s) r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive 0
have have : ∀ (h₁ : motive (PiTensorProduct.tprodCoeff R (s := s) 0 0)), motive 0
Tactic: have h₁ := tprodCoeff 0 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R (s := s) r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
h₁ : motive (PiTensorProduct.tprodCoeff R (s := s) 0 0)
⊢ motive 0
have rwa : ∀ (h₁ : motive 0), motive 0
Tactic: rwa [zero_tprodCoeff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R (s := s) r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive z
have have : ∀ (C0 : motive 0), motive z
Tactic: have C0 : motive 0 := by
    have h₁ := tprodCoeff 0 0
    rwa [zero_tprodCoeff] at h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R (s := s) r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
C0 : motive 0
⊢ motive z
have refine : ∀ (x : FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i))) (x : R × ((i : ι) → (fun (i : ι) ↦ s i) i))
  (xs : FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i))),
  motive (↑xs : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) →
    motive (↑(FreeAddMonoid.of x + xs) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)
Tactic: refine AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R (s := s) r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
C0 : motive 0
x : FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i))
⊢ ∀ (x : R × ((i : ι) → (fun (i : ι) ↦ s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i))),
    motive (↑xs : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) →
      motive (↑(FreeAddMonoid.of x + xs) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)
have simp_rw : ∀ (x : R × ((i : ι) → s i)) (xs : FreeAddMonoid (R × ((i : ι) → s i))),
  motive (↑xs : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) →
    motive
      (HAdd.hAdd (α := AddCon.Quotient (M := FreeAddMonoid (R × ((i : ι) → s i))) (addConGen (Eqv R fun (i : ι) ↦ s i)))
        (↑(FreeAddMonoid.of x) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)
        (↑xs : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient))
Tactic: simp_rw [AddCon.coe_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R (s := s) r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
C0 : motive 0
x : FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i))
⊢ ∀ (x : R × ((i : ι) → s i)) (xs : FreeAddMonoid (R × ((i : ι) → s i))),
    motive (↑xs : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) →
      motive
        (HAdd.hAdd (α :=
          AddCon.Quotient (M := FreeAddMonoid (R × ((i : ι) → s i))) (addConGen (Eqv R fun (i : ι) ↦ s i)))
          (↑(FreeAddMonoid.of x) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)
          (↑xs : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient))
have refine : ∀ (f : R × ((i : ι) → s i)) (y : FreeAddMonoid (R × ((i : ι) → s i)))
  (ih : motive (↑y : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)),
  motive (↑(FreeAddMonoid.of f) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)
Tactic: refine fun f y ih ↦ add _ _ ?_ ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
r : R₁
r' : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i)) (r', f)) 0
have simp_rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (r • r') f) 0
Tactic: simp_rw [zero_tprodCoeff' _ f i hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
r r' : R₁
x_1 x y : ⨂[R] (i : ι), s i
ihx : (r * r') • x = r • r' • x
ihy : (r * r') • y = r • r' • y
⊢ (r * r') • (x + y) = r • r' • (x + y)
have simp_rw : (r * r') • x + (r * r') • y = r • r' • x + r • r' • y
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
r r' : R₁
x_1 x y : ⨂[R] (i : ι), s i
ihx : (r * r') • x = r • r' • x
ihy : (r * r') • y = r • r' • y
simp_rw : (r * r') • x + (r * r') • y = r • r' • x + r • r' • y
⊢ (r * r') • (x + y) = r • r' • (x + y)
have simp_rw₁ : r • r' • x + (r * r') • y = r • r' • x + r • r' • y
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ HSMul.hSMul (α := R₁) (β := ⨂[R] (i : ι), s i) 1 (tprodCoeff R (s := s) r f) = tprodCoeff R (s := s) r f
have rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (HSMul.hSMul.{u_5, u_4, u_4} (α := R₁) 1 r) f)
  (tprodCoeff R (s := s) r f)
Tactic: rw [smul_tprodCoeff', one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
rw :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (HSMul.hSMul.{u_5, u_4, u_4} (α := R₁) 1 r) f)
    (tprodCoeff R (s := s) r f)
⊢ HSMul.hSMul (α := R₁) (β := ⨂[R] (i : ι), s i) 1 (tprodCoeff R (s := s) r f) = tprodCoeff R (s := s) r f
have rw₁ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) r f) (tprodCoeff R (s := s) r f)
Tactic: rw [smul_tprodCoeff', one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : HSMul.hSMul (α := R₁) 1 z = z
ihy : HSMul.hSMul (α := R₁) 1 y = y
⊢ HSMul.hSMul (α := R₁) 1 (z + y) = z + y
have simp_rw : HSMul.hSMul (α := R₁) 1 z + HSMul.hSMul (α := R₁) 1 y = z + y
Tactic: simp_rw [PiTensorProduct.smul_add, ihz, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : HSMul.hSMul (α := R₁) 1 z = z
ihy : HSMul.hSMul (α := R₁) 1 y = y
simp_rw : HSMul.hSMul (α := R₁) 1 z + HSMul.hSMul (α := R₁) 1 y = z + y
⊢ HSMul.hSMul (α := R₁) 1 (z + y) = z + y
have simp_rw₁ : z + HSMul.hSMul (α := R₁) 1 y = z + y
Tactic: simp_rw [PiTensorProduct.smul_add, ihz, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
inst_14 : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
⊢ r' • r'' • (z + y) = r'' • r' • (z + y)
have simp_rw : r' • r'' • z + r' • r'' • y = r'' • r' • z + r'' • r' • y
Tactic: simp_rw [PiTensorProduct.smul_add, ihz, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
inst_14 : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
simp_rw : r' • r'' • z + r' • r'' • y = r'' • r' • z + r'' • r' • y
⊢ r' • r'' • (z + y) = r'' • r' • (z + y)
have simp_rw₁ : r'' • r' • z + r' • r'' • y = r'' • r' • z + r'' • r' • y
Tactic: simp_rw [PiTensorProduct.smul_add, ihz, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
inst_14 : SMul R₁ R₂
inst_15 : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
⊢ (r' • r'') • (z + y) = r' • r'' • (z + y)
have simp_rw : (r' • r'') • z + (r' • r'') • y = r' • r'' • z + r' • r'' • y
Tactic: simp_rw [PiTensorProduct.smul_add, ihz, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Monoid R₁
inst_9 : DistribMulAction R₁ R
inst_10 : SMulCommClass R₁ R R
inst_11 : Monoid R₂
inst_12 : DistribMulAction R₂ R
inst_13 : SMulCommClass R₂ R R
inst_14 : SMul R₁ R₂
inst_15 : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
simp_rw : (r' • r'') • z + (r' • r'') • y = r' • r'' • z + r' • r'' • y
⊢ (r' • r'') • (z + y) = r' • r'' • (z + y)
have simp_rw₁ : r' • r'' • z + (r' • r'') • y = r' • r'' • z + r' • r'' • y
Tactic: simp_rw [PiTensorProduct.smul_add, ihz, ihy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
r_1 r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) (r_1 + r') (tprodCoeff R (s := s) r f) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r_1 (tprodCoeff R (s := s) r f) +
      HSMul.hSMul (β := ⨂[R] (i : ι), s i) r' (tprodCoeff R (s := s) r f)
have simp_rw : tprodCoeff R (s := s) ((r_1 + r') • r) f =
  HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (r_1 • r) f) (tprodCoeff R (s := s) (r' • r) f)
Tactic: simp_rw [smul_tprodCoeff', add_smul, add_tprodCoeff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
r_1 r' : R₁
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
simp_rw :
  tprodCoeff R (s := s) ((r_1 + r') • r) f =
    HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (r_1 • r) f) (tprodCoeff R (s := s) (r' • r) f)
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) (r_1 + r') (tprodCoeff R (s := s) r f) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r_1 (tprodCoeff R (s := s) r f) +
      HSMul.hSMul (β := ⨂[R] (i : ι), s i) r' (tprodCoeff R (s := s) r f)
have simp_rw₁ : tprodCoeff R (s := s) (r_1 • r + r' • r) f =
  HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (r_1 • r) f) (tprodCoeff R (s := s) (r' • r) f)
Tactic: simp_rw [smul_tprodCoeff', add_smul, add_tprodCoeff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
r r' : R₁
x_1 x y : ⨂[R] (i : ι), s i
ihx : (r + r') • x = r • x + r' • x
ihy : (r + r') • y = r • y + r' • y
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)
have simp_rw : (r + r') • x + (r + r') • y = r • x + r • y + (r' • x + r' • y)
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_add_add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
r r' : R₁
x_1 x y : ⨂[R] (i : ι), s i
ihx : (r + r') • x = r • x + r' • x
ihy : (r + r') • y = r • y + r' • y
simp_rw : (r + r') • x + (r + r') • y = r • x + r • y + (r' • x + r' • y)
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)
have simp_rw₁ : r • x + r' • x + (r + r') • y = r • x + r • y + (r' • x + r' • y)
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_add_add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
r r' : R₁
x_1 x y : ⨂[R] (i : ι), s i
ihx : (r + r') • x = r • x + r' • x
ihy : (r + r') • y = r • y + r' • y
simp_rw : (r + r') • x + (r + r') • y = r • x + r • y + (r' • x + r' • y)
simp_rw₁ : r • x + r' • x + (r + r') • y = r • x + r • y + (r' • x + r' • y)
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)
have simp_rw₂ : r • x + r' • x + (r • y + r' • y) = r • x + r • y + (r' • x + r' • y)
Tactic: simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_add_add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
inst_8 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ HSMul.hSMul (α := R₁) (β := ⨂[R] (i : ι), s i) 0 (tprodCoeff R (s := s) r f) = 0
have simp_rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (HSMul.hSMul.{u_5, u_4, u_4} (α := R₁) 0 r) f) 0
Tactic: simp_rw [smul_tprodCoeff', zero_smul, zero_tprodCoeff]