ι : Type u_1
ι₂ : Type ?u.230665
ι₃ : Type ?u.230668
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.230677
R₂ : Type ?u.230680
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.230870
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.231004
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.231138
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
⊢ C z
ι : Type u_1
ι₂ : Type ?u.230665
ι₃ : Type ?u.230668
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.230677
R₂ : Type ?u.230680
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.230870
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.231004
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.231138
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (r • ↑(tprod R) f)
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
⊢ C z
simp_rw [← tprodCoeff_eq_smul_tprod] at C1
no goals
ι : Type u_1
ι₂ : Type ?u.230665
ι₃ : Type ?u.230668
R : Type u_2
inst✝⁷ : CommSemiring R
R₁ : Type ?u.230677
R₂ : Type ?u.230680
s : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type ?u.230870
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type ?u.231004
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type ?u.231138
inst✝ : AddCommMonoid F
C : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C x → C y → C (x + y)
C1 : ∀ {r : R} {f : (i : ι) → s i}, C (tprodCoeff R r f)
⊢ C z
exact PiTensorProduct.induction_on' z @C1 @Cp