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

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).leadingCoeff = x.leadingCoeff

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).leadingCoeff = x.leadingCoeff

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

Tactic:
rw [orderTop_of_ne h, orderTop_of_ne hx, WithTop.coe_eq_coe] at ho

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

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

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

Result:
no goals

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

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

Result:
no goals

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

Tactic:
rw [h, orderTop_zero] at ho

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

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).leadingCoeff = x.leadingCoeff

Tactic:
have ho : (x + y).orderTop = x.orderTop := orderTop_add_eq_left hxy

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
ho : (x + y).orderTop = x.orderTop
⊢ (x + y).leadingCoeff = x.leadingCoeff

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
ho : (x + y).orderTop = x.orderTop
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
by_cases h : x + y = 0

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

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff