awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst_1 : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (s i)
inst_3 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_4 : AddCommMonoid M
inst_5 : Module R M
E : Type u_9
inst_6 : AddCommMonoid E
inst_7 : Module R E
F : Type u_10
inst_8 : 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 : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R),
    φ (r, update (β := s) f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
inst : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r' : R
⊢ 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)
        (FreeAddMonoid.of (z, update (β := s) f i (r' • f i))) :
      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)
        (FreeAddMonoid.of (r' * z, f)) :
      F)

Tactic:
simp [FreeAddMonoid.lift_eval_of, @C_smul inst]

Premises used: FreeAddMonoid.lift_eval_of
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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))
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)
⊢ 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)

Tactic:
simp_rw [map_add, add_comm]

Premises used: map_add, add_comm
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
have : ∀ (h₁ : motive (PiTensorProduct.tprodCoeff R (s := s) 0 0)), motive 0
⊢ motive 0

Tactic:
have h₁ := tprodCoeff 0 0
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h₁ : motive 0), motive 0
⊢ motive 0

Tactic:
rwa [zero_tprodCoeff] at h₁

Premises used: PiTensorProduct.zero_tprodCoeff
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
have : ∀ (C0 : motive 0), motive z
⊢ motive z

Tactic:
have C0 : motive 0 := by
    have h₁ := tprodCoeff 0 0
    rwa [zero_tprodCoeff] at h₁
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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

Tactic:
AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 ?_

Premises used: AddCon.induction_on
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
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)
⊢ motive z

Tactic:
refine AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 ?_
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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))
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))
⊢ ∀ (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:
simp_rw [AddCon.coe_add]

Premises used: AddCon.coe_add
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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))

Tactic:
fun f y ih ↦ add _ _ ?_ ih

Premises used: FreeAddMonoid.of, AddCon.toQuotient
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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))
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)
⊢ ∀ (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:
refine fun f y ih ↦ add _ _ ?_ ih
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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))
f : R × ((i : ι) → s i)
y : FreeAddMonoid (R × ((i : ι) → s i))
ih : motive (↑y : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient)
⊢ motive (PiTensorProduct.tprodCoeff R (s := s) f.1 f.2)

Tactic:
tprodCoeff f.1 f.2

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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))
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:
convert! tprodCoeff f.1 f.2

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
simp_rw simp_rw₁ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (r • r') f) 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

Tactic:
simp_rw [zero_tprodCoeff' _ f i hf]

Premises used: PiTensorProduct.zero_tprodCoeff'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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₁
f : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i)) (0, f)) 0

Tactic:
simp [zero_tprodCoeff]

Premises used: PiTensorProduct.zero_tprodCoeff
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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₁
inst_14 : DecidableEq ι
r' : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ HAdd.hAdd (α := ⨂[R] (i : ι), s i)
      ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i))
        (r', update (β := s) f i m₁))
      ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i))
        (r', update (β := s) f i m₂)) =
    (fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i))
      (r', update (β := s) f i (m₁ + m₂))

Tactic:
simp [add_tprodCoeff]

Premises used: PiTensorProduct.add_tprodCoeff
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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'' : R
f : (i : ι) → s i
⊢ HAdd.hAdd (α := ⨂[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))
      ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i)) (r'', f)) =
    (fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i)) (r' + r'', f)

Tactic:
simp [add_tprodCoeff']

Premises used: PiTensorProduct.add_tprodCoeff'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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₁
inst_14 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r' : R
⊢ Eq (α := ⨂[R] (i : ι), s i)
    ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i))
      (z, update (β := s) f i (r' • f i)))
    ((fun (f : R × ((i : ι) → s i)) ↦ (tprodCoeff R (s := s) (r • f.1) f.2 : ⨂[R] (i : ι), s i)) (r' * z, f))

Tactic:
simp [smul_tprodCoeff, mul_smul_comm]

Premises used: PiTensorProduct.smul_tprodCoeff, mul_smul_comm
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : Monoid R₁
inst_4 : DistribMulAction R₁ R
inst_5 : SMulCommClass R₁ R R
r : R₁
z : R
f : (i : ι) → s i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) z f) = tprodCoeff R (s := s) (r • z) f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, PiTensorProduct.tprodCoeff, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
inst_3 : Monoid R₁
inst_4 : DistribMulAction R₁ R
inst_5 : SMulCommClass R₁ R R
r : R₁
x y : ⨂[R] (i : ι), s i
⊢ r • (x + y) = r • x + r • y

Tactic:
map_add _ _ _

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ⨂[R] (i : ι), s i
r'' : R
f : (i : ι) → s i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) (r * r') (tprodCoeff R (s := s) r'' f) =
    r • HSMul.hSMul (β := ⨂[R] (i : ι), s i) r' (tprodCoeff R (s := s) r'' f)

Tactic:
simp [smul_tprodCoeff', smul_smul]

Premises used: smul_smul, PiTensorProduct.smul_tprodCoeff'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
simp_rw₁ : r • r' • x + (r * r') • y = r • r' • x + r • r' • y
⊢ (r * r') • (x + y) = r • r' • (x + y)

Tactic:
simp_rw [PiTensorProduct.smul_add, ihx, ihy]

Premises used: PiTensorProduct.smul_add
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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)
rw₁ rw₂ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 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

Tactic:
rw [smul_tprodCoeff', one_smul]

Premises used: one_smul, PiTensorProduct.smul_tprodCoeff'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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
simp_rw₁ : z + HSMul.hSMul (α := R₁) 1 y = z + y
⊢ HSMul.hSMul (α := R₁) 1 (z + y) = z + y

Tactic:
simp_rw [PiTensorProduct.smul_add, ihz, ihy]

Premises used: PiTensorProduct.smul_add
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
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 : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ r' • HSMul.hSMul (β := ⨂[R] (i : ι), s i) r'' (tprodCoeff R (s := s) xr xf) =
    r'' • HSMul.hSMul (β := ⨂[R] (i : ι), s i) r' (tprodCoeff R (s := s) xr xf)

Tactic:
simp only [smul_tprodCoeff', smul_comm]

Premises used: PiTensorProduct.smul_tprodCoeff', SMulCommClass.smul_comm