case mk.mk.mk.mk.left
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
y : α
j : Fin n
hy : (y, j) ∈ graph f
h✝ : x < y
⊢ graph.proj { val := (x, i), property := hx } ≤ graph.proj { val := (y, j), property := hy }

case mk.mk.mk.mk.right
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
j : Fin n
hy : (x, j) ∈ graph f
h✝ : i ≤ j
⊢ graph.proj { val := (x, i), property := hx } ≤ graph.proj { val := (x, j), property := hy }
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone graph.proj
rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (_ | h)
no goals
case mk.mk.mk.mk.left
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
y : α
j : Fin n
hy : (y, j) ∈ graph f
h✝ : x < y
⊢ graph.proj { val := (x, i), property := hx } ≤ graph.proj { val := (y, j), property := hy }
exact le_of_lt ‹_›
no goals
case mk.mk.mk.mk.right
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x : α
i : Fin n
hx : (x, i) ∈ graph f
j : Fin n
hy : (x, j) ∈ graph f
h✝ : i ≤ j
⊢ graph.proj { val := (x, i), property := hx } ≤ graph.proj { val := (x, j), property := hy }
simp [graph.proj]