case a
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ order (x * y) ≤ order x + order y

case a
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ order x + order y ≤ order (x * y)
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ order (x * y) = order x + order y
apply le_antisymm
case a.h
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ coeff (x * y) (order x + order y) ≠ 0
case a
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ order (x * y) ≤ order x + order y
apply order_le_of_coeff_ne_zero
case a.h
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ coeff x (order x) * coeff y (order y) ≠ 0
case a.h
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ coeff (x * y) (order x + order y) ≠ 0
rw [mul_coeff_order_add_order x y]
no goals
case a.h
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ coeff x (order x) * coeff y (order y) ≠ 0
exact mul_ne_zero (coeff_order_ne_zero hx) (coeff_order_ne_zero hy)
case a
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ Set.IsWf.min (_ : Set.IsWf (support x + support y)) (_ : Set.Nonempty (support x + support y)) ≤
    Set.IsWf.min (_ : Set.IsWf (support (x * y))) (_ : Set.Nonempty (support (x * y)))
case a
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ order x + order y ≤ order (x * y)
rw [order_of_ne hx, order_of_ne hy, order_of_ne (mul_ne_zero hx hy), ← Set.IsWf.min_add]
no goals
case a
Γ✝ : Type ?u.1293056
R : Type u_2
inst✝³ : OrderedCancelAddCommMonoid Γ✝
Γ : Type u_1
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
⊢ Set.IsWf.min (_ : Set.IsWf (support x + support y)) (_ : Set.Nonempty (support x + support y)) ≤
    Set.IsWf.min (_ : Set.IsWf (support (x * y))) (_ : Set.Nonempty (support (x * y)))
exact Set.IsWf.min_le_min_of_subset support_mul_subset_add_support