awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
hy : x = y.succ
neg :
  ∀ (h' : i.castSucc < y.succ) (hy : x = y.succ),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove y.succ)) :
        Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))

Tactic:
rw [hy] at h' ⊢
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
neg :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove y.succ)) :
      Fin (Δ'.len + 1))

Tactic:
rw [Fin.predAbove_of_castSucc_lt i y.succ h', Fin.pred_succ]

Premises used: Fin.succ, Fin.predAbove_of_castSucc_lt, Fin.pred_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
pos :
  ∀ (h'' : y = i),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
        Fin (Δ'.len + 1))
neg :
  ∀ (h'' : ¬y = i),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
        Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))

Tactic:
by_cases h'' : y = i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
pos :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))

Tactic:
rw [h'']
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))

Tactic:
hi.symm.trans ?_

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
pos :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))

Tactic:
refine hi.symm.trans ?_

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
pos : i.castSucc = (Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i
⊢ Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i) :
      Fin (Δ'.len + 1))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
pos : i.castSucc = i.succ.succAbove i
⊢ i.castSucc = (Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i

Tactic:
dsimp [δ]

Premises used: SimplexCategory.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
pos : i.castSucc < i.succ
⊢ i.castSucc = i.succ.succAbove i

Tactic:
rw [Fin.succAbove_of_castSucc_lt i.succ]

Premises used: Fin.succ, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc < i.succ

Tactic:
Fin.castSucc_lt_succ

Premises used: Fin.castSucc_lt_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc < i.succ

Tactic:
exact Fin.castSucc_lt_succ

Premises used: Fin.castSucc_lt_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
neg :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (i.succ.succAbove y) : Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) y) :
      Fin (Δ'.len + 1))

Tactic:
dsimp [δ]

Premises used: SimplexCategory.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
neg : i.succ ≤ y.castSucc
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y.succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (i.succ.succAbove y) : Fin (Δ'.len + 1))

Tactic:
rw [Fin.succAbove_of_le_castSucc i.succ _]

Premises used: Fin.succAbove_of_le_castSucc, Fin.succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
neg : ∀ (h' : (↑i : ℕ) ≤ (↑y : ℕ)) (h'' : ¬(↑y : ℕ) = (↑i : ℕ)), (↑i : ℕ) + 1 ≤ (↑y : ℕ)
⊢ i.succ ≤ y.castSucc

Tactic:
simp only [Fin.lt_def, Fin.le_iff_val_le_val, Fin.val_succ, Fin.val_castSucc,
        Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢

Premises used: Fin.ext_iff, Fin.val_succ, Fin.lt_def, Nat.lt_succ_iff, Fin.val_castSucc, Fin.le_iff_val_le_val
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h'_1 : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
hy : x = y.succ
h' : (↑i : ℕ) ≤ (↑y : ℕ)
h'' : ¬(↑y : ℕ) = (↑i : ℕ)
⊢ (↑i : ℕ) + 1 ≤ (↑y : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1

Tactic:
simp only [Function.Injective, exists_prop, not_forall] at hθ

Premises used: exists_prop, Function.Injective, Classical.not_forall
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
rcases :
  ∀ (x y : Fin (n + 1 + 1))
    (h₁ :
      Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)))
    (h₂ : ¬x = y),
    ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
      Eq (α := Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
        x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
pos :
  ∀ (h : x < y),
    ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
      Eq (α := Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
        x < y
neg :
  ∀ (h : ¬x < y),
    ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
      Eq (α := Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
        x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
by_cases h : x < y
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
h : x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
⟨x, y, ⟨h₁, h⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
h : x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
exact ⟨x, y, ⟨h₁, h⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
⟨y, x, ⟨h₁.symm, ?_⟩⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
h : ¬x < y
neg : y < x
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (n + 1 + 1)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : ¬x = y
h : ¬x < y
⊢ y < x

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
⊢ ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y

Tactic:
have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y := by
    rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
    by_cases h : x < y
    · exact ⟨x, y, ⟨h₁, h⟩⟩
    · refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
      lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
hθ₂ :
  ∃ (x : Fin (n + 2)) (y : Fin (n + 2)),
    Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)) ∧
      x < y
rcases :
  ∀ (x y : Fin (n + 2))
    (h₁ :
      Eq (α := Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1)))
    (h₂ : x < y), ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'
⊢ ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'

Tactic:
rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
h : ∃ (θ' : ⦋n⦌ ⟶ Δ'), θ = σ (x.castPred ⋯) ≫ θ'
⊢ ∃ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'

Tactic:
use x.castPred ((Fin.le_last _).trans_lt' h₂).ne

Premises used: Fin.castPred, LE.le.trans_lt', LT.lt.ne, Fin.le_last
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ∃ (x : Fin (n + 1 + 1)) (x_1 : Fin (n + 1 + 1)),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
        ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x_1 : Fin (Δ'.len + 1)) ∧
      ¬x = x_1
x y : Fin (n + 2)
h₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
h₂ : x < y
h :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
⊢ ∃ (θ' : ⦋n⦌ ⟶ Δ'), θ = σ (x.castPred ⋯) ≫ θ'

Tactic:
apply eq_σ_comp_of_not_injective'

Premises used: SimplexCategory.eq_σ_comp_of_not_injective'