-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem orderTop_add_orderTop_le_orderTop_mul {Γ} [LinearOrderedCancelAddCommMonoid Γ]
    [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} :
    x.orderTop + y.orderTop ≤ (x * y).orderTop

Proof state:
case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
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_add,
  WithTop.coe_le_coe, ← Set.IsWF.min_add]

Result:
case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x * y = 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Proof state:
case pos
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
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:
case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
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
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : y = 0
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : x = 0
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Proof state:
case pos
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
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
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x * y = 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support

Result:
no goals

Proof state:
case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
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
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
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
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x * y = 0
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Proof state:
case pos
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
hx : ¬x = 0
hy : y = 0
⊢ x.orderTop + y.orderTop ≤ (x * y).orderTop

Tactic:
simp [hy]

Result:
no goals