n : ℕ
α : Type uu
inst✝ : Preorder α
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i j : Fin (length (ofFn f))),
      i < j → r (f (↑(Fin.cast (_ : length (ofFn f) = n)) i)) (f (↑(Fin.cast (_ : length (ofFn f) = n)) j))) ↔
    ∀ ⦃a b : Fin n⦄, a < b → r (f a) (f b)
n : ℕ
α : Type uu
inst✝ : Preorder α
f : Fin n → α
r : α → α → Prop
⊢ Sorted r (ofFn f) ↔ ((fun x x_1 => x < x_1) ⇒ r) f f
simp_rw [Sorted, pairwise_iff_get, get_ofFn, Relator.LiftFun]
no goals
n : ℕ
α : Type uu
inst✝ : Preorder α
f : Fin n → α
r : α → α → Prop
⊢ (∀ (i j : Fin (length (ofFn f))),
      i < j → r (f (↑(Fin.cast (_ : length (ofFn f) = n)) i)) (f (↑(Fin.cast (_ : length (ofFn f) = n)) j))) ↔
    ∀ ⦃a b : Fin n⦄, a < b → r (f a) (f b)
exact Iff.symm (Fin.cast _).surjective.forall₂