[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card (graph f) = n
[PROOFSTEP]
rw [graph, Finset.card_image_of_injective]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card Finset.univ = n
[PROOFSTEP]
exact Finset.card_fin _
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Function.Injective fun i => (f i, i)
[PROOFSTEP]
intro _
  _
    -- Porting note: was `simp`
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (fun i => (f i, i)) a₁✝ = (fun i => (f i, i)) a₂✝ → a₁✝ = a₂✝
[PROOFSTEP]
dsimp only
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝) = (f a₂✝, a₂✝) → a₁✝ = a₂✝
[PROOFSTEP]
rw [Prod.ext_iff]
[GOAL]
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝).fst = (f a₂✝, a₂✝).fst ∧ (f a₁✝, a₁✝).snd = (f a₂✝, a₂✝).snd → a₁✝ = a₂✝
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (f i, i) ∈ graph f
[PROOFSTEP]
simp [graph]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (fun p => (↑p).snd)
      ((fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) }) i) =
    i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i : Fin n
h : (x, i) ∈ graph f
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i), property := h }) =
    { val := (x, i), property := h }
[PROOFSTEP]
simp only [graph, Finset.mem_image, Finset.mem_univ, true_and] at h 
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i : Fin n
h✝ : (x, i) ∈ graph f
h : ∃ a, (f a, a) = (x, i)
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i), property := h✝ }) =
    { val := (x, i), property := h✝ }
[PROOFSTEP]
obtain ⟨i', hi'⟩ := h
[GOAL]
case intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i : Fin n
h : (x, i) ∈ graph f
i' : Fin n
hi' : (f i', i') = (x, i)
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i), property := h }) =
    { val := (x, i), property := h }
[PROOFSTEP]
obtain ⟨-, rfl⟩ := Prod.mk.inj_iff.mp hi'
[GOAL]
case intro.intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
x✝ : { x // x ∈ graph f }
x : α
i' : Fin n
h : (x, i') ∈ graph f
hi' : (f i', i') = (x, i')
⊢ (fun i => { val := (f i, i), property := (_ : (f i, i) ∈ Finset.image (fun i => (f i, i)) Finset.univ) })
      ((fun p => (↑p).snd) { val := (x, i'), property := h }) =
    { val := (x, i'), property := h }
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card (graph f) = n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ graph.proj ∘ (↑(graphEquiv₁ f) ∘ ↑(graphEquiv₁ f).symm) ∘ ↑(graphEquiv₂ f).toEquiv = graph.proj ∘ ↑(graphEquiv₂ f)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone graph.proj
[PROOFSTEP]
rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (_ | h)
[GOAL]
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 }
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
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 }
[PROOFSTEP]
simp [graph.proj]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (f ∘ ↑(sort f))
[PROOFSTEP]
rw [self_comp_sort]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (graph.proj ∘ ↑(graphEquiv₂ f))
[PROOFSTEP]
exact (monotone_proj f).comp (graphEquiv₂ f).monotone
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ StrictMono ↑(σ.trans (graphEquiv₁ f))
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f → StrictMono ↑(σ.trans (graphEquiv₁ f))
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f)) → σ = sort f
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ↑(σ.trans (graphEquiv₁ f))
[PROOFSTEP]
rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]
[GOAL]
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 }))
[PROOFSTEP]
exact (graphEquiv₂ f).strictMono
[GOAL]
case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ↑(σ.trans (graphEquiv₁ f))
⊢ σ = sort f
[PROOFSTEP]
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
[GOAL]
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
[PROOFSTEP]
ext1 x
[GOAL]
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
[PROOFSTEP]
exact (graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (FunLike.congr_fun this x).symm
[GOAL]
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
[PROOFSTEP]
rw [eq_sort_iff']
[GOAL]
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
[PROOFSTEP]
refine' ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => _⟩, fun h i j hij => _⟩
[GOAL]
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
[PROOFSTEP]
exact (((Prod.Lex.lt_iff _ _).1 <| h hij).resolve_left hfij.not_lt).2
[GOAL]
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
[PROOFSTEP]
obtain he | hl := (h.1 hij.le).eq_or_lt
[GOAL]
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
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
[PROOFSTEP]
apply (Prod.Lex.lt_iff _ _).2
[GOAL]
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
⊢ ↑(σ.trans (graphEquiv₁ f)) i < ↑(σ.trans (graphEquiv₁ f)) j
[PROOFSTEP]
apply (Prod.Lex.lt_iff _ _).2
[GOAL]
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
[PROOFSTEP]
exacts [Or.inr ⟨he, h.2 i j hij he⟩, Or.inl hl]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ sort f = Equiv.refl (Fin n) ↔ Monotone f
[PROOFSTEP]
rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp.right_id]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f
[PROOFSTEP]
simp only [id.def, and_iff_left_iff_imp]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j
[PROOFSTEP]
exact fun _ _ _ hij _ => hij
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ (f ∘ ↑σ) ∘ ↑(sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
[PROOFSTEP]
rw [Function.comp.assoc, ← Equiv.Perm.coe_mul]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ f ∘ ↑(σ * sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
[PROOFSTEP]
exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : f ∘ ↑σ ≠ f ∘ ↑(sort f)
⊢ ∃ i j, i < j ∧ (f ∘ ↑σ) j < (f ∘ ↑σ) i
[PROOFSTEP]
contrapose! h
[GOAL]
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ↑σ) i ≤ (f ∘ ↑σ) j
⊢ f ∘ ↑σ = f ∘ ↑(sort f)
[PROOFSTEP]
exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)
