-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem coeff_order_of_eq_add_single {R} [AddCancelCommMonoid R] [Zero Γ] {x y : HahnSeries Γ R}
    (hxy : x = y + single x.order x.leadingCoeff) (h : x ≠ 0) :
    y.coeff x.order = 0

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
⊢ y.coeff x.order = 0

Tactic:
have : xo = x.order := (order_of_ne h).symm

Result:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
⊢ y.coeff x.order = 0

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
⊢ y.coeff x.order = 0

Tactic:
have hx : x.coeff xo = y.coeff xo + (single x.order x.leadingCoeff).coeff xo := by
  nth_rw 1 [hxy, coeff_add]

Result:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : x.coeff xo = y.coeff xo + ((single x.order) x.leadingCoeff).coeff xo
⊢ y.coeff x.order = 0

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : y.coeff x.order = 0
hxx : ((single x.order) x.leadingCoeff).coeff xo = ((single x.order) x.leadingCoeff).leadingCoeff
⊢ y.coeff x.order = 0

Tactic:
exact hx

Result:
no goals

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : x.coeff xo = y.coeff xo + ((single x.order) x.leadingCoeff).coeff xo
⊢ ((single x.order) x.leadingCoeff).coeff xo = ((single x.order) x.leadingCoeff).leadingCoeff

Tactic:
simp [leadingCoeff_of_single, coeff_single, this]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
⊢ x.coeff xo = y.coeff xo + ((single x.order) x.leadingCoeff).coeff xo

Tactic:
nth_rw 1 [hxy, coeff_add]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : x.coeff xo = y.coeff xo + ((single x.order) x.leadingCoeff).coeff xo
⊢ y.coeff x.order = 0

Tactic:
have hxx :
    (single x.order x.leadingCoeff).coeff xo = (single x.order x.leadingCoeff).leadingCoeff := by
  simp [leadingCoeff_of_single, coeff_single, this]

Result:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : x.coeff xo = y.coeff xo + ((single x.order) x.leadingCoeff).coeff xo
hxx : ((single x.order) x.leadingCoeff).coeff xo = ((single x.order) x.leadingCoeff).leadingCoeff
⊢ y.coeff x.order = 0

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
⊢ y.coeff x.order = 0

Tactic:
let xo := x.isWF_support.min (support_nonempty_iff.2 h)

Result:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
⊢ y.coeff x.order = 0

Proof state:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : x.coeff xo = y.coeff xo + ((single x.order) x.leadingCoeff).coeff xo
hxx : ((single x.order) x.leadingCoeff).coeff xo = ((single x.order) x.leadingCoeff).leadingCoeff
⊢ y.coeff x.order = 0

Tactic:
rw [← (leadingCoeff_of_ne h), hxx, leadingCoeff_of_single, self_eq_add_left, this] at hx

Result:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
h : x ≠ 0
xo : Γ := ⋯.min ⋯
this : xo = x.order
hx : y.coeff x.order = 0
hxx : ((single x.order) x.leadingCoeff).coeff xo = ((single x.order) x.leadingCoeff).leadingCoeff
⊢ y.coeff x.order = 0