no goals
ι : Type u_2
β : ι → Type ?u.33701
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
α : Type u_1
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : Preorder α
f : ι → α
i j : ι
h₁ : i < j
h₂ : f j < f i
⊢ (fun x x_1 x_2 => x_1 < x_2) i (↑toLex (f ∘ ↑(Equiv.swap i j)) i) (↑toLex f i)
simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂