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

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order ≤ y.order

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

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Proof state:
case neg
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : ¬g = x.order
⊢ g ∈ x.support

Tactic:
have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]

Result:
case neg
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : ¬g = x.order
this : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g
⊢ g ∈ x.support

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
⊢ g ∈ x.support

Tactic:
by_cases hgx : g = x.order

Result:
case pos
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g = x.order
⊢ g ∈ x.support

case neg
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : ¬g = x.order
⊢ g ∈ x.support

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

Tactic:
have hyne : single y.order y.leadingCoeff ≠ 0 := single_ne_zero <| leadingCoeff_ne_iff.mpr hy

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
hyne : (single y.order) y.leadingCoeff ≠ 0
⊢ False

Proof state:
case neg
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : 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

Result:
no goals

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
hyne : (single y.order) y.leadingCoeff ≠ 0
⊢ False

Tactic:
rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy <| ne_zero_of_eq_add_single hxy hy,
  single_eq_zero] at hyne

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
hyne : 0 ≠ 0
⊢ False

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
h : x.order = y.order
hyne : 0 ≠ 0
⊢ False

Tactic:
exact hyne rfl

Result:
no goals

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ y.support ⊆ x.support

Tactic:
intro g hg

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
⊢ g ∈ x.support

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order < y.order

Tactic:
refine lt_of_le_of_ne ?_ this

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order ≤ y.order

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
this : y.support ⊆ x.support
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset this

Result:
no goals

Proof state:
case pos
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g = x.order
⊢ g ∈ x.support

Tactic:
refine (mem_support x g).mpr ?_

Result:
case pos
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g = x.order
⊢ x.coeff g ≠ 0

Proof state:
case pos
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g = x.order
⊢ x.coeff g ≠ 0

Tactic:
have : x.coeff x.order ≠ 0 := coeff_order_ne_zero <| ne_zero_of_eq_add_single hxy hy

Result:
case pos
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g = x.order
this : x.coeff x.order ≠ 0
⊢ x.coeff g ≠ 0

Proof state:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
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_iff.mpr hy
  rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy <| ne_zero_of_eq_add_single hxy hy,
    single_eq_zero] at hyne
  exact hyne rfl

Result:
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : HahnSeries Γ R
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
⊢ x.order < y.order