awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
rw : φ.invOfUnit u = φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯)
⊢ φ.invOfUnit u = φ⁻¹

Tactic:
rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)]

Premises used: MvPowerSeries.invOfUnit_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
apply : u = Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯
⊢ φ.invOfUnit u = φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯)

Tactic:
apply congrArg (invOfUnit φ)

Premises used: congrArg, MvPowerSeries.invOfUnit
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
rw : (↑u : k) = (↑(Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯) : k)
⊢ u = Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯

Tactic:
rw [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
⊢ (↑u : k) = (↑(Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯) : k)

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
⊢ (↑u : k) = (↑(Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯) : k)

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
rw : φ * φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) h) = 1
rw₁ rw₂ : Eq (α := MvPowerSeries σ k) 1 1
⊢ φ * φ⁻¹ = 1

Tactic:
rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl]

Premises used: Units.mk0, MvPowerSeries.mul_invOfUnit, MvPowerSeries.invOfUnit_eq, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
rw : φ * φ⁻¹ = 1
rw₁ rw₂ : Eq (α := MvPowerSeries σ k) 1 1
⊢ φ⁻¹ * φ = 1

Tactic:
rw [mul_comm, φ.mul_inv_cancel h]

Premises used: mul_comm, MvPowerSeries.mul_inv_cancel
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k_1 : Type u_3
inst : Field k_1
φ₁ φ₂ φ₃ : MvPowerSeries σ k_1
h : Ne.{u_3 + 1} (α := k_1) ((constantCoeff : (a : MvPowerSeries σ k_1) → k_1) φ₃ : k_1) (0 : k_1)
k : φ₁ = φ₂ * φ₃⁻¹
⊢ φ₁ * φ₃ = φ₂

Tactic:
simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h]

Premises used: mul_assoc, MvPowerSeries.inv_mul_cancel
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k_1 : Type u_3
inst : Field k_1
φ₁ φ₂ φ₃ : MvPowerSeries σ k_1
h : Ne.{u_3 + 1} (α := k_1) ((constantCoeff : (a : MvPowerSeries σ k_1) → k_1) φ₃ : k_1) (0 : k_1)
k : φ₁ * φ₃ = φ₂
⊢ φ₁ = φ₂ * φ₃⁻¹

Tactic:
simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]

Premises used: mul_assoc, MvPowerSeries.mul_inv_cancel
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
rw : φ = ψ⁻¹ ↔ φ = 1 * ψ⁻¹
rw₁ rw₂ : φ = ψ⁻¹ ↔ φ = ψ⁻¹
⊢ φ = ψ⁻¹ ↔ φ * ψ = 1

Tactic:
rw [← MvPowerSeries.eq_mul_inv_iff_mul_eq h, one_mul]

Premises used: MvPowerSeries.eq_mul_inv_iff_mul_eq, one_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
rw : φ = ψ⁻¹ ↔ φ * ψ = 1
rw₁ rw₂ : φ * ψ = 1 ↔ φ * ψ = 1
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1

Tactic:
rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h]

Premises used: MvPowerSeries.eq_inv_iff_mul_eq_one, eq_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
pos :
  ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)),
    (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
neg :
  ∀ (h : ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)),
    (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
by_cases h : constantCoeff (φ * ψ) = 0

Premises used: HMul.hMul, MvPowerSeries.constantCoeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
pos : 0 = ψ⁻¹ * φ⁻¹
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
rw [inv_eq_zero.mpr h]

Premises used: Iff.mpr, MvPowerSeries.inv_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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) ∨
    Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)

Tactic:
simp only [map_mul, mul_eq_zero] at h

Premises used: mul_eq_zero, map_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
pos : ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)), 0 = ψ⁻¹ * φ⁻¹
pos₁ : ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)), 0 = ψ⁻¹ * φ⁻¹
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
rcases h with h | h
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
simp [inv_eq_zero.mpr h]

Premises used: Iff.mpr, MvPowerSeries.inv_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
simp [inv_eq_zero.mpr h]

Premises used: Iff.mpr, MvPowerSeries.inv_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
neg : ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]

Premises used: MvPowerSeries.inv_eq_iff_mul_eq_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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) ∧
    ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)

Tactic:
simp only [not_or, map_mul, mul_eq_zero] at h

Premises used: mul_eq_zero, not_or, map_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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
neg₄ neg₅ : Eq (α := MvPowerSeries σ k) 1 1
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1

Tactic:
rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]

Premises used: mul_assoc, MvPowerSeries.inv_mul_cancel, Inv.inv, And.right, And.left, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
k : Type u_3
inst : Field k
rw : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) 1 : k) (0 : k)
⊢ Eq (α := MvPowerSeries σ k) 1⁻¹ 1

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one]

Premises used: MvPowerSeries.inv_eq_iff_mul_eq_one, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
k : Type u_3
inst : Field k
⊢ Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) 1 : k) (0 : k)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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⁻¹)
inr :
  ∀ (hr : r ≠ 0),
    Eq (α := MvPowerSeries σ k) (((C : (a : k) → MvPowerSeries σ k) r)⁻¹ : MvPowerSeries σ k)
      ((C : (a : k) → MvPowerSeries σ k) r⁻¹ : MvPowerSeries σ k)
⊢ 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)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
⊢ Eq (α := MvPowerSeries σ k) ((C : (a : k) → MvPowerSeries σ k) 0)⁻¹ ((C : (a : k) → MvPowerSeries σ k) 0⁻¹)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
r : k
hr : r ≠ 0
inr :
  Ne.{u_3 + 1} (α := k)
    ((constantCoeff : (a : MvPowerSeries σ k) → k) ((C : (a : k) → MvPowerSeries σ k) r : MvPowerSeries σ k) : k)
    (0 : k)
⊢ Eq (α := MvPowerSeries σ k) (((C : (a : k) → MvPowerSeries σ k) r)⁻¹ : MvPowerSeries σ k)
    ((C : (a : k) → MvPowerSeries σ k) r⁻¹ : MvPowerSeries σ k)

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel₀ hr, map_one]

Premises used: MvPowerSeries.inv_eq_iff_mul_eq_one, map_mul, map_one, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
r : k
hr : r ≠ 0
⊢ Ne.{u_3 + 1} (α := k)
    ((constantCoeff : (a : MvPowerSeries σ k) → k) ((C : (a : k) → MvPowerSeries σ k) r : MvPowerSeries σ k) : k)
    (0 : k)

Tactic:
simpa using hr
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := k) 0 0
⊢ Eq (α := MvPowerSeries σ k) (X s)⁻¹ 0

Tactic:
rw [inv_eq_zero, constantCoeff_X]

Premises used: MvPowerSeries.inv_eq_zero, MvPowerSeries.constantCoeff_X
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
r : k
φ : MvPowerSeries σ k
⊢ (r • φ)⁻¹ = r⁻¹ • φ⁻¹

Tactic:
simp [smul_eq_C_mul, mul_comm]

Premises used: MvPowerSeries.smul_eq_C_mul, mul_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)

Tactic:
simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, h, not_false_eq_true]

Premises used: Set.image_nonempty, ne_eq, Function.support_nonempty_iff, not_false_eq_true
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ 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]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 φ)
a : Lex (σ →₀ ℕ)
⊢ WithTop (Lex (σ →₀ ℕ))

Tactic:
apply WithTop.some

Premises used: WithTop.some
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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
apply₁ : WellFounded.{u_1 + 1} (α := Lex (σ →₀ ℕ)) LT.lt
⊢ Lex (σ →₀ ℕ)

Tactic:
apply WellFounded.min _ (toLex '' φ.support) ne

Premises used: Function.support, WellFounded.min, Set.image, DFunLike.coe, toLex
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 (σ →₀ ℕ) → Lex (σ →₀ ℕ) → Prop

Tactic:
exact Finsupp.instLTLex.lt

Premises used: LT.lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 φ)
⊢ WellFounded.{u_1 + 1} (α := Lex (σ →₀ ℕ)) LT.lt

Tactic:
wellFounded_lt

Premises used: wellFounded_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 φ)
⊢ WellFounded.{u_1 + 1} (α := Lex (σ →₀ ℕ)) LT.lt

Tactic:
exact wellFounded_lt

Premises used: wellFounded_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ WithTop (Lex (σ →₀ ℕ))

Tactic:
exact if h : φ = 0 then ⊤ else by
    have ne : Set.Nonempty (toLex '' φ.support) := by
      simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, h, not_false_eq_true]
    apply WithTop.some
    apply WellFounded.min _ (toLex '' φ.support) ne
    · exact Finsupp.instLTLex.lt
    · exact wellFounded_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ WithTop (Lex (σ →₀ ℕ))

Tactic:
classical
  exact if h : φ = 0 then ⊤ else by
    have ne : Set.Nonempty (toLex '' φ.support) := by
      simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, h, not_false_eq_true]
    apply WithTop.some
    apply WellFounded.min _ (toLex '' φ.support) ne
    · exact Finsupp.instLTLex.lt
    · exact wellFounded_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 φ)
h :
  φ.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 φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))

Tactic:
use ne
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 φ)
⊢ (if h : φ = 0 then ⊤
    else
      have ne := ⋯;
      (↑(WellFounded.min (r := LT.lt) ⋯ ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))) =
    (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
          ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
      WithTop (Lex (σ →₀ ℕ)))

Tactic:
simp only [dif_neg hφ]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
suffices : 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 (σ →₀ ℕ)))

Tactic:
suffices ne : Set.Nonempty (toLex '' φ.support) by
    use ne
    unfold lexOrder
    simp only [dif_neg hφ]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ Set.Nonempty (α := Lex (σ →₀ ℕ)) ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ)

Tactic:
simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, hφ, not_false_eq_true]

Premises used: Set.image_nonempty, ne_eq, Function.support_nonempty_iff, not_false_eq_true
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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
neg :
  ∀ (h : ¬φ = 0),
    Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ)))
        (have ne := ⋯;
        (↑(WellFounded.min (r := LT.lt) ⋯ ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
          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

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : φ = 0
⊢ Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ))) ⊤ ⊤ ↔ φ = 0

Tactic:
simp only [h]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
h : ¬φ = 0
⊢ Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ)))
      (have ne := ⋯;
      (↑(WellFounded.min (r := LT.lt) ⋯ ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ))))
      ⊤ ↔
    φ = 0

Tactic:
simp only [h, WithTop.coe_ne_top]

Premises used: WithTop.coe_ne_top
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
rw rw₁ : Eq.{u_1 + 1} (α := WithTop (Lex (σ →₀ ℕ))) ⊤ ⊤
⊢ 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 (σ →₀ ℕ))))
    ⊤

Tactic:
rw [dif_pos rfl]

Premises used: dif_pos, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ∃ (a : Lex (σ →₀ ℕ)), (↑a : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder

Tactic:
simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, WithTop.ne_top_iff_exists] at hφ

Premises used: WithTop.ne_top_iff_exists, ne_eq, MvPowerSeries.lexOrder_eq_top_iff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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
obtain :
  ∀ (p : Lex (σ →₀ ℕ)) (hp : (↑p : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder),
    ∃ (d : σ →₀ ℕ), φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))
⊢ ∃ (d : σ →₀ ℕ), φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
obtain ⟨p, hp⟩ := hφ
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : (↑p : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
⊢ φ.lexOrder =
    (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) p : σ →₀ ℕ)) :
      WithTop (Lex (σ →₀ ℕ)))

Tactic:
simp only [toLex_ofLex, hp]

Premises used: toLex_ofLex
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder σ
inst_2 : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : (↑p : WithTop (Lex (σ →₀ ℕ))) = φ.lexOrder
⊢ ∃ (d : σ →₀ ℕ), φ.lexOrder = (↑((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) d) : WithTop (Lex (σ →₀ ℕ)))

Tactic:
exact ⟨ofLex p, by simp only [toLex_ofLex, hp]⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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
⊢ φ ≠ 0

Tactic:
simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, ← h, WithTop.coe_ne_top, not_false_eq_true]

Premises used: ne_eq, WithTop.coe_ne_top, MvPowerSeries.lexOrder_eq_top_iff_eq_zero, not_false_eq_true
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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
⊢ φ ≠ 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]
-- Module: Mathlib.RingTheory.MvPowerSeries.LexOrder
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 φ)),
    φ.lexOrder =
      (↑(WellFounded.min (r := fun (x1 x2 : Lex (σ →₀ ℕ)) ↦ x1 < x2) ⋯
            ((⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) '' Function.support φ) ne) :
        WithTop (Lex (σ →₀ ℕ)))

Tactic:
have hφ' := lexOrder_def_of_ne_zero hφ