awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
p q : (i : ι) → κ i
⊢ Eq.{u_2 + 1} (α := R)
    ((((Basis.repr
                  (Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                    (b i).dualBasis) :
                (a : ⨂[R] (i : ι), Dual R (M i)) → ((i : ι) → κ i) →₀ R)
              ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
                  (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
                ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                      (b i).dualBasis :
                    (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
                  p)) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        q :
      R)
    ((((Basis.repr
                  (Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                    (b i).dualBasis) :
                (a : ⨂[R] (i : ι), Dual R (M i)) → ((i : ι) → κ i) →₀ R)
              ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
                ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                      (b i).dualBasis :
                    (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
                  p)) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        q :
      R)

Tactic:
simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Premises used: funext_iff, Fintype.prod_ite_zero, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual
Goal:
ι : Type u_1
R : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommRing R
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), Finite.{u_3 + 1} (κ i)
b : (i : ι) → Basis.{u_3, u_2, u_4} (κ i) R (M i)
this_1 : Fintype ι
this : (i : ι) → Fintype (κ i)
refine :
  ∀ (p : (i : ι) → κ i),
    Eq (α := ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
      ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
            (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
              (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
            p) :
        ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
      ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
          ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦ (b i).dualBasis :
              (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
            p) :
        ⨂[R] (i : ι), Dual.{u_2, u_4} R (M i))
refine₁ :
  ∀ (p q : (i : ι) → κ i),
    Eq.{u_2 + 1} (α := R)
      ((((Basis.repr
                    (Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                      (b i).dualBasis) :
                  (a : ⨂[R] (i : ι), Dual R (M i)) → ((i : ι) → κ i) →₀ R)
                ((dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) :
                    (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
                  ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                        (b i).dualBasis :
                      (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
                    p)) :
              ((i : ι) → κ i) →₀ R) :
            (a : (i : ι) → κ i) → R)
          q :
        R)
      ((((Basis.repr
                    (Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                      (b i).dualBasis) :
                  (a : ⨂[R] (i : ι), Dual R (M i)) → ((i : ι) → κ i) →₀ R)
                ((LinearMap.id : (a : ⨂[R] (i : ι), Dual R (M i)) → ⨂[R] (i : ι), Dual R (M i))
                  ((Basis.piTensorProduct (M := fun (i : ι) ↦ Dual.{u_2, u_4} R (M i)) (κ := κ) fun (i : ι) ↦
                        (b i).dualBasis :
                      (a : (i : ι) → κ i) → ⨂[R] (i : ι), Dual R (M i))
                    p)) :
              ((i : ι) → κ i) →₀ R) :
            (a : (i : ι) → κ i) → R)
          q :
        R)
⊢ dualDistribInvOfBasis (κ := κ) (M := M) b ∘ₗ dualDistrib (M := M) = LinearMap.id

Tactic:
classical
  refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext (fun p ↦ ?_)
  refine (Basis.piTensorProduct (fun i => (b i).dualBasis)).ext_elem (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Premises used: funext_iff, Fintype.prod_ite_zero, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommSemiring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (κ i)
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_6 : (i : ι) → DecidableEq (M i)
p : (i : ι) → κ i
m : (i : ι) → M i
⊢ Eq (α := ((i : ι) → κ i) →₀ ⨂[R] (i : ι), M i)
    ((ofFinsuppEquiv (κ := κ) (M := M) : (a : ⨂[R] (i : ι), κ i →₀ M i) → ((i : ι) → κ i) →₀ ⨂[R] (i : ι), M i)
      ((tprod R (s := fun (i : ι) ↦ Finsupp.{u_3, u_4} (κ i) (M i)) :
          (a : (i : ι) → κ i →₀ M i) → ⨂[R] (i : ι), κ i →₀ M i)
        fun (i : ι) ↦ Finsupp.single (p i) (m i)))
    (Finsupp.single p (⨂ₜ[R] (i : ι), m i))

Tactic:
simp [ofFinsuppEquiv]

Premises used: PiTensorProduct.ofFinsuppEquiv
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommSemiring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (κ i)
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_6 : (i : ι) → DecidableEq (M i)
f : (i : ι) → Finsupp.{u_3, u_4} (κ i) (M i)
p : (i : ι) → κ i
⊢ Eq (α := ⨂[R] (i : ι), M i)
    (((ofFinsuppEquiv (κ := κ) (M := M) : (a : ⨂[R] (i : ι), κ i →₀ M i) → ((i : ι) → κ i) →₀ ⨂[R] (i : ι), M i)
            ((tprod R (s := fun (i : ι) ↦ Finsupp.{u_3, u_4} (κ i) (M i)) :
                (a : (i : ι) → κ i →₀ M i) → ⨂[R] (i : ι), κ i →₀ M i)
              fun (i : ι) ↦ f i) :
          (a : (i : ι) → κ i) → ⨂[R] (i : ι), M i)
        p :
      ⨂[R] (i : ι), M i)
    (⨂ₜ[R] (i : ι), (f i : (a : κ i) → M i) (p i) : ⨂[R] (i : ι), M i)

Tactic:
simp [ofFinsuppEquiv]

Premises used: PiTensorProduct.ofFinsuppEquiv
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : ι → Type u_4
inst : CommSemiring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (κ i)
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_1, u_4} R (M i)
inst_6 : (i : ι) → DecidableEq (M i)
p : (i : ι) → κ i
m : (i : ι) → M i
⊢ Eq (α := ⨂[R] (i : ι), Finsupp.{u_3, u_4} (κ i) (M i))
    ((LinearEquiv.symm (ofFinsuppEquiv (κ := κ) (M := M)) :
          (a : ((i : ι) → κ i) →₀ ⨂[R] (i : ι), M i) → ⨂[R] (i : ι), κ i →₀ M i)
        (Finsupp.single p (⨂ₜ[R] (i : ι), m i)) :
      ⨂[R] (i : ι), Finsupp.{u_3, u_4} (κ i) (M i))
    ((tprod R (s := fun (i : ι) ↦ Finsupp.{u_3, u_4} (κ i) (M i)) :
          (a : (i : ι) → κ i →₀ M i) → ⨂[R] (i : ι), κ i →₀ M i)
        fun (i : ι) ↦ Finsupp.single (p i) (m i) :
      ⨂[R] (i : ι), Finsupp.{u_3, u_4} (κ i) (M i))

Tactic:
(LinearEquiv.symm_apply_eq _).2 (ofFinsuppEquiv_tprod_single _ _).symm

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, PiTensorProduct.ofFinsuppEquiv_tprod_single, Eq.symm
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
inst : CommSemiring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (κ i)
inst_4 : DecidableEq R
f : (i : ι) → Finsupp.{u_3, u_1} (κ i) R
p : (i : ι) → κ i
⊢ Eq.{u_1 + 1} (α := R)
    (((ofFinsuppEquiv' (κ := κ) : (a : ⨂[R] (i : ι), κ i →₀ R) → ((i : ι) → κ i) →₀ R)
            ((tprod R (s := fun (i : ι) ↦ Finsupp.{u_3, u_1} (κ i) R) :
                (a : (i : ι) → κ i →₀ R) → ⨂[R] (i : ι), κ i →₀ R)
              fun (i : ι) ↦ f i) :
          (a : (i : ι) → κ i) → R)
        p :
      R)
    (∏ i : ι, (f i : (a : κ i) → R) (p i) : R)

Tactic:
simp [ofFinsuppEquiv']

Premises used: PiTensorProduct.ofFinsuppEquiv'
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
Goal:
R : Type u_1
ι : Type u_2
κ : ι → Type u_3
inst : CommSemiring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (κ i)
inst_4 : DecidableEq R
p : (i : ι) → κ i
r : ι → R
⊢ Eq (α := ((i : ι) → κ i) →₀ R)
    ((ofFinsuppEquiv' (κ := κ) : (a : ⨂[R] (i : ι), κ i →₀ R) → ((i : ι) → κ i) →₀ R)
      ((tprod R (s := fun (i : ι) ↦ Finsupp.{u_3, u_1} (κ i) R) : (a : (i : ι) → κ i →₀ R) → ⨂[R] (i : ι), κ i →₀ R)
        fun (i : ι) ↦ Finsupp.single (p i) (r i)))
    (Finsupp.single p (∏ i : ι, r i))

Tactic:
simp [ofFinsuppEquiv']

Premises used: PiTensorProduct.ofFinsuppEquiv'
-- 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)
f : (i : ι) → s i
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) 0 f) 0

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_scalar _

Premises used: Quotient.sound', PiTensorProduct.Eqv.of_zero_scalar, AddConGen.Rel.of, PiTensorProduct.tprodCoeff, PiTensorProduct, AddCon.Quotient, 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)
z : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z f) 0

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero _ _ i hf

Premises used: Quotient.sound', AddConGen.Rel.of, PiTensorProduct.Eqv.of_zero, PiTensorProduct.tprodCoeff, PiTensorProduct, AddCon.Quotient, 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)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i m₁))
      (tprodCoeff R (s := s) z (update (β := s) f i m₂)) =
    tprodCoeff R (s := s) z (update (β := s) f i (m₁ + m₂))

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ (Eqv.of_add _ z f i m₁ m₂)

Premises used: Quotient.sound', Quotient.map₂, AddConGen.Rel.of, PiTensorProduct.tprodCoeff, PiTensorProduct.Eqv.of_add, PiTensorProduct, AddCon.Quotient, 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)
z₁ z₂ : R
f : (i : ι) → s i
⊢ HAdd.hAdd (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z₁ f) (tprodCoeff R (s := s) z₂ f) =
    tprodCoeff R (s := s) (z₁ + z₂) f

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ (Eqv.of_add_scalar z₁ z₂ f)

Premises used: Quotient.sound', Quotient.map₂, PiTensorProduct.Eqv.of_add_scalar, AddConGen.Rel.of, PiTensorProduct.tprodCoeff, PiTensorProduct, AddCon.Quotient, 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)
inst_3 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (r • f i)))
    (tprodCoeff R (s := s) (r * z) f)

Tactic:
Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _ _ _

Premises used: Quotient.sound', AddConGen.Rel.of, PiTensorProduct.tprodCoeff, PiTensorProduct, AddCon.Quotient, PiTensorProduct.Eqv.of_smul, AddCon.toQuotient
-- 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 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
rw : r • z = r • (1 * z)
rw₁ rw₂ : r • z = r • z
⊢ r • z = HSMul.hSMul (β := R) r 1 * z

Tactic:
rw [smul_mul_assoc, one_mul]

Premises used: smul_mul_assoc, one_mul
-- 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 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
⊢ r • z = HSMul.hSMul (β := R) r 1 * z

Tactic:
have h₁ : r • z = r • (1 : R) * z := by rw [smul_mul_assoc, one_mul]
-- 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 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
⊢ r • f i = HSMul.hSMul (β := R) r 1 • f i

Tactic:
have h₂ : r • f i = (r • (1 : R)) • f i := (smul_one_smul _ _ _).symm
-- 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 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
h₂ : r • f i = HSMul.hSMul (β := R) r 1 • f i
rw :
  Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (HSMul.hSMul (β := R) r 1 • f i)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1 * z) f)
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (r • f i)))
    (tprodCoeff R (s := s) (r • z) f)

Tactic:
rw [h₁, h₂]
-- 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 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
h₂ : r • f i = HSMul.hSMul (β := R) r 1 • f i
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (HSMul.hSMul (β := R) r 1 • f i)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1 * z) f)

Tactic:
smul_tprodCoeff_aux z f i _

Premises used: PiTensorProduct.smul_tprodCoeff_aux
-- 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 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst_4 : SMul R₁ R
inst_5 : IsScalarTower R₁ R R
inst_6 : SMul.{u_5, u_7} R₁ (s i)
inst_7 : IsScalarTower.{u_5, u_4, u_7} R₁ R (s i)
h₁ : r • z = HSMul.hSMul (β := R) r 1 * z
h₂ : r • f i = HSMul.hSMul (β := R) r 1 • f i
⊢ Eq (α := ⨂[R] (i : ι), s i) (tprodCoeff R (s := s) z (update (β := s) f i (HSMul.hSMul (β := R) r 1 • f i)))
    (tprodCoeff R (s := s) (HSMul.hSMul (β := R) r 1 * z) f)

Tactic:
exact smul_tprodCoeff_aux z f i _

Premises used: PiTensorProduct.smul_tprodCoeff_aux
-- 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 y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
r' : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ 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 (r', 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)
        0 :
      F)

Tactic:
simp [FreeAddMonoid.lift_eval_of, C0 r' f i hf]

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 y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
f : (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)
        (FreeAddMonoid.of (0, 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)
        0 :
      F)

Tactic:
simp [FreeAddMonoid.lift_eval_of, C0']

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_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 : ι
m₁ m₂ : 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)
        (FreeAddMonoid.of (z, update (β := s) f i m₁) + FreeAddMonoid.of (z, update (β := s) f i m₂)) :
      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 (m₁ + m₂))) :
      F)

Tactic:
simp [FreeAddMonoid.lift_eval_of, @C_add 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 y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
z₁ z₂ : R
f : (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)
        (FreeAddMonoid.of (z₁, f) + FreeAddMonoid.of (z₂, 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)
        (FreeAddMonoid.of (z₁ + z₂, f)) :
      F)

Tactic:
simp [FreeAddMonoid.lift_eval_of, C_add_scalar]

Premises used: FreeAddMonoid.lift_eval_of