awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∧
    ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
neg : ψ⁻¹ * φ⁻¹ * φ * ψ = 1
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
have neg₁ : ψ⁻¹ * (φ⁻¹ * φ) * ψ = 1
Tactic: rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∧
    ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
neg : ψ⁻¹ * φ⁻¹ * φ * ψ = 1
neg₁ : ψ⁻¹ * (φ⁻¹ * φ) * ψ = 1
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
have neg₂ : ψ⁻¹ * 1 * ψ = 1
Tactic: rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∧
    ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
neg : ψ⁻¹ * φ⁻¹ * φ * ψ = 1
neg₁ : ψ⁻¹ * (φ⁻¹ * φ) * ψ = 1
neg₂ : ψ⁻¹ * 1 * ψ = 1
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
have neg₃ : ψ⁻¹ * ψ = 1
Tactic: rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∧
    ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
neg : ψ⁻¹ * φ⁻¹ * φ * ψ = 1
neg₁ : ψ⁻¹ * (φ⁻¹ * φ) * ψ = 1
neg₂ : ψ⁻¹ * 1 * ψ = 1
neg₃ : ψ⁻¹ * ψ = 1
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
have neg₄ : Eq (α := MvPowerSeries σ k) 1 1
Tactic: rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
k : Type u_3
inst : Field k
⊢ Eq (α := MvPowerSeries σ k) 1⁻¹ 1
have rw : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) 1 : k) (0 : k)
Tactic: rw [MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
r : k
⊢ Eq (α := MvPowerSeries σ k) (((C : (a : k) → MvPowerSeries σ k) r)⁻¹ : MvPowerSeries σ k)
    ((C : (a : k) → MvPowerSeries σ k) r⁻¹ : MvPowerSeries σ k)
have inl : Eq (α := MvPowerSeries σ k) ((C : (a : k) → MvPowerSeries σ k) 0)⁻¹ ((C : (a : k) → MvPowerSeries σ k) 0⁻¹)
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
r : k
inl : Eq (α := MvPowerSeries σ k) ((C : (a : k) → MvPowerSeries σ k) 0)⁻¹ ((C : (a : k) → MvPowerSeries σ k) 0⁻¹)
⊢ Eq (α := MvPowerSeries σ k) (((C : (a : k) → MvPowerSeries σ k) r)⁻¹ : MvPowerSeries σ k)
    ((C : (a : k) → MvPowerSeries σ k) r⁻¹ : MvPowerSeries σ k)
have inr : ∀ (hr : r ≠ 0),
  Eq (α := MvPowerSeries σ k) (((C : (a : k) → MvPowerSeries σ k) r)⁻¹ : MvPowerSeries σ k)
    ((C : (a : k) → MvPowerSeries σ k) r⁻¹ : MvPowerSeries σ k)
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
r : k
hr : r ≠ 0
⊢ Eq (α := MvPowerSeries σ k) (((C : (a : k) → MvPowerSeries σ k) r)⁻¹ : MvPowerSeries σ k)
    ((C : (a : k) → MvPowerSeries σ k) r⁻¹ : MvPowerSeries σ k)
have inr : Ne.{u_3 + 1} (α := k)
  ((constantCoeff : (a : MvPowerSeries σ k) → k) ((C : (a : k) → MvPowerSeries σ k) r : MvPowerSeries σ k) : k) (0 : k)
Tactic: rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel₀ hr, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
s : σ
⊢ Eq (α := MvPowerSeries σ k) (X s)⁻¹ 0
have rw : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (X s) : k) (0 : k)
Tactic: rw [inv_eq_zero, constantCoeff_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
s : σ
rw : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (X s) : k) (0 : k)
⊢ Eq (α := MvPowerSeries σ k) (X s)⁻¹ 0
have rw₁ : Eq.{u_3 + 1} (α := k) 0 0
Tactic: rw [inv_eq_zero, constantCoeff_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ WithTop (Lex (σ →₀ ℕ))
have ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
Tactic: have ne : Set.Nonempty (toLex '' φ.support) := by
      simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, h, not_false_eq_true]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ WithTop (Lex (σ →₀ ℕ))
have a : Lex (σ →₀ ℕ)
Tactic: apply WithTop.some
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ Lex (σ →₀ ℕ)
have apply : Lex (σ →₀ ℕ) → Lex (σ →₀ ℕ) → Prop
Tactic: apply WellFounded.min _ (toLex '' φ.support) ne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
apply : Lex (σ →₀ ℕ) → Lex (σ →₀ ℕ) → Prop
⊢ Lex (σ →₀ ℕ)
have apply₁ : WellFounded.{u_1 + 1} (α := Lex (σ →₀ ℕ)) LT.lt
Tactic: apply WellFounded.min _ (toLex '' φ.support) ne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))
have h : φ.lexOrder =
  (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
        ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
    WithTop (Lex (σ →₀ ℕ)))
Tactic: use ne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))
have suffices : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
Tactic: suffices ne : Set.Nonempty (toLex '' φ.support) by
    use ne
    unfold lexOrder
    simp only [dif_neg hφ]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ)))
      (if h : φ = 0 then ⊤
      else
        have ne := ⋯;
        (↑(WellFounded.min (r := LT.lt) ⋯ ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
          WithTop (Lex (σ →₀ ℕ))))
      ⊤ ↔
    φ = 0
have pos : ∀ (h : φ = 0), Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ))) ⊤ ⊤ ↔ φ = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
pos : ∀ (h : φ = 0), Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ))) ⊤ ⊤ ↔ φ = 0
⊢ Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ)))
      (if h : φ = 0 then ⊤
      else
        have ne := ⋯;
        (↑(WellFounded.min (r := LT.lt) ⋯ ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
          WithTop (Lex (σ →₀ ℕ))))
      ⊤ ↔
    φ = 0
have neg : ∀ (h : ¬φ = 0),
  Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ)))
      (have ne := sorry;
      (↑(WellFounded.min (r := LT.lt) sorry ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ))))
      ⊤ ↔
    φ = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
⊢ Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ)))
    (if h : Eq (α := MvPowerSeries σ R) 0 0 then ⊤
    else
      have ne := ⋯;
      (↑(WellFounded.min (r := LT.lt) ⋯
            (Set.image (α := σ →₀ ℕ) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) (Function.support.{u_1, u_2} (M := R) 0))
            ne) :
        WithTop (Lex (σ →₀ ℕ))))
    ⊤
have rw : Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ))) ⊤ ⊤
Tactic: rw [dif_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ∃ (d : σ →₀ ℕ), φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
have hφ₁ : ∃ (a : Lex (σ →₀ ℕ)), (↑a : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
Tactic: simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, WithTop.ne_top_iff_exists] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : ∃ (a : Lex (σ →₀ ℕ)), (↑a : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
⊢ ∃ (d : σ →₀ ℕ), φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
have obtain : ∀ (p : Lex (σ →₀ ℕ)) (hp : (↑p : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder),
  ∃ (d : σ →₀ ℕ), φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
Tactic: obtain ⟨p, hp⟩ := hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have hφ : φ ≠ 0
Tactic: have hφ : φ ≠ 0 := by
    simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, ← h, WithTop.coe_ne_top, not_false_eq_true]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have hφ' : ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
Tactic: have hφ' := lexOrder_def_of_ne_zero hφ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
hφ' :
  ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
Tactic: rcases hφ' with ⟨ne, hφ'⟩
Cleared hypotheses: hφ'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
hφ' :
  ∃ (ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have hφ'₁ : φ.lexOrder =
  (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
        ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
    WithTop (Lex (σ →₀ ℕ)))
Tactic: rcases hφ' with ⟨ne, hφ'⟩
Cleared hypotheses: hφ'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have hφ'₁ : (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
  WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
Tactic: simp only [← h, WithTop.coe_eq_coe] at hφ'
Cleared hypotheses: hφ'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
this :
  Membership.mem (α := Lex (σ →₀ ℕ)) (γ := Set (Lex (σ →₀ ℕ)))
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have this₁ : ¬φ d = 0
Tactic: simp only [Set.mem_image_equiv, toLex_symm_eq, ofLex_toLex, Function.mem_support, ne_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have suffices : Membership.mem (α := Lex (σ →₀ ℕ)) (γ := Set (Lex (σ →₀ ℕ)))
  ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
  ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))
Tactic: suffices toLex d ∈ toLex '' φ.support by
    simp only [Set.mem_image_equiv, toLex_symm_eq, ofLex_toLex, Function.mem_support, ne_eq] at this
    apply this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
hφ : φ ≠ 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d =
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
⊢ Membership.mem (α := Lex (σ →₀ ℕ)) (γ := Set (Lex (σ →₀ ℕ)))
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d : Lex (σ →₀ ℕ))
have rw : Membership.mem (γ := Set (Lex (σ →₀ ℕ))) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
  (WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne)
Tactic: rw [hφ']
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have pos : ∀ (hφ : φ = 0), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
Tactic: by_cases hφ : φ = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
pos : ∀ (hφ : φ = 0), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have neg : ∀ (hφ : ¬φ = 0), Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
Tactic: by_cases hφ : φ = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
Tactic: rcases lexOrder_def_of_ne_zero hφ with ⟨ne, hφ'⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have hφ' : φ.lexOrder =
  (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
        ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
    WithTop (Lex (σ →₀ ℕ)))
Tactic: rcases lexOrder_def_of_ne_zero hφ with ⟨ne, hφ'⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have h₁ : (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
  WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) sorry
    ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
Tactic: rw [hφ', WithTop.coe_lt_coe] at h
Cleared hypotheses: h, hφ'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
hφ : ¬φ = 0
ne : Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)
h :
  (toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d <
    WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
      ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne
hφ' :
  φ.lexOrder =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have neg : ∀ (h' : ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ φ.lexOrder ≤ (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
have rw : ¬(↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < φ.lexOrder
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LexOrder (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
⊢ w ≤ φ.lexOrder ↔
    ∀ (d : σ →₀ ℕ),
      (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mp : w ≤ φ.lexOrder →
  ∀ (d : σ →₀ ℕ),
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ))) < w →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
Tactic: constructor