case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f))

case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
⊢ σ = sort f
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ StrictMono ↑(σ.trans (graphEquiv₁ f))
constructor <;> intro h
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑((graphEquiv₂ f).trans (Equiv.refl { x // x ∈ graph f }))
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f))
rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]
no goals
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑((graphEquiv₂ f).trans (Equiv.refl { x // x ∈ graph f }))
exact (graphEquiv₂ f).strictMono
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
this :
  graphEquiv₂ f =
    StrictMono.orderIsoOfSurjective (↑(σ.trans (graphEquiv₁ f))) h (_ : Function.Surjective ↑(σ.trans (graphEquiv₁ f)))
⊢ σ = sort f
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
⊢ σ = sort f
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
case mpr.H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
this :
  graphEquiv₂ f =
    StrictMono.orderIsoOfSurjective (↑(σ.trans (graphEquiv₁ f))) h (_ : Function.Surjective ↑(σ.trans (graphEquiv₁ f)))
x : Fin n
⊢ ↑σ x = ↑(sort f) x
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
this :
  graphEquiv₂ f =
    StrictMono.orderIsoOfSurjective (↑(σ.trans (graphEquiv₁ f))) h (_ : Function.Surjective ↑(σ.trans (graphEquiv₁ f)))
⊢ σ = sort f
ext1 x
no goals
case mpr.H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
this :
  graphEquiv₂ f =
    StrictMono.orderIsoOfSurjective (↑(σ.trans (graphEquiv₁ f))) h (_ : Function.Surjective ↑(σ.trans (graphEquiv₁ f)))
x : Fin n
⊢ ↑σ x = ↑(sort f) x
exact (graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (FunLike.congr_fun this x).symm