-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_add_of_order_eq.aux (φ ψ : R⟦X⟧) (_h : order φ ≠ order ψ)
    (H : order φ < order ψ) : order (φ + ψ) ≤ order φ ⊓ order ψ

Proof state:
case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
i : ℕ
hi : ↑i < φ.order
⊢ (coeff R i) (φ + ψ) = 0

Tactic:
rw [(coeff _ _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H),
  zero_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order

Tactic:
exact ⟨le_rfl, le_of_lt H⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
rw [le_inf_iff, this]

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ φ.order ≤ φ.order ∧ φ.order ≤ ψ.order

Proof state:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff R i) (φ + ψ) ≠ 0

Tactic:
rw [(coeff _ _).map_add, coeff_of_lt_order i H, add_zero]

Result:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff R i) φ ≠ 0

Proof state:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff R i) φ ≠ 0

Tactic:
exact (order_eq_nat.1 hi.symm).1

Result:
no goals

Proof state:
case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff R i) (φ + ψ) = 0

Tactic:
intro i hi

Result:
case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
i : ℕ
hi : ↑i < φ.order
⊢ (coeff R i) (φ + ψ) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ (φ + ψ).order = φ.order

Tactic:
rw [order_eq]

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ (∀ (i : ℕ), ↑i = φ.order → (coeff R i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < φ.order → (coeff R i) (φ + ψ) = 0

Proof state:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i = φ.order → (coeff R i) (φ + ψ) ≠ 0

Tactic:
intro i hi

Result:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
i : ℕ
hi : ↑i = φ.order
⊢ (coeff R i) (φ + ψ) ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
suffices order (φ + ψ) = order φ by
  rw [le_inf_iff, this]
  exact ⟨le_rfl, le_of_lt H⟩

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ (φ + ψ).order = φ.order

Proof state:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
i : ℕ
hi : ↑i = φ.order
⊢ (coeff R i) (φ + ψ) ≠ 0

Tactic:
rw [← hi] at H

Result:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff R i) (φ + ψ) ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ (∀ (i : ℕ), ↑i = φ.order → (coeff R i) (φ + ψ) ≠ 0) ∧ ∀ (i : ℕ), ↑i < φ.order → (coeff R i) (φ + ψ) = 0

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i = φ.order → (coeff R i) (φ + ψ) ≠ 0

case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
_h : φ.order ≠ ψ.order
H : φ.order < ψ.order
⊢ ∀ (i : ℕ), ↑i < φ.order → (coeff R i) (φ + ψ) = 0