-- Mathlib/Order/RelSeries.lean
/--
In ℕ, two entries in an `LTSeries` differ by at least the difference of their indices.
(Expressed in a way that avoids subtraction).
-/
lemma apply_add_index_le_apply_add_index_nat (p : LTSeries ℕ) (i j : Fin (p.length + 1))
    (hij : i ≤ j) : p i + j ≤ p j + i

Proof state:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩

Tactic:
simp only at *

Result:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i

Proof state:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i

Tactic:
induction j, hij using Nat.le_induction with
| base => simp
| succ j _hij ih =>
  specialize ih (Nat.lt_of_succ_lt hj)
  have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by omega⟩
  norm_cast at *; omega

Result:
no goals

Proof state:
case base
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : i < p.length + 1
⊢ p.toFun ⟨i, hi⟩ + i ≤ p.toFun ⟨i, hj⟩ + i

Tactic:
simp

Result:
no goals

Proof state:
p : LTSeries ℕ
i✝ j : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
hij : ⟨i, hi⟩ ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun j + ↑⟨i, hi⟩

Tactic:
have ⟨j, hj⟩ := j

Result:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : ⟨i, hi⟩ ≤ ⟨j, hj⟩
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩

Proof state:
p : LTSeries ℕ
i j : Fin (p.length + 1)
hij : i ≤ j
⊢ p.toFun i + ↑j ≤ p.toFun j + ↑i

Tactic:
have ⟨i, hi⟩ := i

Result:
p : LTSeries ℕ
i✝ j : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
hij : ⟨i, hi⟩ ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun j + ↑⟨i, hi⟩

Proof state:
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
⊢ j < p.length

Tactic:
omega

Result:
no goals

Proof state:
case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
ih : ∀ (hj : j < p.length + 1), p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i
hj : j + 1 < p.length + 1
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Tactic:
specialize ih (Nat.lt_of_succ_lt hj)

Result:
case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Proof state:
case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Tactic:
have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by omega⟩

Result:
case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
step : p.toFun ⟨j, ⋯⟩ < p.toFun ⟨j + 1, ⋯⟩
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Proof state:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : ⟨i, hi⟩ ≤ ⟨j, hj⟩
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩

Tactic:
simp only [Fin.mk_le_mk] at hij

Result:
p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑⟨j, hj⟩ ≤ p.toFun ⟨j, hj⟩ + ↑⟨i, hi⟩

Proof state:
case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
step : p.toFun ⟨j, ⋯⟩ < p.toFun ⟨j + 1, ⋯⟩
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Tactic:
omega

Result:
no goals