-- Mathlib/Order/Fin/Basic.lean
/-- If `e` is an `orderIso` between `Fin n` and `Fin m`, then `n = m` and `e` is the identity
map. In this lemma we state that for each `i : Fin n` we have `(e i : ℕ) = (i : ℕ)`. -/
@[simp] lemma coe_orderIso_apply (e : Fin n ≃o Fin m) (i : Fin n) : (e i : ℕ) = i

Proof state:
case mk
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
induction' i using Nat.strong_induction_on with i h

Result:
case mk.h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Proof state:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i

Tactic:
have := e.symm.lt_iff_lt.2 (mk_lt_of_lt_val hj)

Result:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < e.symm (e ⟨i, hi⟩)
⊢ j < i

Proof state:
case h.e'_3
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this✝ : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
this : ↑(e.symm ⟨j, ⋯⟩) < i
⊢ j = ↑(e.symm ⟨j, ⋯⟩)

Tactic:
simpa using h _ this (e.symm _).is_lt

Result:
no goals

Proof state:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this✝ : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
this : ↑(e.symm ⟨j, ⋯⟩) < i
⊢ j < i

Tactic:
convert this

Result:
case h.e'_3
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this✝ : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
this : ↑(e.symm ⟨j, ⋯⟩) < i
⊢ j = ↑(e.symm ⟨j, ⋯⟩)

Proof state:
case mk
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = ↑⟨i, hi⟩

Tactic:
dsimp only

Result:
case mk
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Proof state:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
⊢ j < i

Tactic:
have : _ < i := this

Result:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this✝ : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
this : ↑(e.symm ⟨j, ⋯⟩) < i
⊢ j < i

Proof state:
case mk.h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)

Result:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i

case mk.h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Proof state:
case mk.h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
rwa [← h j hj (hj.trans hi), ← lt_iff_val_lt_val, e.lt_iff_lt]

Result:
no goals

Proof state:
m n : ℕ
e : Fin n ≃o Fin m
i : Fin n
⊢ ↑(e i) = ↑i

Tactic:
rcases i with ⟨i, hi⟩

Result:
case mk
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = ↑⟨i, hi⟩

Proof state:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < e.symm (e ⟨i, hi⟩)
⊢ j < i

Tactic:
rw [e.symm_apply_apply] at this

Result:
case mk.h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ m_1 < i, ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
⊢ j < i