awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
smul_tprod :
  ∀ (r : R) (f : (i : ι) → s i),
    motive
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i))
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R (s := s) r f)

Tactic:
simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod

Premises used: PiTensorProduct.tprodCoeff_eq_smul_tprod
-- 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
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R (s := s) r f)
⊢ motive z

Tactic:
PiTensorProduct.induction_on' z smul_tprod add

Premises used: PiTensorProduct.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
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R (s := s) r f)
⊢ motive z

Tactic:
exact PiTensorProduct.induction_on' z smul_tprod 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
⊢ φ₁ = φ₂

Tactic:
LinearMap.ext ?_

Premises used: LinearMap.ext
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
refine :
  ∀ (x : ⨂[R] (i : ι), s i),
    Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E)
⊢ φ₁ = φ₂

Tactic:
refine LinearMap.ext ?_

Premises used: LinearMap.ext
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
z x y : ⨂[R] (i : ι), s i
hx : Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E)
hy : Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
rw :
  HAdd.hAdd (α := E) (β := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    (φ₂ : (a : ⨂[R] (i : ι), s i) → E) (x + y)
rw₁ :
  HAdd.hAdd (α := E) (β := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
rw₂ :
  HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
rw₃ rw₄ :
  HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E) =
    HAdd.hAdd (α := E) (β := E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) y : E)
⊢ Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) (x + y) : E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) (x + y) : E)

Tactic:
rw [φ₁.map_add, φ₂.map_add, hx, hy]

Premises used: LinearMap.map_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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
refine :
  ∀ (z : ⨂[R] (i : ι), s i) (r : R) (f : (i : ι) → s i),
    Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
      ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
⊢ ∀ (x : ⨂[R] (i : ι), s i),
    Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) x : E) ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) x : E)

Tactic:
refine fun z ↦
    PiTensorProduct.induction_on' z ?_ fun {x y} hx hy ↦ by rw [φ₁.map_add, φ₂.map_add, hx, hy]
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
rw :
  HSMul.hSMul (β := E) r
      ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
        E) =
    HSMul.hSMul (β := E) r
      ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
        E)
⊢ Eq.{u_9 + 1} (α := E) ((φ₁ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r f) : E)

Tactic:
rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]

Premises used: PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMap.map_smul
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
h :
  Eq.{u_9 + 1} (α := E)
    ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
⊢ HSMul.hSMul (β := E) r
      ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
        E) =
    HSMul.hSMul (β := E) r
      ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
          ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
        E)

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)

Tactic:
MultilinearMap.congr_fun H f

Premises used: MultilinearMap.congr_fun
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (M₁ := s) (tprod R (s := s)) = φ₂.compMultilinearMap (M₁ := s) (tprod R (s := s))
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    ((φ₁ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
    ((φ₂ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)

Tactic:
exact MultilinearMap.congr_fun H f

Premises used: MultilinearMap.congr_fun
-- 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)
t : ⨂[R] (i : ι), s i
x : R
x_1 : (i : ι) → s i
⊢ Membership.mem (α := ⨂[R] (i : ι), s i) (γ := Set (⨂[R] (i : ι), s i))
    (Set.range (ι := (i : ι) → s i) (⇑(tprod R (s := s)) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i))
    ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) x_1 : ⨂[R] (i : ι), s i)

Tactic:
simp only [Set.mem_range, exists_apply_eq_apply]

Premises used: Set.mem_range, exists_apply_eq_apply
-- 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
φ : MultilinearMap R s E
z : R
f : (i : ι) → s i
i : ι
hf : f i = 0
simp_rw simp_rw₁ : HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E) = 0
simp_rw₂ : HSMul.hSMul (β := E) z 0 = 0
⊢ Eq.{u_9 + 1} (α := E)
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z, f)) 0

Tactic:
simp_rw [map_coord_zero φ i hf, smul_zero]

Premises used: smul_zero, MultilinearMap.map_coord_zero
-- 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
φ : MultilinearMap R s E
f : (i : ι) → s i
simp_rw simp_rw₁ : HSMul.hSMul.{u_4, u_9, u_9} (α := R) (β := E) 0 ((φ : (a : (i : ι) → s i) → E) f : E) = 0
⊢ Eq.{u_9 + 1} (α := E)
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (0, f)) 0

Tactic:
simp_rw [zero_smul]

Premises used: zero_smul
-- 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
φ : MultilinearMap R s E
inst_8 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
simp_rw simp_rw₁ :
  HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₁) : E) +
      HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₂) : E) =
    HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i (m₁ + m₂)) : E)
simp_rw₂ :
  z •
      HAdd.hAdd (α := E) (β := E) ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₁) : E)
        ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i m₂) : E) =
    HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) (update (β := s) f i (m₁ + m₂)) : E)
⊢ HAdd.hAdd (α := E)
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
        (z, update (β := s) f i m₁))
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
        (z, update (β := s) f i m₂)) =
    (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
      (z, update (β := s) f i (m₁ + m₂))

Tactic:
simp_rw [← smul_add, φ.map_update_add]

Premises used: MultilinearMap.map_update_add, 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
φ : MultilinearMap R s E
z₁ z₂ : R
f : (i : ι) → s i
rw rw₁ :
  HSMul.hSMul (β := E) ((z₁, f).1 + (z₂, f).1) ((φ : (a : (i : ι) → s i) → E) (z₁, f).2 : E) =
    (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₁ + z₂, f)
⊢ HAdd.hAdd (α := E)
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₁, f))
      ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₂, f)) =
    (fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (z₁ + z₂, f)

Tactic:
rw [← add_smul]

Premises used: add_smul
-- 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
φ : MultilinearMap R s E
inst_8 : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R
⊢ Eq.{u_9 + 1} (α := E)
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
      (z, update (β := s) f i (r • f i)))
    ((fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E)) (r * z, f))

Tactic:
simp [φ.map_update_smul, smul_smul, mul_comm]

Premises used: MultilinearMap.map_update_smul, smul_smul, mul_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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
f : (i : ι) → s i
simp :
  Eq.{u_9 + 1} (α := E)
    ((AddCon.lift (addConGen (Eqv R s))
            ((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
              fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
            ⋯ :
          (a : ⨂[R] (i : ι), s i) → E)
        (↑(FreeAddMonoid.of (1, f)) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)
⊢ Eq.{u_9 + 1} (α := E)
    ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) f : ⨂[R] (i : ι), s i) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)

Tactic:
simp only [liftAux, liftAddHom, tprod_eq_tprodCoeff_one, tprodCoeff, AddCon.coe_mk']

Premises used: PiTensorProduct.liftAux, AddCon.coe_mk', PiTensorProduct.tprod_eq_tprodCoeff_one, PiTensorProduct.liftAddHom, PiTensorProduct.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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
f : (i : ι) → s i
conv_lhs :
  Eq.{u_9 + 1} (α := E)
    (((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
            fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → E)
        (FreeAddMonoid.of (1, f)) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)
⊢ Eq.{u_9 + 1} (α := E)
    ((AddCon.lift (addConGen (Eqv R s))
            ((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
              fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E))
            ⋯ :
          (a : ⨂[R] (i : ι), s i) → E)
        (↑(FreeAddMonoid.of (1, f)) : (addConGen (Eqv R fun (i : ι) ↦ s i)).Quotient) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)

Tactic:
conv_lhs => apply AddCon.lift_coe

Premises used: AddCon.lift_coe
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ Eq.{u_9 + 1} (α := E)
    (((FreeAddMonoid.lift : (a : R × ((i : ι) → s i) → E) → FreeAddMonoid (R × ((i : ι) → s i)) →+ E)
            fun (p : R × ((i : ι) → s i)) ↦ HSMul.hSMul (β := E) p.1 ((φ : (a : (i : ι) → s i) → E) p.2 : E) :
          (a : FreeAddMonoid (R × ((i : ι) → s i))) → E)
        (FreeAddMonoid.of (1, f)) :
      E)
    ((φ : (a : (i : ι) → s i) → E) f : E)

Tactic:
simp
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
z : R
f : (i : ι) → s i
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) =
    HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • x) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) x : E)

Tactic:
PiTensorProduct.induction_on' x ?_ ?_

Premises used: PiTensorProduct.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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
refine_1 :
  ∀ (r_1 : R) (f : (i : ι) → s i),
    (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
        (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) r_1 f)) =
      HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) r_1 f) : E)
refine_2 :
  ∀ (x y : ⨂[R] (i : ι), s i),
    (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • x) =
        HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) x : E) →
      (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • y) =
          HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) y : E) →
        (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • (x + y)) =
          HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (x + y) : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (r • x) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) x : E)

Tactic:
refine PiTensorProduct.induction_on' x ?_ ?_
-- 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)
E : Type u_9
inst_3 : AddCommMonoid E
inst_4 : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
z : R
f : (i : ι) → s i
refine_1 :
  (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) (r • z) f) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
refine_1₁ :
  HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)
refine_1₂ :
  HSMul.hSMul (β := E) (r • z) ((φ : (a : (i : ι) → s i) → E) f : E) =
    r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E)
refine_1₃ refine_1₄ :
  r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E) =
    r • HSMul.hSMul (β := E) z ((φ : (a : (i : ι) → s i) → E) f : E)
⊢ (liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E)
      (HSMul.hSMul (β := ⨂[R] (i : ι), s i) r (tprodCoeff R (s := s) z f)) =
    HSMul.hSMul (β := E) r ((liftAux (s := s) φ : (a : ⨂[R] (i : ι), s i) → E) (tprodCoeff R (s := s) z f) : E)

Tactic:
rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]

Premises used: smul_assoc, PiTensorProduct.liftAux_tprodCoeff, PiTensorProduct.smul_tprodCoeff'