-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_mul_prod_one_sub_of_lt_weightedOrder {R ι : Type*} [CommRing R] (d : σ →₀ ℕ)
    (s : Finset ι) (f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R) :
    (∀ i ∈ s, (weight w d) < weightedOrder w (g i)) →
      coeff R d (f * ∏ i ∈ s, (1 - g i)) = coeff R d f

Proof state:
case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f
h : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff R d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff R d) f

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

Result:
case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f
h : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff R d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff R d) f

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f

Tactic:
classical
induction s using Finset.induction_on with
| empty => simp only [imp_true_iff, Finset.prod_empty, mul_one, eq_self_iff_true]
| @insert a s ha ih =>
  intro h
  simp only [Finset.mem_insert, forall_eq_or_imp] at h
  rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
    coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

Result:
no goals

Proof state:
case empty
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ ∅, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ ∅, (1 - g i)) = (coeff R d) f

Tactic:
simp only [imp_true_iff, Finset.prod_empty, mul_one, eq_self_iff_true]

Result:
no goals

Proof state:
case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f
⊢ (∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)) →
    (coeff R d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff R d) f

Tactic:
intro h

Result:
case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f
h : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff R d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff R d) f

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f

Tactic:
induction s using Finset.induction_on with
| empty => simp only [imp_true_iff, Finset.prod_empty, mul_one, eq_self_iff_true]
| @insert a s ha ih =>
  intro h
  simp only [Finset.mem_insert, forall_eq_or_imp] at h
  rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
    coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

Result:
no goals

Proof state:
case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f
h : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff R d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff R d) f

Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
  coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

Result:
no goals