case empty
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
⊢ (∀ (i : ι), i ∈ ∅ → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in ∅, (1 - f i)) = ↑(coeff R k) φ

case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
⊢ (∀ (i : ι), i ∈ insert a s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in insert a s, (1 - f i)) = ↑(coeff R k) φ
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
s : Finset ι
φ : PowerSeries R
f : ι → PowerSeries R
⊢ (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
induction' s using Finset.induction_on with a s ha ih t
no goals
case empty
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
⊢ (∀ (i : ι), i ∈ ∅ → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in ∅, (1 - f i)) = ↑(coeff R k) φ
simp
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
t : ∀ (i : ι), i ∈ insert a s → ↑k < order (f i)
⊢ ↑(coeff R k) (φ * ∏ i in insert a s, (1 - f i)) = ↑(coeff R k) φ
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
⊢ (∀ (i : ι), i ∈ insert a s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in insert a s, (1 - f i)) = ↑(coeff R k) φ
intro t
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
t : ↑k < order (f a) ∧ ∀ (a : ι), a ∈ s → ↑k < order (f a)
⊢ ↑(coeff R k) (φ * ∏ i in insert a s, (1 - f i)) = ↑(coeff R k) φ
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
t : ∀ (i : ι), i ∈ insert a s → ↑k < order (f i)
⊢ ↑(coeff R k) (φ * ∏ i in insert a s, (1 - f i)) = ↑(coeff R k) φ
simp only [Finset.mem_insert, forall_eq_or_imp] at t
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
t : ↑k < order (f a) ∧ ∀ (a : ι), a ∈ s → ↑k < order (f a)
⊢ ↑(coeff R k) (φ * ∏ x in s, (1 - f x)) = ↑(coeff R k) φ
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
t : ↑k < order (f a) ∧ ∀ (a : ι), a ∈ s → ↑k < order (f a)
⊢ ↑(coeff R k) (φ * ∏ i in insert a s, (1 - f i)) = ↑(coeff R k) φ
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]
no goals
case insert
R✝ : Type ?u.4226629
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
ι : Type u_2
inst✝ : CommRing R
k : ℕ
φ : PowerSeries R
f : ι → PowerSeries R
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑k < order (f i)) → ↑(coeff R k) (φ * ∏ i in s, (1 - f i)) = ↑(coeff R k) φ
t : ↑k < order (f a) ∧ ∀ (a : ι), a ∈ s → ↑k < order (f a)
⊢ ↑(coeff R k) (φ * ∏ x in s, (1 - f x)) = ↑(coeff R k) φ
exact ih t.2