R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ order (φ + ψ) = order φ
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
suffices order (φ + ψ) = order φ by
  rw [le_inf_iff, this]
  exact ⟨le_rfl, le_of_lt H⟩
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
this : order (φ + ψ) = order φ
⊢ order φ ≤ order φ ∧ order φ ≤ order ψ
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
this : order (φ + ψ) = order φ
⊢ order (φ + ψ) ≤ order φ ⊓ order ψ
rw [le_inf_iff, this]
no goals
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
this : order (φ + ψ) = order φ
⊢ order φ ≤ order φ ∧ order φ ≤ order ψ
exact ⟨le_rfl, le_of_lt H⟩
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ (∀ (i : ℕ), ↑i = order φ → ↑(coeff R i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < order φ → ↑(coeff R i) (φ + ψ) = 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ order (φ + ψ) = order φ
rw [order_eq]
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ ∀ (i : ℕ), ↑i = order φ → ↑(coeff R i) (φ + ψ) ≠ 0

case right
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ ∀ (i : ℕ), ↑i < order φ → ↑(coeff R i) (φ + ψ) = 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ (∀ (i : ℕ), ↑i = order φ → ↑(coeff R i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < order φ → ↑(coeff R i) (φ + ψ) = 0
constructor
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
i : ℕ
hi : ↑i = order φ
⊢ ↑(coeff R i) (φ + ψ) ≠ 0
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ ∀ (i : ℕ), ↑i = order φ → ↑(coeff R i) (φ + ψ) ≠ 0
intro i hi
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
i : ℕ
H : ↑i < order ψ
hi : ↑i = order φ
⊢ ↑(coeff R i) (φ + ψ) ≠ 0
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
i : ℕ
hi : ↑i = order φ
⊢ ↑(coeff R i) (φ + ψ) ≠ 0
rw [← hi] at H
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
i : ℕ
H : ↑i < order ψ
hi : ↑i = order φ
⊢ ↑(coeff R i) φ ≠ 0
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
i : ℕ
H : ↑i < order ψ
hi : ↑i = order φ
⊢ ↑(coeff R i) (φ + ψ) ≠ 0
rw [(coeff _ _).map_add, coeff_of_lt_order i H, add_zero]
no goals
case left
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
i : ℕ
H : ↑i < order ψ
hi : ↑i = order φ
⊢ ↑(coeff R i) φ ≠ 0
exact (order_eq_nat.1 hi.symm).1
case right
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
i : ℕ
hi : ↑i < order φ
⊢ ↑(coeff R i) (φ + ψ) = 0
case right
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
⊢ ∀ (i : ℕ), ↑i < order φ → ↑(coeff R i) (φ + ψ) = 0
intro i hi
no goals
case right
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
_h : order φ ≠ order ψ
H : order φ < order ψ
i : ℕ
hi : ↑i < order φ
⊢ ↑(coeff R i) (φ + ψ) = 0
rw [(coeff _ _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
  zero_add]