case pos
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : x = 0
⊢ min (order x) (order y) ≤ order (x + y)

case neg
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min (order x) (order y) ≤ order (x + y)
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
⊢ min (order x) (order y) ≤ order (x + y)
by_cases hx : x = 0
case pos
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (order x) (order y) ≤ order (x + y)

case neg
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (order x) (order y) ≤ order (x + y)
case neg
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min (order x) (order y) ≤ order (x + y)
by_cases hy : y = 0
case neg
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x)))
      (Set.IsWf.min (_ : Set.IsWf (support y)) (_ : Set.Nonempty (support y))) ≤
    Set.IsWf.min (_ : Set.IsWf (support (x + y))) (_ : Set.Nonempty (support (x + y)))
case neg
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (order x) (order y) ≤ order (x + y)
rw [order_of_ne hx, order_of_ne hy, order_of_ne hxy]
case neg.refine'_1
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x)))
      (Set.IsWf.min (_ : Set.IsWf (support y)) (_ : Set.Nonempty (support y))) =
    Set.IsWf.min ?neg.refine'_2✝ ?neg.refine'_3✝

case neg.refine'_2
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ Set.IsWf (support x ∪ support y)

case neg.refine'_3
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ Set.Nonempty (support x ∪ support y)
case neg
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x)))
      (Set.IsWf.min (_ : Set.IsWf (support y)) (_ : Set.Nonempty (support y))) ≤
    Set.IsWf.min (_ : Set.IsWf (support (x + y))) (_ : Set.Nonempty (support (x + y)))
refine' le_of_eq_of_le _ (Set.IsWf.min_le_min_of_subset (support_add_subset (x := x) (y := y)))
no goals
case neg.refine'_1
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x)))
      (Set.IsWf.min (_ : Set.IsWf (support y)) (_ : Set.Nonempty (support y))) =
    Set.IsWf.min ?neg.refine'_2✝ ?neg.refine'_3✝

case neg.refine'_2
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ Set.IsWf (support x ∪ support y)

case neg.refine'_3
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ Set.Nonempty (support x ∪ support y)
. exact (Set.IsWf.min_union _ _ _ _).symm
no goals
case pos
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : x = 0
⊢ min (order x) (order y) ≤ order (x + y)
simp [hx]
no goals
case pos
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (order x) (order y) ≤ order (x + y)
simp [hy]
no goals
case neg.refine'_1
Γ✝ : Type ?u.666994
R : Type u_2
inst✝² : PartialOrder Γ✝
inst✝¹ : AddMonoid R
Γ : Type u_1
inst✝ : LinearOrderedCancelAddCommMonoid Γ
x y : HahnSeries Γ R
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x)))
      (Set.IsWf.min (_ : Set.IsWf (support y)) (_ : Set.Nonempty (support y))) =
    Set.IsWf.min ?neg.refine'_2✝ ?neg.refine'_3✝
exact (Set.IsWf.min_union _ _ _ _).symm