awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
rw :
  LE.le (α := ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
    (↑n : ℕ∞)
⊢ φ.order ≤ (↑n : ℕ∞)
have rw₁ : LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞)
  (↑n : ℕ∞)
Tactic: classical
  rw [order, dif_neg]
  · simpa using ⟨n, le_rfl, h⟩
  · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
rw :
  LE.le (α := ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
    (↑n : ℕ∞)
rw₁ :
  LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)
⊢ φ.order ≤ (↑n : ℕ∞)
have hnc : ¬φ = 0
Tactic: classical
  rw [order, dif_neg]
  · simpa using ⟨n, le_rfl, h⟩
  · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : (↑n : ℕ∞) < φ.order
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
have contrapose! : ∀ (h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)), φ.order ≤ (↑n : ℕ∞)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
have pos : ∀ (h' : φ = 0), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: by_cases h' : φ = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
pos : ∀ (h' : φ = 0), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
have neg : ∀ (h' : ¬φ = 0), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: by_cases h' : φ = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
have neg : (↑n : ℕ∞) < φ.order
Tactic: refine coeff_of_lt_order _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
h' : ¬φ = 0
⊢ (↑n : ℕ∞) < φ.order
have neg : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑φ.order.toNat : ℕ∞)
Tactic: rwa [← coe_toNat_order h', ENat.coe_lt_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
have pos : φ = 0 → LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
pos : φ = 0 → LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
have neg : ∀ (h : ¬φ = 0),
  LE.le (α := ℕ∞) (↑n : ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ φ.order
have simp : LE.le (α := ℕ∞) (↑n : ℕ∞)
  (if h : φ = 0 then ⊤
  else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞))
Tactic: classical
  simp only [order]
  split_ifs
  · simp
  · simpa [Nat.le_find_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
simp :
  LE.le (α := ℕ∞) (↑n : ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
⊢ (↑n : ℕ∞) ≤ φ.order
have pos : φ = 0 → LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: classical
  simp only [order]
  split_ifs
  · simp
  · simpa [Nat.le_find_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
simp :
  LE.le (α := ℕ∞) (↑n : ℕ∞)
    (if h : φ = 0 then ⊤
    else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
pos : φ = 0 → LE.le (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ (↑n : ℕ∞) ≤ φ.order
have neg : ∀ (h : ¬φ = 0),
  LE.le (α := ℕ∞) (↑n : ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞)
Tactic: classical
  simp only [order]
  split_ifs
  · simp
  · simpa [Nat.le_find_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ φ.order
have coe : ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: convert! nat_le_order φ n _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ∞
h : ∀ (i : ℕ), (↑i : ℕ∞) < n → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ n ≤ φ.order
have top : ∀ (h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)), ⊤ ≤ φ.order
Tactic: cases n with
  | top => simpa using ext (by simpa using h)
  | coe n =>
    convert! nat_le_order φ n _
    simpa using h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ∞
h : ∀ (i : ℕ), (↑i : ℕ∞) < n → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
top :
  ∀ (h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)), ⊤ ≤ φ.order
⊢ n ≤ φ.order
have coe : ∀ (n : ℕ) (h : ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)),
  (↑n : ℕ∞) ≤ φ.order
Tactic: cases n with
  | top => simpa using ext (by simpa using h)
  | coe n =>
    convert! nat_le_order φ n _
    simpa using h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have inl : order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
  Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
    ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)
Tactic: rcases eq_or_ne φ 0 with (rfl | hφ)
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
inl :
  order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
      ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have inr : ∀ (hφ : φ ≠ 0),
  φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rcases eq_or_ne φ 0 with (rfl | hφ)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have inl : order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
  Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
    ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)
Tactic: classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  simp [order, dif_neg hφ, Nat.find_eq_iff]
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
inl :
  order.{u_1} (R := R) 0 = (↑n : ℕ∞) ↔
    Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) 0 : R) (0 : R) ∧
      ∀ i < n, Eq.{u_1 + 1} (α := R) ((coeff i : (a : R⟦X⟧) → R) 0 : R) (0 : R)
⊢ φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have inr : ∀ (hφ : φ ≠ 0),
  φ.order = (↑n : ℕ∞) ↔
    Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R) ∧
      ∀ i < n, Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: classical
  rcases eq_or_ne φ 0 with (rfl | hφ)
  · simp
  simp [order, dif_neg hφ, Nat.find_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ∞
⊢ φ.order = n ↔
    (∀ (i : ℕ), (↑i : ℕ∞) = n → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), (↑i : ℕ∞) < n → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have top : φ.order = ⊤ ↔
  (∀ (i : ℕ), Eq (α := ℕ∞) (↑i : ℕ∞) ⊤ → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
    ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: cases n with
  | top => simp
  | coe n => simp [order_eq_nat]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ∞
top :
  φ.order = ⊤ ↔
    (∀ (i : ℕ), Eq (α := ℕ∞) (↑i : ℕ∞) ⊤ → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) ⊤ → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order = n ↔
    (∀ (i : ℕ), (↑i : ℕ∞) = n → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), (↑i : ℕ∞) < n → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have coe : ∀ (n : ℕ),
  φ.order = (↑n : ℕ∞) ↔
    (∀ (i : ℕ), Eq (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)) ∧
      ∀ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: cases n with
  | top => simp
  | coe n => simp [order_eq_nat]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ φ.order = MvPowerSeries.order φ
have refine_1 : φ.order ≤ MvPowerSeries.order φ
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
refine_1 : φ.order ≤ MvPowerSeries.order φ
⊢ φ.order = MvPowerSeries.order φ
have refine_2 : MvPowerSeries.order φ ≤ φ.order
Tactic: refine eq_of_le_of_ge ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
⊢ Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
have this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: have : coeff ↑(Finsupp.degree d) φ = 0 := coeff_of_lt_order _ hd
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
d : Unit →₀ ℕ
hd : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : ℕ∞) < φ.order
this : Eq (α := R) ((coeff ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d) : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) φ : R) (0 : R)
have eq_aux : Eq (α := ℕ) ((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) d : ℕ) ((d : (a : Unit) → ℕ) () : ℕ)
Tactic: have eq_aux : d.degree = d () := Finset.sum_eq_single _ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
i : ℕ
hi : (↑i : ℕ∞) < MvPowerSeries.order φ
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
have hi₁ : (↑((Finsupp.degree : (a : Unit →₀ ℕ) → ℕ) (single () i)) : ℕ∞) < MvPowerSeries.order φ
Tactic: rw [← Finsupp.degree_single () i] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
⊢ min φ.order ψ.order ≤ (φ + ψ).order
have refine : ∀ (i : ℕ), (↑i : ℕ∞) < min φ.order ψ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
Tactic: refine le_order _ _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
have rw : φ.order ≤ φ.order ∧ φ.order ≤ ψ.order
Tactic: rw [le_inf_iff, this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
have suffices : (φ + ψ).order = φ.order
Tactic: suffices order (φ + ψ) = order φ by
    rw [le_inf_iff, this]
    exact ⟨le_rfl, le_of_lt H⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (φ + ψ).order = φ.order
have rw : (∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)) ∧
  ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
Tactic: rw [order_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
⊢ (∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)) ∧
    ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have left : ∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
left : ∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
⊢ (∀ (i : ℕ), (↑i : ℕ∞) = φ.order → Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)) ∧
    ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have right : ∀ (i : ℕ), (↑i : ℕ∞) < φ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) = φ.order
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have H₁ : (↑i : ℕ∞) < ψ.order
Tactic: rw [← hi] at H
Cleared hypotheses: H, hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : (↑i : ℕ∞) < ψ.order
hi : (↑i : ℕ∞) = φ.order
⊢ Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have left : Ne (α := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [(coeff _).map_add, coeff_of_lt_order i H, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) < φ.order
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have right : HAdd.hAdd (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) < φ.order
right : HAdd.hAdd (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have right₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) < φ.order
right : HAdd.hAdd (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
right₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have right₂ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : (↑i : ℕ∞) < φ.order
right : HAdd.hAdd (α := R) (β := R) ((coeff i : (a : R⟦X⟧) → R) φ : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
right₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff i : (a : R⟦X⟧) → R) ψ : R) = 0
right₂ : HAdd.hAdd (α := R) 0 0 = 0
⊢ Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ + ψ) : R) (0 : R)
have right₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [(coeff _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
      zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
⊢ (φ + ψ).order = min φ.order ψ.order
have refine : (φ + ψ).order ≤ min φ.order ψ.order
Tactic: refine le_antisymm ?_ (min_order_le_order_add _ _)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
have inl : ∀ (φ_lt_ψ : φ.order < ψ.order), (φ + ψ).order ≤ min φ.order ψ.order
Tactic: rcases h.lt_or_gt with (φ_lt_ψ | ψ_lt_φ)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
inl : ∀ (φ_lt_ψ : φ.order < ψ.order), (φ + ψ).order ≤ min φ.order ψ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order
have inr : ∀ (ψ_lt_φ : ψ.order < φ.order), (φ + ψ).order ≤ min φ.order ψ.order
Tactic: rcases h.lt_or_gt with (φ_lt_ψ | ψ_lt_φ)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
⊢ φ.order + ψ.order ≤ (φ * ψ).order
have h : ∀ (i : ℕ), (↑i : ℕ∞) < φ.order + ψ.order → Eq (α := R) ((coeff i : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
Tactic: apply le_order
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (φ * ψ) : R) (0 : R)
have h : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R) ((coeff x.2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rw [coeff_mul, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have pos : ∀ (hi : (↑i : ℕ∞) < φ.order),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: by_cases! hi : ↑i < order φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
pos :
  ∀ (hi : (↑i : ℕ∞) < φ.order),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg : ∀ (hi : φ.order ≤ (↑i : ℕ∞)),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: by_cases! hi : ↑i < order φ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : (↑i : ℕ∞) < φ.order
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: rw [coeff_of_lt_order i hi, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : (↑i : ℕ∞) < φ.order
pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have pos₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_of_lt_order i hi, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have pos : ∀ (hj : (↑j : ℕ∞) < ψ.order),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: by_cases! hj : ↑j < order ψ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
pos :
  ∀ (hj : (↑j : ℕ∞) < ψ.order),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have neg : ∀ (hj : ψ.order ≤ (↑j : ℕ∞)),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
Tactic: by_cases! hj : ↑j < order ψ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
n : ℕ
hn : (↑n : ℕ∞) < φ.order + ψ.order
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hi : φ.order ≤ (↑i : ℕ∞)
hj : (↑j : ℕ∞) < ψ.order
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) ((coeff (i, j).2 : (a : R⟦X⟧) → R) ψ : R) = 0
have pos : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R) (0 : R) = 0
Tactic: rw [coeff_of_lt_order j hj, mul_zero]