-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem coeff_mul_prod_one_sub_of_lt_order {R ι : Type*} [CommRing R] (k : ℕ) (s : Finset ι)
    (φ : R⟦X⟧) (f : ι → R⟦X⟧) :
    (∀ i ∈ s, ↑k < (f i).order) → coeff R k (φ * ∏ i ∈ s, (1 - f i)) = coeff R k φ

Proof state:
case empty
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ i ∈ ∅, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ ∅, (1 - f i)) = (coeff R k) φ

Tactic:
simp

Result:
no goals

Proof state:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
t : ∀ i ∈ insert a s, ↑k < (f i).order
⊢ (coeff R k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff R k) φ

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at t

Result:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff R k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff R k) φ

Proof state:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff R k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff R k) φ

Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_one_sub_of_lt_order _ t.1]

Result:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff R k) (φ * ∏ x ∈ s, (1 - f x)) = (coeff R k) φ

Proof state:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
⊢ (∀ i ∈ insert a s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff R k) φ

Tactic:
intro t

Result:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
t : ∀ i ∈ insert a s, ↑k < (f i).order
⊢ (coeff R k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff R k) φ

Proof state:
case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
t : ↑k < (f a).order ∧ ∀ a ∈ s, ↑k < (f a).order
⊢ (coeff R k) (φ * ∏ x ∈ s, (1 - f x)) = (coeff R k) φ

Tactic:
exact ih t.2

Result:
no goals

Proof state:
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
s : Finset ι
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ

Tactic:
induction' s using Finset.induction_on with a s ha ih t

Result:
case empty
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
⊢ (∀ i ∈ ∅, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ ∅, (1 - f i)) = (coeff R k) φ

case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff R k) φ
⊢ (∀ i ∈ insert a s, ↑k < (f i).order) → (coeff R k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff R k) φ