awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (fun (p : ↥(graph f)) ↦ (↑p : Lex (α × Fin n)).2)
      ((fun (i : Fin n) ↦ (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (f i, i) ⋯ : ↥(graph f))) i) =
    i

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
x_1 : ↥(graph f)
x : α
i : Fin n
h : (x, i) ∈ graph f
⊢ (fun (i : Fin n) ↦ (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (f i, i) ⋯ : ↥(graph f)))
      ((fun (p : ↥(graph f)) ↦ (↑p : Lex (α × Fin n)).2)
        (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (x, i) h)) =
    Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (x, i) h

Tactic:
simpa [graph, eq_comm, eqComm] using h

Premises used: Tuple.graph, eq_comm, eqComm
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Function.comp (β := ↥(graph f)) graph.proj (⇑(graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) = f

Tactic:
rfl

Premises used: Tuple.graph.proj, rfl
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ (graph f).card = n

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
i : Fin n
⊢ Eq (α := ↥(graph f)) ((graphEquiv₂ f : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((graphEquiv₁ f : (a : Fin n) → ↥(graph f)) ((sort f : (a : Fin n) → Fin n) i : Fin n) : ↥(graph f))

Tactic:
((graphEquiv₁ f).apply_symm_apply _).symm

Premises used: Equiv.apply_symm_apply, Tuple.graphEquiv₁, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Eq (α := Fin n → α)
    (Function.comp (β := ↥(graph f)) graph.proj
      (Function.comp (β := ↥(graph f))
        (Function.comp (β := Fin n) (⇑(graphEquiv₁ f) : (a : Fin n) → ↥(graph f))
          (⇑(Equiv.symm (graphEquiv₁ f)) : (a : ↥(graph f)) → Fin n))
        (⇑(RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(graph f)) ↦ x1 ≤ x2)
              (graphEquiv₂ f)) :
          (a : Fin n) → ↥(graph f))))
    (Function.comp (β := ↥(graph f)) graph.proj (⇑(graphEquiv₂ f) : (a : Fin n) → ↥(graph f)))

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
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 (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (x, i) hx) ≤
    graph.proj (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (y, j) hy)

Tactic:
le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
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 (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (x, i) hx) ≤
    graph.proj (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (y, j) hy)

Tactic:
exact le_of_lt ‹_›

Premises used: le_of_lt
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
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 (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (x, i) hx) ≤
    graph.proj (Subtype.mk (p := fun (x : Lex (α × Fin n)) ↦ x ∈ graph f) (x, j) hy)

Tactic:
simp [graph.proj]

Premises used: Tuple.graph.proj
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
rw :
  Monotone (α := Fin n) (β := α)
    (Function.comp (β := ↥(graph f)) graph.proj (⇑(graphEquiv₂ f) : (a : Fin n) → ↥(graph f)))
⊢ Monotone (α := Fin n) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
rw [self_comp_sort]

Premises used: Tuple.self_comp_sort
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Monotone (α := Fin n) (β := α)
    (Function.comp (β := ↥(graph f)) graph.proj (⇑(graphEquiv₂ f) : (a : Fin n) → ↥(graph f)))

Tactic:
(monotone_proj f).comp (graphEquiv₂ f).monotone

Premises used: OrderIso.monotone, Tuple.monotone_proj, Monotone.comp, Tuple.graphEquiv₂
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Monotone (α := Fin n) (β := α)
    (Function.comp (β := ↥(graph f)) graph.proj (⇑(graphEquiv₂ f) : (a : Fin n) → ↥(graph f)))

Tactic:
exact (monotone_proj f).comp (graphEquiv₂ f).monotone

Premises used: OrderIso.monotone, Tuple.monotone_proj, Monotone.comp, Tuple.graphEquiv₂
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
j : Fin n
f : Fin n → α
inst : Preorder α
a : α
inst_1 : DecidableLE α
h_sorted : Monotone f
⊢ ∀ (i j : Fin n), j ≤ i → (fun (x : Fin n) ↦ f x ≤ a) i → (fun (x : Fin n) ↦ f x ≤ a) j

Tactic:
grind [Monotone]

Premises used: Monotone
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
j : Fin n
f : Fin n → α
inst : Preorder α
a : α
inst_1 : DecidableLE α
h_sorted : Antitone f
⊢ ∀ (i j : Fin n), j ≤ i → (fun (x : Fin n) ↦ a ≤ f x) i → (fun (x : Fin n) ↦ a ≤ f x) j

Tactic:
grind [Antitone]

Premises used: Antitone
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
j : Fin n
f : Fin n → α
inst : Preorder α
a : α
inst_1 : DecidableLT α
h_sorted : Monotone f
⊢ ∀ (i j : Fin n), j ≤ i → (fun (x : Fin n) ↦ f x < a) i → (fun (x : Fin n) ↦ f x < a) j

Tactic:
grind [Monotone]

Premises used: Monotone
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
j : Fin n
f : Fin n → α
inst : Preorder α
a : α
inst_1 : DecidableLT α
h_sorted : Antitone f
⊢ ∀ (i j : Fin n), j ≤ i → (fun (x : Fin n) ↦ a < f x) i → (fun (x : Fin n) ↦ a < f x) j

Tactic:
grind [Antitone]

Premises used: Antitone
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : PartialOrder α
f : Fin n → α
σ τ : Equiv.Perm (Fin n)
hfσ : Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n))
hfτ : Monotone (α := Fin n) (f ∘ (⇑τ : (a : Fin n) → Fin n))
⊢ Eq (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑τ : (a : Fin n) → Fin n))

Tactic:
ofFn_injective <|
    ((σ.ofFn_comp_perm f).trans (τ.ofFn_comp_perm f).symm).eq_of_pairwise'
      hfσ.sortedLE_ofFn.pairwise hfτ.sortedLE_ofFn.pairwise

Premises used: Equiv.Perm.ofFn_comp_perm, List.SortedLE.pairwise, Monotone.sortedLE_ofFn, List.Perm.eq_of_pairwise', List.ofFn_injective, List.Perm.trans, List.Perm.symm
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : PartialOrder α
f : Fin n → α
σ τ : Equiv.Perm (Fin n)
hfσ : Antitone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n))
hfτ : Antitone (α := Fin n) (f ∘ (⇑τ : (a : Fin n) → Fin n))
⊢ Eq (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑τ : (a : Fin n) → Fin n))

Tactic:
ofFn_injective <|
    ((σ.ofFn_comp_perm f).trans (τ.ofFn_comp_perm f).symm).eq_of_pairwise'
      hfσ.sortedGE_ofFn.pairwise hfτ.sortedGE_ofFn.pairwise

Premises used: Equiv.Perm.ofFn_comp_perm, Antitone.sortedGE_ofFn, List.SortedGE.pairwise, List.Perm.eq_of_pairwise', List.ofFn_injective, List.Perm.trans, List.Perm.symm
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
mp :
  σ = sort f → StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
mpr :
  StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) → σ = sort f
⊢ σ = sort f ↔ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))

Tactic:
constructor
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
mp :
  StrictMono (α := Fin n) (β := ↥(graph f))
    (⇑(Equiv.trans
          (RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(graph f)) ↦ x1 ≤ x2)
            (graphEquiv₂ f))
          (Equiv.refl ↥(graph f))) :
      (a : Fin n) → ↥(graph f))
⊢ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))

Tactic:
rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]

Premises used: Equiv.trans_assoc, Tuple.sort, Equiv.symm_trans_self
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono (α := Fin n) (β := ↥(graph f))
    (⇑(Equiv.trans
          (RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(graph f)) ↦ x1 ≤ x2)
            (graphEquiv₂ f))
          (Equiv.refl ↥(graph f))) :
      (a : Fin n) → ↥(graph f))

Tactic:
(graphEquiv₂ f).strictMono

Premises used: OrderIso.strictMono, Tuple.graphEquiv₂
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono (α := Fin n) (β := ↥(graph f))
    (⇑(Equiv.trans
          (RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(graph f)) ↦ x1 ≤ x2)
            (graphEquiv₂ f))
          (Equiv.refl ↥(graph f))) :
      (a : Fin n) → ↥(graph f))

Tactic:
exact (graphEquiv₂ f).strictMono

Premises used: OrderIso.strictMono, Tuple.graphEquiv₂
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
⊢ graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) h ⋯

Tactic:
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) h ⋯
mpr : ∀ (x : Fin n), Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) x : Fin n) ((sort f : (a : Fin n) → Fin n) x : Fin n)
⊢ σ = sort f

Tactic:
ext1 x
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) h ⋯
x : Fin n
⊢ Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) x : Fin n) ((sort f : (a : Fin n) → Fin n) x : Fin n)

Tactic:
(graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (DFunLike.congr_fun this x).symm

Premises used: DFunLike.congr_fun, Tuple.graphEquiv₁, Iff.mp, Eq.symm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) h ⋯
x : Fin n
⊢ Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) x : Fin n) ((sort f : (a : Fin n) → Fin n) x : Fin n)

Tactic:
exact (graphEquiv₁ f).apply_eq_iff_eq_symm_apply.1 (DFunLike.congr_fun this x).symm

Premises used: DFunLike.congr_fun, Tuple.graphEquiv₁, Iff.mp, Eq.symm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
rw :
  StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
⊢ σ = sort f ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)

Tactic:
rw [eq_sort_iff']

Premises used: Tuple.eq_sort_iff'
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)

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

Premises used: StrictMono.monotone, Tuple.monotone_proj, Monotone.comp, And.intro, Iff.intro
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
refine_1 :
  ∀ (h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)))
    (i j : Fin n) (hij : i < j) (hfij : f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j)),
    LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
refine_2 :
  ∀
    (h :
      Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
        ∀ (i j : Fin n),
          i < j →
            f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
              LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n))
    (i j : Fin n) (hij : i < j),
    LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
      ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
⊢ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)

Tactic:
refine ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => ?_⟩, fun h i j hij => ?_⟩
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
i j : Fin n
hij : i < j
hfij : f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j)
⊢ LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)

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

Premises used: Or.resolve_left, Prod.Lex.toLex_lt_toLex, And.right, Iff.mp, Eq.not_lt
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
i j : Fin n
hij : i < j
hfij : f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j)
⊢ LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)

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

Premises used: Or.resolve_left, Prod.Lex.toLex_lt_toLex, And.right, Iff.mp, Eq.not_lt
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
refine_2 :
  ∀ (he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j),
    LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
      ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
refine_2₁ :
  ∀ (hl : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i < (f ∘ (⇑σ : (a : Fin n) → Fin n)) j),
    LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
      ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))

Tactic:
obtain he | hl := (h.1 hij.le).eq_or_lt

Premises used: LE.le.eq_or_lt, LT.lt.le, And.left
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
refine_2 :
  ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
    ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
      LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))

Tactic:
apply Prod.Lex.toLex_lt_toLex.2

Premises used: Iff.mpr, Prod.Lex.toLex_lt_toLex
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
hl : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i < (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
refine_2 :
  ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
    ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
      LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))

Tactic:
apply Prod.Lex.toLex_lt_toLex.2

Premises used: Iff.mpr, Prod.Lex.toLex_lt_toLex
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
    ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
      LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)

Tactic:
Or.inr ⟨he, h.2 i j hij he⟩

Premises used: And.right, And.intro, Or.inr
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
hl : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i < (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
    ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
      LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)

Tactic:
Or.inl hl

Premises used: Or.inl
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
    ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
      LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
        ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)

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

Premises used: Or.inr
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
rw : (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f
⊢ sort f = Equiv.refl (Fin n) ↔ Monotone f

Tactic:
rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp_id]

Premises used: Function.comp_id, eq_comm, Tuple.eq_sort_iff, Equiv.coe_refl
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
simp : Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j
⊢ (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f

Tactic:
simp only [id, and_iff_left_iff_imp]

Premises used: id, and_iff_left_iff_imp
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j

Tactic:
fun _ _ _ hij _ => hij
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j

Tactic:
exact fun _ _ _ hij _ => hij