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 : 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
simp_rw₁ : r'' • r' • z + r' • r'' • y = r'' • r' • z + r'' • r' • y
⊢ r' • r'' • (z + y) = r'' • r' • (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 : SMul R₁ R₂
inst_15 : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), s i) (r' • 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_assoc]

Premises used: smul_assoc, 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
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
simp_rw₁ : r' • r'' • z + (r' • r'') • y = r' • r'' • z + r' • r'' • y
⊢ (r' • r'') • (z + y) = r' • r'' • (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 : 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)
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)
⊢ 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)

Tactic:
simp_rw [smul_tprodCoeff', add_smul, add_tprodCoeff']

Premises used: add_smul, PiTensorProduct.smul_tprodCoeff', 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 : 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)
simp_rw₂ : r • x + r' • x + (r • y + r' • y) = r • x + r • y + (r' • x + r' • y)
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)

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

Premises used: add_add_add_comm, 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 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
simp_rw : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) (HSMul.hSMul.{u_5, u_4, u_4} (α := R₁) 0 r) f) 0
simp_rw₁ : Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 0 f) 0
⊢ HSMul.hSMul (α := R₁) (β := ⨂[R] (i : ι), s i) 0 (tprodCoeff R (s := s) r f) = 0

Tactic:
simp_rw [smul_tprodCoeff', zero_smul, zero_tprodCoeff]

Premises used: zero_smul, PiTensorProduct.smul_tprodCoeff', 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 : Semiring R₁
inst_9 : Module R₁ R
inst_10 : SMulCommClass R₁ R R
x_1 x y : ⨂[R] (i : ι), s i
ihx : HSMul.hSMul (α := R₁) 0 x = 0
ihy : HSMul.hSMul (α := R₁) 0 y = 0
simp_rw : HSMul.hSMul (α := R₁) 0 x + HSMul.hSMul (α := R₁) 0 y = 0
simp_rw₁ : 0 + HSMul.hSMul (α := R₁) 0 y = 0
simp_rw₂ : HAdd.hAdd (α := ⨂[R] (i : ι), s i) 0 0 = 0
⊢ HSMul.hSMul (α := R₁) 0 (x + y) = 0

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

Premises used: add_zero, 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
⊢ SMulCommClass R R (⨂[R] (i : ι), s i)

Tactic:
PiTensorProduct.smulCommClass'

Premises used: PiTensorProduct.smulCommClass'
-- 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
⊢ IsScalarTower R R (⨂[R] (i : ι), s i)

Tactic:
PiTensorProduct.isScalarTower'

Premises used: PiTensorProduct.isScalarTower'
-- 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
x_1 : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
rw :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1) (update (β := s) f i x))
rw₁ :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) 1 (update (β := s) (update (β := s) f i x) i (r • update (β := s) f i x i)))
rw₂ :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) 1 (update (β := s) f i (r • update (β := s) f i x i)))
rw₃ rw₄ :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
    (tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)))
⊢ tprodCoeff R (s := s) 1 (update (β := s) f i (r • x)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) 1 (update (β := s) f i x))

Tactic:
rw [smul_tprodCoeff', ← smul_tprodCoeff (1 : R) _ i, update_idem, update_self]

Premises used: Function.update_idem, PiTensorProduct.smul_tprodCoeff', PiTensorProduct.smul_tprodCoeff, Function.update_self, OfNat.ofNat
-- 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)
⊢ Eq (α := (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i)
    (tprodCoeff R (s := s) 1)

Tactic:
rfl

Premises used: PiTensorProduct.tprodCoeff, AddCon.toQuotient, rfl
-- 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)
z : R
f : (i : ι) → s i
⊢ z = HSMul.hSMul (β := R) z 1

Tactic:
simp only [mul_one, smul_eq_mul]

Premises used: smul_eq_mul, mul_one
-- 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)
z : R
f : (i : ι) → s i
⊢ z = HSMul.hSMul (β := R) z 1

Tactic:
have : z = z • (1 : R) := by simp only [mul_one, smul_eq_mul]
-- 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)
z : R
f : (i : ι) → s i
this : z = HSMul.hSMul (β := R) z 1
rw : tprodCoeff R (s := s) (HSMul.hSMul (β := R) z 1) f
| tprodCoeff R (s := s) z f

Tactic:
rw [this]
-- 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)
z : R
f : (i : ι) → s i
this : z = HSMul.hSMul (β := R) z 1
conv_lhs :
  tprodCoeff R (s := s) (HSMul.hSMul (β := R) z 1) f =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) z
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)
⊢ tprodCoeff R (s := s) z f =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) z
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)

Tactic:
conv_lhs => rw [this]
-- 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)
z : R
f : (i : ι) → s i
this : z = HSMul.hSMul (β := R) z 1
⊢ tprodCoeff R (s := s) (HSMul.hSMul (β := R) z 1) f =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) z
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i)

Tactic:
rfl
-- 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)
⊢ Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑0 : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))

Tactic:
rfl
-- 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)
b : R × ((i : ι) → s i)
a : FreeAddMonoid (R × ((i : ι) → s i))
ih :
  Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑a : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) a)))
add_of :
  (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient) =
    HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) b.1 fun (i : ι) ↦ b.2 i)
      (↑a : (addConGen (Eqv R s)).Quotient)
⊢ Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          (FreeAddMonoid.of b + a))))

Tactic:
rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod]

Premises used: List.map_cons, PiTensorProduct.tprodCoeff_eq_smul_tprod, FreeAddMonoid.toList_of_add, List.sum_cons
-- 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)
b : R × ((i : ι) → s i)
a : FreeAddMonoid (R × ((i : ι) → s i))
ih :
  Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑a : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) a)))
⊢ (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient) =
    HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) b.1 fun (i : ι) ↦ b.2 i)
      (↑a : (addConGen (Eqv R s)).Quotient)

Tactic:
rfl
-- 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)
p : FreeAddMonoid (R × ((i : ι) → s i))
zero :
  Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑0 : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
add_of :
  ∀ (b : R × ((i : ι) → s i)) (a : FreeAddMonoid (R × ((i : ι) → s i)))
    (ih :
      Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑a : (addConGen (Eqv R s)).Quotient)
        (List.sum
          (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
            ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) a)))),
    Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑(FreeAddMonoid.of b + a) : (addConGen (Eqv R s)).Quotient)
      (List.sum
        (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
            (FreeAddMonoid.of b + a))))
⊢ Eq (α := AddCon.Quotient (addConGen (Eqv R s))) (↑p : (addConGen (Eqv R s)).Quotient)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)))

Tactic:
induction p using FreeAddMonoid.inductionOn' with
  | zero => rfl
  | add_of b a ih =>
    rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih, ← tprodCoeff_eq_smul_tprod]
    rfl

Premises used: List.map_cons, PiTensorProduct.tprodCoeff_eq_smul_tprod, FreeAddMonoid.toList_of_add, List.sum_cons
-- 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)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ p ∈ x.lifts (s := s) ↔
    List.sum
        (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)) =
      x

Tactic:
simp only [lifts, Set.mem_setOf_eq, FreeAddMonoid.toPiTensorProduct]

Premises used: FreeAddMonoid.toPiTensorProduct, PiTensorProduct.lifts, Set.mem_setOf_eq
-- 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)
x : ⨂[R] (i : ι), s i
existsi :
  Quot.out (r :=
      (⇑(addConGen (Eqv R fun (i : ι) ↦ s i)).toSetoid :
        FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i)) →
          FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i)) → Prop))
      x ∈
    x.lifts (s := s)
⊢ x.lifts (s := s).Nonempty

Tactic:
existsi Quot.out x

Premises used: Quot.out
-- 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)
x : ⨂[R] (i : ι), s i
⊢ Quot.out (r :=
      (⇑(addConGen (Eqv R fun (i : ι) ↦ s i)).toSetoid :
        FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i)) →
          FreeAddMonoid (R × ((i : ι) → (fun (i : ι) ↦ s i) i)) → Prop))
      x ∈
    x.lifts (s := s)

Tactic:
simp [lifts, ← AddCon.quot_mk_eq_coe]

Premises used: PiTensorProduct.lifts, AddCon.quot_mk_eq_coe
-- 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
x : ⨂[R] (i : ι), s i
⊢ Nonempty (↑(x.lifts (s := s)) : Type (max (max u_1 u_4) u_7))

Tactic:
nonempty_subtype.mpr (nonempty_lifts x)

Premises used: Iff.mpr, nonempty_subtype, PiTensorProduct.nonempty_lifts
-- 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)
rw :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) 0)))
    0
rw₁ :
  Eq (α := ⨂[R] (i : ι), s i)
    (List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i)) []))
    0
rw₂ : Eq (α := ⨂[R] (i : ι), s i) (List.sum []) 0
rw₃ rw₄ : Eq (α := ⨂[R] (i : ι), s i) 0 0
⊢ Membership.mem (γ := Set (FreeAddMonoid (R × ((i : ι) → s i)))) (lifts (s := s) 0) 0

Tactic:
rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]

Premises used: List.sum_nil, FreeAddMonoid.toList_zero, PiTensorProduct.mem_lifts_iff, List.map_nil
-- 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)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts (s := s)
hq : q ∈ y.lifts (s := s)
rw : x + (↑q : (addConGen (Eqv R s)).Quotient) = x + y
rw₁ rw₂ : x + y = x + y
⊢ HAdd.hAdd (α := AddCon.Quotient (addConGen (Eqv R s))) (↑p : (addConGen (Eqv R s)).Quotient)
      (↑q : (addConGen (Eqv R s)).Quotient) =
    x + y

Tactic:
rw [hp, hq]
-- 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)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h :
  List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)) =
    x
a : R
rw :
  List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          ((FreeAddMonoid.map fun (y : R × ((i : ι) → s i)) ↦ (a * y.1, y.2) :
              (a : FreeAddMonoid (R × ((i : ι) → s i))) → FreeAddMonoid (R × ((i : ι) → s i)))
            p))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) a
      (List.sum
        (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)))
⊢ List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          ((FreeAddMonoid.map fun (y : R × ((i : ι) → s i)) ↦ (a * y.1, y.2) :
              (a : FreeAddMonoid (R × ((i : ι) → s i))) → FreeAddMonoid (R × ((i : ι) → s i)))
            p))) =
    a • x

Tactic:
rw [← 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)
x : ⨂[R] (i : ι), s i
p : FreeAddMonoid (R × ((i : ι) → s i))
h :
  List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)) =
    x
a : R
⊢ List.sum
      (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i)))
          ((FreeAddMonoid.map fun (y : R × ((i : ι) → s i)) ↦ (a * y.1, y.2) :
              (a : FreeAddMonoid (R × ((i : ι) → s i))) → FreeAddMonoid (R × ((i : ι) → s i)))
            p))) =
    HSMul.hSMul (β := ⨂[R] (i : ι), s i) a
      (List.sum
        (List.map (fun (x : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := ⨂[R] (i : ι), s i) x.1 (⨂ₜ[R] (i : ι), x.2 i))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (R × ((i : ι) → s i))) → List (R × ((i : ι) → s i))) p)))

Tactic:
simp [Function.comp_def, mul_smul, List.smul_sum]

Premises used: Function.comp_def, List.smul_sum, SemigroupAction.mul_smul