Theorem: MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrder (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
Tactic:
refine' Finset.induction_on s _ _
State after:
case refine'_1
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ (∀ i ∈ ∅, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ ∅, (1 - g i)) = (coeff α d) f

case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f) →
        (∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)) →
          (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f

State before:
case refine'_1
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ (∀ i ∈ ∅, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ ∅, (1 - g i)) = (coeff α d) f
Tactic:
simp only [imp_true_iff, Finset.prod_empty, mul_one, eq_self_iff_true]
State after:
no goals

State before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f) →
        (∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)) →
          (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Tactic:
intro a s ha ih t
State after:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f

State before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at t
State after:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f

State before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff α d) f
Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
  coeff_mul_one_sub_of_lt_weightedOrder w _ t.1]
State after:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ x ∈ s, (1 - g x)) = (coeff α d) f

State before:
case refine'_2
σ : Type u_3
α✝ : Type ?u.62270
inst✝¹ : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
α : Type u_1
ι : Type u_2
inst✝ : CommRing α
d : σ →₀ ℕ
s✝ : Finset ι
f : MvPowerSeries σ α
g : ι → MvPowerSeries σ α
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff α d) (f * ∏ i ∈ s, (1 - g i)) = (coeff α d) f
t : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff α d) (f * ∏ x ∈ s, (1 - g x)) = (coeff α d) f
Tactic:
exact ih t.2
State after:
no goals