case mk
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = ↑{ val := i, isLt := hi }
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : Fin n
⊢ ↑(↑e i) = ↑i
rcases i with ⟨i, hi⟩
case mk
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = i
case mk
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = ↑{ val := i, isLt := hi }
dsimp only
case mk.h
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = i
case mk
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = i
induction' i using Nat.strong_induction_on with i h
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
⊢ j < i

case mk.h.refine'_2
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(↑e { val := i, isLt := hi })
case mk.h
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
⊢ ↑(↑e { val := i, isLt := hi }) = i
refine' le_antisymm (forall_lt_iff_le.1 fun j hj => _) (forall_lt_iff_le.1 fun j hj => _)
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < ↑(OrderIso.symm e) (↑e { val := i, isLt := hi })
⊢ j < i
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
⊢ j < i
have := e.symm.lt_iff_lt.2 (mk_lt_of_lt_val hj)
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
⊢ j < i
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < ↑(OrderIso.symm e) (↑e { val := i, isLt := hi })
⊢ j < i
rw [e.symm_apply_apply] at this
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this✝ : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
this : ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) }) < i
⊢ j < i
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
⊢ j < i
have : _ < i := this
case h.e'_3
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this✝ : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
this : ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) }) < i
⊢ j = ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) })
case mk.h.refine'_1
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this✝ : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
this : ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) }) < i
⊢ j < i
convert this
no goals
case h.e'_3
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < ↑(↑e { val := i, isLt := hi })
this✝ : ↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) } < { val := i, isLt := hi }
this : ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) }) < i
⊢ j = ↑(↑(OrderIso.symm e) { val := j, isLt := (_ : j < m) })
simpa using h _ this (e.symm _).is_lt
no goals
case mk.h.refine'_2
n m : ℕ
α : Type ?u.29565
inst✝ : Preorder α
e : Fin n ≃o Fin m
i✝ : ℕ
hi✝ : i✝ < n
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(↑e { val := m_1, isLt := hi }) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(↑e { val := i, isLt := hi })
rwa [← h j hj (hj.trans hi), ← lt_iff_val_lt_val, e.lt_iff_lt]