-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem orderTop_add_eq_left {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R}
    (hxy : x.orderTop < y.orderTop) : (x + y).orderTop = x.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
⊢ (x + y).orderTop = x.orderTop

Tactic:
have hx : x ≠ 0 := ne_zero_iff_orderTop.mpr hxy.ne_top

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
⊢ (x + y).orderTop = x.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
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)

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
⊢ (x + y).orderTop = x.orderTop

Tactic:
let g : Γ := Set.IsWF.min x.isWF_support (support_nonempty_iff.2 hx)

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ (x + y).orderTop = x.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ ↑(⋯.min ⋯)

Tactic:
exact orderTop_le_of_coeff_ne_zero hcxyne

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop = x.orderTop

Tactic:
have hxyx : (x + y).orderTop ≤ x.orderTop := by
  rw [orderTop_of_ne hx]
  exact orderTop_le_of_coeff_ne_zero hcxyne

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
hxyx : (x + y).orderTop ≤ x.orderTop
⊢ (x + y).orderTop = x.orderTop

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ (x + y).coeff g ≠ 0

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

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ x.coeff g ≠ 0

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ x.coeff g ≠ 0

Tactic:
exact coeff_orderTop_ne (orderTop_of_ne hx)

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ x.orderTop

Tactic:
rw [orderTop_of_ne hx]

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop ≤ ↑(⋯.min ⋯)

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ (x + y).orderTop = x.orderTop

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 hx).symm hxy),
    add_zero]
  exact coeff_orderTop_ne (orderTop_of_ne hx)

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
hcxyne : (x + y).coeff g ≠ 0
⊢ (x + y).orderTop = x.orderTop