-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem eq_sort_iff :
    σ = sort f ↔ Monotone (f ∘ σ) ∧ ∀ i j, i < j → f (σ i) = f (σ j) → σ i < σ j

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f)) ↔
    Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j

Tactic:
refine ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => ?_⟩, fun h i j hij => ?_⟩

Result:
case refine_1
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.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
⊢ (Equiv.trans σ (graphEquiv₁ f)) i < (Equiv.trans σ (graphEquiv₁ f)) j

Proof state:
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

Tactic:
rw [eq_sort_iff']

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f)) ↔
    Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j

Proof state:
case refine_1
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
i j : Fin n
hij : i < j
hfij : f (σ i) = f (σ j)
⊢ σ i < σ j

Tactic:
exact ((Prod.Lex.toLex_lt_toLex.1 <| h hij).resolve_left hfij.not_lt).2

Result:
no goals

Proof state:
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).1 < (f (σ j), σ j).1 ∨ (f (σ i), σ i).1 = (f (σ j), σ j).1 ∧ (f (σ i), σ i).2 < (f (σ j), σ j).2

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).1 < (f (σ j), σ j).1 ∨ (f (σ i), σ i).1 = (f (σ j), σ j).1 ∧ (f (σ i), σ i).2 < (f (σ j), σ j).2

Tactic:
exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl]

Result:
no goals

Proof state:
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
⊢ (Equiv.trans σ (graphEquiv₁ f)) i < (Equiv.trans σ (graphEquiv₁ f)) j

Tactic:
obtain he | hl := (h.1 hij.le).eq_or_lt <;> apply Prod.Lex.toLex_lt_toLex.2

Result:
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).1 < (f (σ j), σ j).1 ∨ (f (σ i), σ i).1 = (f (σ j), σ j).1 ∧ (f (σ i), σ i).2 < (f (σ j), σ j).2

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).1 < (f (σ j), σ j).1 ∨ (f (σ i), σ i).1 = (f (σ j), σ j).1 ∧ (f (σ i), σ i).2 < (f (σ j), σ j).2