awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ Subset (α := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) {a}

Tactic:
Pi.support_single_subset

Premises used: HahnSeries.support, Function.update, Pi.support_single_subset, Pi.single, dite
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ Subset (α := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) {a}

Tactic:
exact Pi.support_single_subset

Premises used: Pi.support_single_subset
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ Subset (α := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) {a}

Tactic:
classical exact Pi.support_single_subset

Premises used: Pi.support_single_subset
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
b : Γ
h : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) b
⊢ b = a

Tactic:
support_single_subset h

Premises used: Set.Mem, setOf, Set.singleton, HahnSeries.support_single_subset
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
⊢ Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) 0) 0

Tactic:
(single a).map_zero

Premises used: HahnSeries.single, ZeroHom.map_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r s : R
rs : Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
rw : coeff ((single a : (a : R) → R⟦Γ⟧) r) a = s
rw₁ : Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) r) a) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a)
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a) (coeff ((single a : (a : R) → R⟦Γ⟧) s) a)
⊢ r = s

Tactic:
rw [← coeff_single_same a r, ← coeff_single_same a s, rs]

Premises used: HahnSeries.coeff_single_same
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ Ne (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
fun con =>
  h (single_injective a (con.trans single_eq_zero.symm))

Premises used: HahnSeries.single_injective, HahnSeries.single_eq_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (0 : R⟦Γ⟧) ↔ r = 0

Tactic:
map_eq_zero_iff _ <| single_injective a

Premises used: HahnSeries.single_injective, map_eq_zero_iff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
coeff :
  ∀ (g : Γ),
    HahnSeries.coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g =
      HahnSeries.coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
⊢ Eq (α := S⟦Γ⟧) (map ((single a : (a : R) → R⟦Γ⟧) r) f) ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r))

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
g : Γ
pos :
  ∀ (h : g = a),
    coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
neg :
  ∀ (h : ¬g = a),
    coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g
⊢ coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g

Tactic:
by_cases h : g = a
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
g : Γ
h : g = a
⊢ coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
inst_2 : Zero S
f : ZeroHom R S
g : Γ
h : ¬g = a
⊢ coeff (map ((single a : (a : R) → R⟦Γ⟧) r) f) g = coeff ((single a : (a : S) → S⟦Γ⟧) ((f : (a : R) → S) r)) g

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
obtain : ∀ (r s : R) (rs : r ≠ s), ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y

Tactic:
obtain ⟨r, s, rs⟩ := exists_pair_ne R

Premises used: exists_pair_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabit : ∀ (inhabited_h : Inhabited Γ), ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y

Tactic:
inhabit Γ
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y

Tactic:
⟨single default r, single default s, fun con => rs ?_⟩

Premises used: Inhabited.default, HahnSeries.single, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
refine :
  ∀ (con : Eq (α := R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)),
    r = s
⊢ ∃ (x : R⟦Γ⟧) (y : R⟦Γ⟧), x ≠ y

Tactic:
refine ⟨single default r, single default s, fun con => rs ?_⟩
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r_1 : R
inst_2 : Nonempty Γ
inst_3 : Nontrivial R
r s : R
rs : r ≠ s
inhabited_h : Inhabited Γ
con : Eq (α := R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single default : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
rw : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) r) default = s
rw₁ : coeff.{u_1, u_3} (Γ := Γ) ((single default : (a : R) → R⟦Γ⟧) s) default = s
rw₂ rw₃ : s = s
⊢ r = s

Tactic:
rw [← coeff_single_same (default : Γ) r, con, coeff_single_same]

Premises used: Inhabited.default, HahnSeries.coeff_single_same
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) 0) ⊤

Tactic:
dif_pos rfl

Premises used: HahnSeries.orderTop, dif_pos, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
inst_2 : Subsingleton R
⊢ x.orderTop = ⊤

Tactic:
(Subsingleton.eq_zero x) ▸ orderTop_zero

Premises used: Eq.rec, Subsingleton.eq_zero, Eq.symm, HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop = (↑(⋯.min (s := x.support) ⋯) : WithTop Γ)

Tactic:
dif_neg hx

Premises used: HahnSeries.orderTop, dif_neg
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.orderTop = ⊤ ↔ x = 0

Tactic:
simp [orderTop]

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.orderTop < ⊤ ↔ x ≠ 0

Tactic:
simp [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.orderTop ≠ ⊤ ↔ x ≠ 0

Tactic:
orderTop_eq_top.not

Premises used: Iff.not, HahnSeries.orderTop_eq_top
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : g ∈ x.support
hx : ∀ g' ∈ x.support, g ≤ g'
rw : (↑(⋯.min (s := x.support) ⋯) : WithTop Γ) = (↑g : WithTop Γ)
rw₁ rw₂ : (↑g : WithTop Γ) = (↑g : WithTop Γ)
⊢ x.orderTop = (↑g : WithTop Γ)

Tactic:
rw [orderTop_of_ne_zero <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
    x.isWF_support.min_eq_of_le hg hx]

Premises used: HahnSeries.support_nonempty_iff, HahnSeries.orderTop_of_ne_zero, Set.IsWF.min_eq_of_le, Iff.mp, Set.nonempty_of_mem, HahnSeries.isWF_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop.untop ⋯ = ⋯.min (s := x.support) ⋯

Tactic:
WithTop.coe_inj.mp ((WithTop.coe_untop (orderTop x) (orderTop_ne_top.2 hx)).trans
    (orderTop_of_ne_zero hx))

Premises used: WithTop.coe_inj, Iff.mpr, HahnSeries.orderTop_ne_top, WithTop.coe_untop, HahnSeries.orderTop, HahnSeries.orderTop_of_ne_zero, Iff.mp, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
⊢ x.orderTop ≠ ⊤

Tactic:
simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]

Premises used: ne_eq, WithTop.coe_ne_top, not_false_eq_true
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
⊢ x.orderTop ≠ ⊤

Tactic:
have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
h : x.orderTop ≠ ⊤
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := orderTop_ne_top.1 h
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = (↑g : WithTop Γ)
h : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ ⋯.min (s := x.support) ⋯ = g

Tactic:
rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hg

Premises used: WithTop.coe_eq_coe, HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min (s := x.support) ⋯ = g
rw : x.coeff (⋯.min (s := x.support) ⋯) ≠ 0
⊢ x.coeff g ≠ 0

Tactic:
rw [← hg]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min (s := x.support) ⋯ = g
⊢ x.coeff (⋯.min (s := x.support) ⋯) ≠ 0

Tactic:
x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Premises used: HahnSeries.support, Iff.mpr, Set.Mem, setOf, Set.IsWF.min_mem, HahnSeries.support_nonempty_iff, Function.support, HahnSeries.isWF_support, Not
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min (s := x.support) ⋯ = g
⊢ x.coeff (⋯.min (s := x.support) ⋯) ≠ 0

Tactic:
exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Premises used: Iff.mpr, Set.IsWF.min_mem, HahnSeries.support_nonempty_iff, HahnSeries.isWF_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hx : x.coeff i = 0
⊢ x.orderTop ≠ (↑i : WithTop Γ)

Tactic:
fun h ↦ coeff_orderTop_ne h hx

Premises used: HahnSeries.coeff_orderTop_ne, Not
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
R : Type u_3
inst : Zero R
Γ : Type u_5
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
rw : ⋯.min (s := x.support) ⋯ ≤ g
⊢ x.orderTop ≤ (↑g : WithTop Γ)

Tactic:
rw [orderTop_of_ne_zero (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]

Premises used: HahnSeries.ne_zero_of_coeff_ne_zero, HahnSeries.orderTop_of_ne_zero, WithTop.coe_le_coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
R : Type u_3
inst : Zero R
Γ : Type u_5
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min (s := x.support) ⋯ ≤ g

Tactic:
Set.IsWF.min_le _ _ ((mem_support _ _).2 h)

Premises used: Iff.mpr, Set.IsWF.min_le, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
R : Type u_3
inst : Zero R
Γ : Type u_5
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min (s := x.support) ⋯ ≤ g

Tactic:
exact Set.IsWF.min_le _ _ ((mem_support _ _).2 h)

Premises used: Iff.mpr, Set.IsWF.min_le, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r) = (↑a : WithTop Γ)

Tactic:
(orderTop_of_ne_zero (single_ne_zero h)).trans
    (WithTop.coe_inj.mpr (support_single_subset
      ((single a r).isWF_support.min_mem (support_nonempty_iff.2 (single_ne_zero h)))))

Premises used: WithTop.coe_inj, Iff.mpr, HahnSeries.single, Set.IsWF.min_mem, HahnSeries.support_nonempty_iff, HahnSeries.orderTop_of_ne_zero, HahnSeries.support_single_subset, HahnSeries.single_ne_zero, HahnSeries.isWF_support, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
pos : ∀ (hr : r = 0), (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
neg : ∀ (hr : ¬r = 0), (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)
⊢ (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
hr : r = 0
⊢ (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)

Tactic:
simp only [hr, map_zero, orderTop_zero, le_top]

Premises used: map_zero, le_top, HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
hr : ¬r = 0
neg neg₁ : (↑a : WithTop Γ) ≤ (↑a : WithTop Γ)
⊢ (↑a : WithTop Γ) ≤ orderTop.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)

Tactic:
rw [orderTop_single hr]

Premises used: HahnSeries.orderTop_single
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
r : R
g g' : Γ
hgg' : g < g'
⊢ (↑g : WithTop Γ) < orderTop.{u_1, u_3} (R := R) ((single g' : (a : R) → R⟦Γ⟧) r)

Tactic:
lt_of_lt_of_le (WithTop.coe_lt_coe.mpr hgg') orderTop_single_le

Premises used: Iff.mpr, HahnSeries.orderTop_single_le, WithTop.coe_lt_coe, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hi : (↑i : WithTop Γ) < x.orderTop
inl : ∀ (hi : (↑i : WithTop Γ) < orderTop.{u_1, u_3} (R := R) 0), Eq.{u_3 + 1} (α := R) (coeff 0 i) 0
inr : ∀ (hx : x ≠ 0), x.coeff i = 0
⊢ x.coeff i = 0

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
i : Γ
hi : (↑i : WithTop Γ) < orderTop.{u_1, u_3} (R := R) 0
⊢ Eq.{u_3 + 1} (α := R) (coeff 0 i) 0

Tactic:
coeff_zero

Premises used: HahnSeries.coeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
i : Γ
hi : (↑i : WithTop Γ) < orderTop.{u_1, u_3} (R := R) 0
⊢ Eq.{u_3 + 1} (α := R) (coeff 0 i) 0

Tactic:
exact coeff_zero

Premises used: HahnSeries.coeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hi : (↑i : WithTop Γ) < x.orderTop
hx : x ≠ 0
inr : ∀ (hi : x.coeff i ≠ 0), ¬(↑i : WithTop Γ) < x.orderTop
⊢ x.coeff i = 0

Tactic:
contrapose! hi
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ i ∈ x.support

Tactic:
rw [← mem_support] at hi

Premises used: HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
inr : ¬i < ⋯.min (s := x.support) ⋯
⊢ ¬(↑i : WithTop Γ) < x.orderTop

Tactic:
rw [orderTop_of_ne_zero hx, WithTop.coe_lt_coe]

Premises used: HahnSeries.orderTop_of_ne_zero, WithTop.coe_lt_coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min (s := x.support) ⋯

Tactic:
Set.IsWF.not_lt_min _ _ hi

Premises used: Set.IsWF.not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min (s := x.support) ⋯

Tactic:
exact Set.IsWF.not_lt_min _ _ hi

Premises used: Set.IsWF.not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) 0

Tactic:
simp [leadingCoeff]

Premises used: HahnSeries.leadingCoeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.leadingCoeff = x.coeff (x.orderTop.untop ⋯)

Tactic:
simp [leadingCoeff, orderTop, hx]

Premises used: HahnSeries.orderTop, HahnSeries.leadingCoeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
inl : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) 0 ↔ Eq (α := R⟦Γ⟧) 0 0
inr : ∀ (hx : x ≠ 0), x.leadingCoeff = 0 ↔ x = 0
⊢ x.leadingCoeff = 0 ↔ x = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
⊢ Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) 0 ↔ Eq (α := R⟦Γ⟧) 0 0

Tactic:
simp [leadingCoeff_of_ne_zero, coeff_orderTop_ne, *]

Premises used: HahnSeries.coeff_orderTop_ne, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.leadingCoeff = 0 ↔ x = 0

Tactic:
simp [leadingCoeff_of_ne_zero, coeff_orderTop_ne, *]

Premises used: HahnSeries.coeff_orderTop_ne, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
⊢ x.leadingCoeff ≠ 0 ↔ x ≠ 0

Tactic:
leadingCoeff_eq_zero.not

Premises used: Iff.not, HahnSeries.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
pos : ∀ (h : r = 0), leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
neg : ∀ (h : ¬r = 0), leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r

Tactic:
by_cases h : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r = 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r

Tactic:
simp [leadingCoeff, h]

Premises used: HahnSeries.leadingCoeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : ¬r = 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single a : (a : R) → R⟦Γ⟧) r) = r

Tactic:
simp [leadingCoeff, h]

Premises used: HahnSeries.leadingCoeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx : x.orderTop ≠ ⊤
⊢ x ≠ 0

Tactic:
rw [orderTop_ne_top] at hx

Premises used: HahnSeries.orderTop_ne_top
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
hx_1 : x.orderTop ≠ ⊤
hx : x ≠ 0
rw : x.coeff (x.orderTop.untop hx_1) = x.coeff (x.orderTop.untop ⋯)
rw₁ rw₂ : x.coeff (⋯.min (s := x.support) ⋯) = x.coeff (⋯.min (s := x.support) ⋯)
⊢ x.coeff (x.orderTop.untop hx_1) = x.leadingCoeff

Tactic:
rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]

Premises used: Iff.mpr, WithTop.untop_eq_iff, HahnSeries.orderTop_of_ne_zero, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 0) 0

Tactic:
dif_pos rfl

Premises used: HahnSeries.order, dif_pos, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.order = ⋯.min (s := x.support) ⋯

Tactic:
dif_neg hx

Premises used: HahnSeries.order, dif_neg
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
x : R⟦Γ⟧
inst_2 : Zero Γ
hx : x ≠ 0
rw : (↑(⋯.min (s := x.support) ⋯) : WithTop Γ) = x.orderTop
rw₁ rw₂ : (↑(⋯.min (s := x.support) ⋯) : WithTop Γ) = (↑(⋯.min (s := x.support) ⋯) : WithTop Γ)
⊢ (↑x.order : WithTop Γ) = x.orderTop

Tactic:
rw [order_of_ne hx, orderTop_of_ne_zero hx]

Premises used: HahnSeries.orderTop_of_ne_zero, HahnSeries.order_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
⊢ x = 0 → x.coeff x.order = 0

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
refine : ∀ (hx : ¬x = 0), ¬x.coeff x.order = 0
⊢ x.coeff x.order = 0 ↔ x = 0

Tactic:
refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
rw : ¬x.coeff (⋯.min (s := x.support) ⋯) = 0
⊢ ¬x.coeff x.order = 0

Tactic:
rw [order_of_ne hx]

Premises used: HahnSeries.order_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff (⋯.min (s := x.support) ⋯) = 0

Tactic:
x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Premises used: HahnSeries.support, Iff.mpr, Set.Mem, setOf, Set.IsWF.min_mem, HahnSeries.support_nonempty_iff, Function.support, HahnSeries.isWF_support, Not
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff (⋯.min (s := x.support) ⋯) = 0

Tactic:
exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Premises used: Iff.mpr, Set.IsWF.min_mem, HahnSeries.support_nonempty_iff, HahnSeries.isWF_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.coeff x.order ≠ 0

Tactic:
coeff_order_eq_zero.not.2 hx

Premises used: Iff.mpr, Iff.not, HahnSeries.coeff_order_eq_zero