R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
⊢ order (φ + ψ) = order φ ⊓ order ψ
refine' le_antisymm _ (le_order_add _ _)
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : order φ < order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ

case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
by_cases H₁ : order φ < order ψ
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
H₂ : order ψ < order φ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ

case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
H₂ : ¬order ψ < order φ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
by_cases H₂ : order ψ < order φ
case neg.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
H₂ : ¬order ψ < order φ
⊢ False
case neg
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
H₂ : ¬order ψ < order φ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
exfalso
no goals
case neg.h
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
H₂ : ¬order ψ < order φ
⊢ False
exact h (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁))
no goals
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : order φ < order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
apply order_add_of_order_eq.aux _ _ h H₁
no goals
case pos
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
h : order φ ≠ order ψ
H₁ : ¬order φ < order ψ
H₂ : order ψ < order φ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
simpa only [add_comm, inf_comm] using order_add_of_order_eq.aux _ _ h.symm H₂