awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
pos : ∀ (hy : y = 0), min x.order y.order ≤ (x + y).order
neg : ∀ (hy : ¬y = 0), min x.order y.order ≤ (x + y).order
⊢ min x.order y.order ≤ (x + y).order

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
neg : min (⋯.min (s := x.support) ⋯) (⋯.min (s := y.support) ⋯) ≤ ⋯.min (s := (x + y).support) ⋯
⊢ min x.order y.order ≤ (x + y).order

Tactic:
rw [order_of_ne hx, order_of_ne hy, order_of_ne hxy]

Premises used: HahnSeries.order_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (⋯.min (s := x.support) ⋯) (⋯.min (s := y.support) ⋯) ≤ ⋯.min (s := (x + y).support) ⋯

Tactic:
HahnSeries.min_le_min_add hx hy hxy

Premises used: HahnSeries.min_le_min_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (⋯.min (s := x.support) ⋯) (⋯.min (s := y.support) ⋯) ≤ ⋯.min (s := (x + y).support) ⋯

Tactic:
exact HahnSeries.min_le_min_add hx hy hxy

Premises used: HahnSeries.min_le_min_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := orderTop_ne_top.1 hxy.ne_top
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
rw : x.coeff g ≠ 0
⊢ (x + y).coeff g ≠ 0

Tactic:
rw [coeff_add, coeff_eq_zero_of_lt_orderTop (lt_of_eq_of_lt (orderTop_of_ne_zero hx).symm hxy),
      add_zero]

Premises used: HahnSeries.orderTop_of_ne_zero, lt_of_eq_of_lt, HahnSeries.coeff_add, add_zero, Eq.symm, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
⊢ x.coeff g ≠ 0

Tactic:
coeff_orderTop_ne (orderTop_of_ne_zero hx)

Premises used: HahnSeries.coeff_orderTop_ne, HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
⊢ x.coeff g ≠ 0

Tactic:
exact coeff_orderTop_ne (orderTop_of_ne_zero hx)

Premises used: HahnSeries.coeff_orderTop_ne, HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
⊢ (x + y).coeff g ≠ 0

Tactic:
have hcxyne : (x + y).coeff g ≠ 0 := by
    rw [coeff_add, coeff_eq_zero_of_lt_orderTop (lt_of_eq_of_lt (orderTop_of_ne_zero hx).symm hxy),
      add_zero]
    exact coeff_orderTop_ne (orderTop_of_ne_zero hx)
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
rw : (x + y).orderTop ≤ (↑(⋯.min (s := x.support) ⋯) : WithTop Γ)
⊢ (x + y).orderTop ≤ x.orderTop

Tactic:
rw [orderTop_of_ne_zero hx]

Premises used: HahnSeries.orderTop_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ (↑(⋯.min (s := x.support) ⋯) : WithTop Γ)

Tactic:
orderTop_le_of_coeff_ne_zero hcxyne

Premises used: HahnSeries.orderTop_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ (↑(⋯.min (s := x.support) ⋯) : WithTop Γ)

Tactic:
exact orderTop_le_of_coeff_ne_zero hcxyne

Premises used: HahnSeries.orderTop_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ x.orderTop

Tactic:
have hxyx : (x + y).orderTop ≤ x.orderTop := by
    rw [orderTop_of_ne_zero hx]
    exact orderTop_le_of_coeff_ne_zero hcxyne
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
hxyx : (x + y).orderTop ≤ x.orderTop
⊢ (x + y).orderTop = x.orderTop

Tactic:
le_antisymm hxyx (le_of_eq_of_le (min_eq_left_of_lt hxy).symm min_orderTop_le_orderTop_add)

Premises used: min_eq_left_of_lt, le_antisymm, le_of_eq_of_le, Eq.symm, HahnSeries.min_orderTop_le_orderTop_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min (s := x.support) ⋯
hcxyne : (x + y).coeff g ≠ 0
hxyx : (x + y).orderTop ≤ x.orderTop
⊢ (x + y).orderTop = x.orderTop

Tactic:
exact le_antisymm hxyx (le_of_eq_of_le (min_eq_left_of_lt hxy).symm min_orderTop_le_orderTop_add)

Premises used: min_eq_left_of_lt, le_antisymm, le_of_eq_of_le, Eq.symm, HahnSeries.min_orderTop_le_orderTop_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).orderTop = y.orderTop

Tactic:
simpa [← map_add, ← AddOpposite.op_add, hxy] using orderTop_add_eq_left
    (x := addOppositeEquiv.symm (.op y))
    (y := addOppositeEquiv.symm (.op x))

Premises used: map_add, AddOpposite.op_add, HahnSeries.orderTop_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
⊢ (x + y).orderTop = x.orderTop

Tactic:
have ho : (x + y).orderTop = x.orderTop := orderTop_add_eq_left hxy
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
pos : ∀ (h : x + y = 0), (x + y).leadingCoeff = x.leadingCoeff
neg : ∀ (h : ¬x + y = 0), (x + y).leadingCoeff = x.leadingCoeff
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
by_cases h : x + y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ ⊤ = x.orderTop

Tactic:
rw [h, orderTop_zero] at ho

Premises used: HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
ho₁ : ⊤ = x.orderTop
⊢ x + y = 0

Tactic:
rw [h, orderTop_zero] at ho

Premises used: HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : ⊤ = x.orderTop
h : x + y = 0
pos : leadingCoeff.{u_8, u_3} (Γ := Γ) 0 = x.leadingCoeff
pos₁ pos₂ : Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_8, u_3} (Γ := Γ) 0) (leadingCoeff.{u_8, u_3} (Γ := Γ) 0)
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
rw [h, orderTop_eq_top.mp ho.symm]

Premises used: HahnSeries.orderTop_eq_top, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
neg : x.coeff (x.orderTop.untop ⋯) + y.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
simp_rw [leadingCoeff_of_ne_zero h, leadingCoeff_of_ne_zero hx, ho, coeff_add]

Premises used: HahnSeries.coeff_add, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (↑(x.orderTop.untop ⋯) : WithTop Γ) < y.orderTop

Tactic:
simpa using hxy
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
neg : x.coeff (x.orderTop.untop ⋯) + 0 = x.coeff (x.orderTop.untop ⋯)
neg₁ neg₂ : x.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
⊢ x.coeff (x.orderTop.untop ⋯) + y.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)

Tactic:
rw [coeff_eq_zero_of_lt_orderTop (x := y) (by simpa using hxy), add_zero]

Premises used: add_zero, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).leadingCoeff = y.leadingCoeff

Tactic:
simpa [← map_add, ← AddOpposite.op_add, hxy] using leadingCoeff_add_eq_left
    (x := addOppositeEquiv.symm (.op y))
    (y := addOppositeEquiv.symm (.op x))

Premises used: map_add, AddOpposite.op_add, HahnSeries.leadingCoeff_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : Zero Γ
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
by_contra : ∀ (h : x = 0), False
⊢ x ≠ 0

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : Zero Γ
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x = 0
⊢ 0 = y

Tactic:
simp only [h, order_zero, leadingCoeff_zero, map_zero, add_zero] at hxy

Premises used: map_zero, HahnSeries.order_zero, add_zero, HahnSeries.leadingCoeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : Zero Γ
x y : R⟦Γ⟧
hy : y ≠ 0
h : x = 0
hxy : 0 = y
⊢ False

Tactic:
hy hxy.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : Zero Γ
x y : R⟦Γ⟧
hy : y ≠ 0
h : x = 0
hxy : 0 = y
⊢ False

Tactic:
exact hy hxy.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
inst : PartialOrder Γ
R : Type u_8
inst_1 : AddCancelCommMonoid R
inst_2 : Zero Γ
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
⊢ y.coeff x.order = 0

Tactic:
simpa [← leadingCoeff_eq] using congr(($hxy).coeff x.order)

Premises used: HahnSeries.leadingCoeff_eq
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x.order = y.order
⊢ Ne (α := R⟦Γ⟧) ((single y.order : (a : R) → R⟦Γ⟧) y.leadingCoeff : R⟦Γ⟧) (0 : R⟦Γ⟧)

Tactic:
have hyne : single y.order y.leadingCoeff ≠ 0 := single_ne_zero <| leadingCoeff_ne_zero.mpr hy
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x.order = y.order
hyne : Ne (α := R⟦Γ⟧) ((single y.order : (a : R) → R⟦Γ⟧) y.leadingCoeff : R⟦Γ⟧) (0 : R⟦Γ⟧)
⊢ Ne (α := R⟦Γ⟧) 0 0

Tactic:
rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy, single_eq_zero] at hyne

Premises used: HahnSeries.coeff_order_of_eq_add_single, HahnSeries.leadingCoeff_eq, HahnSeries.single_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x.order = y.order
hyne : Ne (α := R⟦Γ⟧) 0 0
⊢ False

Tactic:
hyne rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
h : x.order = y.order
hyne : Ne (α := R⟦Γ⟧) 0 0
⊢ False

Tactic:
exact hyne rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
⊢ x.order ≠ y.order

Tactic:
have : x.order ≠ y.order := by
    intro h
    have hyne : single y.order y.leadingCoeff ≠ 0 := single_ne_zero <| leadingCoeff_ne_zero.mpr hy
    rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy, single_eq_zero] at hyne
    exact hyne rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order < y.order

Tactic:
lt_of_le_of_ne ?_ this

Premises used: lt_of_le_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
refine : x.order ≤ y.order
⊢ x.order < y.order

Tactic:
refine lt_of_le_of_ne ?_ this

Premises used: lt_of_le_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
simp : ⋯.min (s := x.support) ⋯ ≤ ⋯.min (s := y.support) ⋯
⊢ x.order ≤ y.order

Tactic:
simp only [order, ne_zero_of_eq_add_single hxy hy, ↓reduceDIte, hy]

Premises used: HahnSeries.order, reduceDIte, HahnSeries.ne_zero_of_eq_add_single
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
⊢ ⋯.min (s := x.support) ⋯ ≤ ⋯.min (s := y.support) ⋯

Tactic:
Set.IsWF.min_le_min_of_subset fun g hg ↦ ?_

Premises used: Set.IsWF.min_le_min_of_subset
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
refine : ∀ (g : Γ) (hg : g ∈ y.support), g ∈ x.support
⊢ ⋯.min (s := x.support) ⋯ ≤ ⋯.min (s := y.support) ⋯

Tactic:
refine Set.IsWF.min_le_min_of_subset fun g hg ↦ ?_

Premises used: Set.IsWF.min_le_min_of_subset
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
inl : ∀ (hg : x.order ∈ y.support), x.order ∈ x.support
inr : ∀ (hgx : g ≠ x.order), g ∈ x.support
⊢ g ∈ x.support

Tactic:
obtain rfl | hgx := eq_or_ne g x.order

Premises used: HahnSeries.order, eq_or_ne, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
hg : x.order ∈ y.support
⊢ x.order ∈ x.support

Tactic:
simpa using coeff_order_eq_zero.not.2 <| ne_zero_of_eq_add_single hxy hy

Premises used: Iff.mpr, Iff.not, HahnSeries.coeff_order_eq_zero, HahnSeries.ne_zero_of_eq_add_single
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
rw rw₁ : x.coeff g = x.coeff g
⊢ x.coeff g = (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)).coeff g

Tactic:
rw [← hxy]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ x.coeff g = (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)).coeff g

Tactic:
have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this_1 : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)).coeff g
⊢ x.coeff g = y.coeff g

Tactic:
rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this

Premises used: HahnSeries.coeff_single_of_ne, HahnSeries.coeff_add, add_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_8
Γ : Type u_9
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : y ≠ 0
this_1 : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = y.coeff g
⊢ g ∈ x.support

Tactic:
simpa [this] using hg
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
coeff : ∀ (g : Γ'), (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
⊢ embDomain f (x + y) = embDomain f x + embDomain f y

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
pos :
  ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
    (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
neg :
  ∀ (hg : g ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
    (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
by_cases hg : g ∈ Set.range f

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : Membership.mem (γ := Set Γ') (Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g
pos :
  ∀ (a : Γ),
    (embDomain f (x + y)).coeff ((f : (a : Γ) → Γ') a) = (embDomain f x + embDomain f y).coeff ((f : (a : Γ) → Γ') a)
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
a : Γ
⊢ (embDomain f (x + y)).coeff ((f : (a : Γ) → Γ') a) = (embDomain f x + embDomain f y).coeff ((f : (a : Γ) → Γ') a)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
simp [embDomain_notin_range hg]

Premises used: HahnSeries.embDomain_notin_range
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
coeff :
  ∀ (i : Γ),
    HahnSeries.coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y)) i =
      (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
            ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
        i
⊢ (truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
      ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)

Tactic:
ext i
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
pos :
  ∀ (h : i < c),
    coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y)) i =
      (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
            ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
        i
neg :
  ∀ (h : ¬i < c),
    coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y)) i =
      (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
            ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
        i
⊢ coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y)) i =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      i

Tactic:
by_cases h : i < c
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
h : i < c
⊢ coeff ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) (x + y)) i =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x : R⟦Γ⟧)
          ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) y : R⟦Γ⟧)).coeff
      i

Tactic:
simp [h]