n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f)) ↔ Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
rw [eq_sort_iff']
case refine'_1
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
i j : Fin n
hij : i < j
hfij : f (↑σ i) = f (↑σ j)
⊢ ↑σ i < ↑σ j

case refine'_2
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f)) ↔ Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
refine' ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => _⟩, fun h i j hij => _⟩
no goals
case refine'_1
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
i j : Fin n
hij : i < j
hfij : f (↑σ i) = f (↑σ j)
⊢ ↑σ i < ↑σ j
exact (((Prod.Lex.lt_iff _ _).1 <| h hij).resolve_left hfij.not_lt).2
case refine'_2.inl
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
he : (f ∘ ↑σ) i = (f ∘ ↑σ) j
⊢ (f (↑σ i), ↑σ i).fst < (f (↑σ j), ↑σ j).fst ∨
    (f (↑σ i), ↑σ i).fst = (f (↑σ j), ↑σ j).fst ∧ (f (↑σ i), ↑σ i).snd < (f (↑σ j), ↑σ j).snd

case refine'_2.inr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
hl : (f ∘ ↑σ) i < (f ∘ ↑σ) j
⊢ (f (↑σ i), ↑σ i).fst < (f (↑σ j), ↑σ j).fst ∨
    (f (↑σ i), ↑σ i).fst = (f (↑σ j), ↑σ j).fst ∧ (f (↑σ i), ↑σ i).snd < (f (↑σ j), ↑σ j).snd
case refine'_2
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
obtain he | hl := (h.1 hij.le).eq_or_lt <;> apply (Prod.Lex.lt_iff _ _).2
no goals
case refine'_2.inl
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
he : (f ∘ ↑σ) i = (f ∘ ↑σ) j
⊢ (f (↑σ i), ↑σ i).fst < (f (↑σ j), ↑σ j).fst ∨
    (f (↑σ i), ↑σ i).fst = (f (↑σ j), ↑σ j).fst ∧ (f (↑σ i), ↑σ i).snd < (f (↑σ j), ↑σ j).snd

case refine'_2.inr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Monotone (f ∘ ↑σ) ∧ ∀ (i j : Fin n), i < j → f (↑σ i) = f (↑σ j) → ↑σ i < ↑σ j
i j : Fin n
hij : i < j
hl : (f ∘ ↑σ) i < (f ∘ ↑σ) j
⊢ (f (↑σ i), ↑σ i).fst < (f (↑σ j), ↑σ j).fst ∨
    (f (↑σ i), ↑σ i).fst = (f (↑σ j), ↑σ j).fst ∧ (f (↑σ i), ↑σ i).snd < (f (↑σ j), ↑σ j).snd
exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl]