awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
cons :
  weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤
    weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
have cons₁ : weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
cons :
  weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤
    weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
cons₁ : weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
have cons₂ : weightedOrder w (f a) + weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
cons :
  weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤
    weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
cons₁ : weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
cons₂ :
  weightedOrder w (f a) + weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) ≤ weightedOrder w (f a * ∏ x ∈ s, f x)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
have cons₃ : weightedOrder w (f a * ∏ i ∈ s, f i) ≤ weightedOrder w (f a * ∏ i ∈ s, f i)
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
s : Finset ι
⊢ ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
have empty : ∑ i ∈ ∅, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
s : Finset ι
empty : ∑ i ∈ ∅, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i)
⊢ ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)),
  ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have simp : Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
Tactic: simp only [mul_sub, mul_one, map_sub, sub_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
have apply : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (f * g)
Tactic: apply coeff_eq_zero_of_lt_weightedOrder w
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((1 - g) * f) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have simp : Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (g * f) : R) (0 : R)
Tactic: simp only [sub_mul, one_mul, map_sub, sub_eq_self]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (g * f) : R) (0 : R)
have apply : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g * f)
Tactic: apply coeff_eq_zero_of_lt_weightedOrder w
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : 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 :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h : ∀ i ∈ insert a s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have h₁ : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
  ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
Tactic: simp only [Finset.mem_insert, forall_eq_or_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : 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 :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert : Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ((1 - g a) * ∏ x ∈ s, (1 - g x))) : R)
  ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : 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 :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
insert :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ((1 - g a) * ∏ x ∈ s, (1 - g x))) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert₁ : Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g a) * ∏ x ∈ s, (1 - g x)) : R)
  ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : 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 :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
insert :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ((1 - g a) * ∏ x ∈ s, (1 - g x))) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₁ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g a) * ∏ x ∈ s, (1 - g x)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert₂ : Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((f * ∏ x ∈ s, (1 - g x)) * (1 - g a)) : R)
  ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : 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 :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
insert :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ((1 - g a) * ∏ x ∈ s, (1 - g x))) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₁ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g a) * ∏ x ∈ s, (1 - g x)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₂ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((f * ∏ x ∈ s, (1 - g x)) * (1 - g a)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert₃ : Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ x ∈ s, (1 - g x)) : R)
  ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : 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 :
  ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
h :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a) ∧
    ∀ a ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g a)
insert :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ((1 - g a) * ∏ x ∈ s, (1 - g x))) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₁ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * (1 - g a) * ∏ x ∈ s, (1 - g x)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₂ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) ((f * ∏ x ∈ s, (1 - g x)) * (1 - g a)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert₃ :
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ x ∈ s, (1 - g x)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert₄ : Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have empty : ∀
  (h :
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
Tactic: induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, mul_one]
  | insert a s ha ih =>
    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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
      Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
        ((coeff d : (a : MvPowerSeries σ R) → R) f : R))
  (h : ∀ i ∈ insert a s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
Tactic: induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, mul_one]
  | insert a s ha ih =>
    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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have empty : ∀
  (h :
    ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, mul_one]
  | insert a s ha ih =>
    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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (ih :
    ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
      Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
        ((coeff d : (a : MvPowerSeries σ R) → R) f : R))
  (h : ∀ i ∈ insert a s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
  Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ insert a s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, mul_one]
  | insert a s ha ih =>
    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]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
⊢ weightedOrder w (-f) = weightedOrder w f
have by_contra! : ∀ (h : weightedOrder w (-f) ≠ weightedOrder w f), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
⊢ False
have this : f = 0
Tactic: have : f = 0 := by simpa using (weightedOrder_add_of_weightedOrder_ne w h).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ weightedOrder w (p.toSubring T hp) = weightedOrder w p
have refine_1 : weightedOrder w (p.toSubring T hp) ≤ weightedOrder w p
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
refine_1 : weightedOrder w (p.toSubring T hp) ≤ weightedOrder w p
⊢ weightedOrder w (p.toSubring T hp) = weightedOrder w p
have refine_2 : weightedOrder w p ≤ weightedOrder w (p.toSubring T hp)
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔
    ∃ (n : ℕ) (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (degree : (a : σ →₀ ℕ) → ℕ) d = n
have simp_rw : f ≠ 0 ↔
  ∃ (n : ℕ) (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n
Tactic: simp_rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : (↑f.order.toNat : ℕ∞) = f.order
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = f.order
have simp_rw : ∃ (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = f.order
Tactic: simp_rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ f.order ≤ (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw : f.order ≤ (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < f.order
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
have h₁ : (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < f.order
Tactic: rw [degree_eq_weight_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (degree : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ f.order
have h₁ : ∀ (d : σ →₀ ℕ),
  (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: simp_rw [degree_eq_weight_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h :
  ∀ (d : σ →₀ ℕ),
    (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ n ≤ f.order
have h₁ : ∀ (d : σ →₀ ℕ),
  (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < n →
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
Tactic: simp_rw [degree_eq_weight_one] at h
Cleared hypotheses: h