ι : Type u_1
ι₂ : Type ?u.228081
ι₃ : Type ?u.228084
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.228093
R₂ : Type ?u.228096
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.228286
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.228420
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.228554
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R z f = z • ↑(tprod R) f
ι : Type u_1
ι₂ : Type ?u.228081
ι₃ : Type ?u.228084
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.228093
R₂ : Type ?u.228096
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.228286
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.228420
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.228554
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
⊢ tprodCoeff R z f = z • ↑(tprod R) f
have : z = z • (1 : R) := by simp only [mul_one, Algebra.id.smul_eq_mul]
no goals
ι : Type u_1
ι₂ : Type ?u.228081
ι₃ : Type ?u.228084
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.228093
R₂ : Type ?u.228096
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.228286
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.228420
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.228554
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
this : z = z • 1
⊢ tprodCoeff R z f = z • ↑(tprod R) f
conv_lhs => rw [this]
no goals
ι : Type u_1
ι₂ : Type ?u.228081
ι₃ : Type ?u.228084
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.228093
R₂ : Type ?u.228096
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.228286
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.228420
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.228554
inst✝ : AddCommMonoid F
z : R
f : (i : ι) → s i
⊢ z = z • 1
simp only [mul_one, Algebra.id.smul_eq_mul]