-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem min_orderTop_le_orderTop_add {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} :
    min x.orderTop y.orderTop ≤ (x + y).orderTop

Proof state:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Tactic:
by_cases hxy : x + y = 0

Result:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Proof state:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ ⋯.min ⋯ ⊓ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact HahnSeries.min_le_min_add hx hy hxy

Result:
no goals

Proof state:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Tactic:
by_cases hy : y = 0

Result:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Proof state:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Tactic:
simp [hxy]

Result:
no goals

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

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : x = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Proof state:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Tactic:
simp [hy]

Result:
no goals

Proof state:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : x = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ x.orderTop ⊓ y.orderTop ≤ (x + y).orderTop

Tactic:
rw [orderTop_of_ne hx, orderTop_of_ne hy, orderTop_of_ne hxy, ← WithTop.coe_min,
  WithTop.coe_le_coe]

Result:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ ⋯.min ⋯ ⊓ ⋯.min ⋯ ≤ ⋯.min ⋯