awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  LE.le (α := 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))
h₃ :
  LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
⊢ 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))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
⊢ LE.le (α := 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))

Tactic:
θ.toOrderHom.monotone (le_of_lt Fin.castSucc_lt_succ)

Premises used: OrderHom.monotone, le_of_lt, Fin.castSucc_lt_succ, SimplexCategory.Hom.toOrderHom
-- 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
⊢ LE.le (α := 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))

Tactic:
exact θ.toOrderHom.monotone (le_of_lt Fin.castSucc_lt_succ)

Premises used: OrderHom.monotone, le_of_lt, Fin.castSucc_lt_succ, SimplexCategory.Hom.toOrderHom
-- 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 :
  LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
⊢ LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))

Tactic:
rw [Fin.castSucc_castPred, h₁]

Premises used: Fin.castSucc_castPred
-- 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
⊢ LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))

Tactic:
θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

Premises used: Iff.mpr, OrderHom.monotone, Fin.succ_castPred_le_iff, SimplexCategory.Hom.toOrderHom
-- 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
⊢ LE.le (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).succ : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))

Tactic:
exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

Premises used: Iff.mpr, OrderHom.monotone, Fin.succ_castPred_le_iff, SimplexCategory.Hom.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
h : θ = (θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i
⊢ ∃ (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i

Tactic:
use θ ≫ σ (.predAbove (.last n) i)

Premises used: SimplexCategory.σ, Fin.predAbove, Fin.last
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
h :
  ∀ (x : Fin (Δ.len + 1)),
    Eq (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x :
        Fin (⦋n + 1⦌.len + 1))
⊢ θ = (θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
dsimp :
  (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x =
    i.succAbove (((Fin.last n).predAbove i).predAbove ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x))
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x :
      Fin (⦋n + 1⦌.len + 1))

Tactic:
dsimp [δ, σ]

Premises used: SimplexCategory.δ, SimplexCategory.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x =
    i.succAbove (((Fin.last n).predAbove i).predAbove ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x))

Tactic:
.symm <| this _ (hi _)

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x =
    i.succAbove (((Fin.last n).predAbove i).predAbove ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (n + 1 + 1)) x))

Tactic:
exact .symm <| this _ (hi _)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
h : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x :
      Fin (⦋n + 1⦌.len + 1))

Tactic:
suffices ∀ j ≠ i, i.succAbove (((Fin.last n).predAbove i).predAbove j) = j by
    dsimp [δ, σ]
    exact .symm <| this _ (hi _)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hj : j ≠ i
h :
  ∀
    (hi :
      ∀ (x : Fin (Δ.len + 1)),
        Ne (α := Fin (⦋n + 1⦌.len + 1))
          ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
          (Fin.last (n + 1) : Fin (n + 1 + 1)))
    (hj : j ≠ Fin.last (n + 1)),
    Fin.succAbove (Fin.last (n + 1)) (((Fin.last n).predAbove (Fin.last (n + 1))).predAbove j) = j
h₁ :
  ∀ (i : Fin (n + 1))
    (hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i.castSucc)
    (hj : j ≠ i.castSucc), i.castSucc.succAbove (((Fin.last n).predAbove i.castSucc).predAbove j) = j
⊢ i.succAbove (((Fin.last n).predAbove i).predAbove j) = j

Tactic:
cases i using Fin.lastCases
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
hi :
  ∀ (x : Fin (Δ.len + 1)),
    Ne (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x : Fin (⦋n + 1⦌.len + 1))
      (Fin.last (n + 1) : Fin (n + 1 + 1))
hj : j ≠ Fin.last (n + 1)
⊢ Fin.succAbove (Fin.last (n + 1)) (((Fin.last n).predAbove (Fin.last (n + 1))).predAbove j) = j

Tactic:
simp [hj]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
i : Fin (n + 1)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x ≠ i.castSucc
hj : j ≠ i.castSucc
⊢ i.castSucc.succAbove (((Fin.last n).predAbove i.castSucc).predAbove j) = j

Tactic:
simp [hj]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ :
  ¬Function.Surjective (α := Fin (Δ.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1))
obtain :
  ∀ (i : Fin (⦋n + 1⦌.len + 1))
    (hi : ¬∃ (a : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) a = i),
    ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
⊢ ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp hθ

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ :
  ¬Function.Surjective (α := Fin (Δ.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1))
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ (a : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) a = i
h : ∃ (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i
⊢ ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i

Tactic:
use i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ :
  ¬Function.Surjective (α := Fin (Δ.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1))
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ (a : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) a = i
⊢ ∃ (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i

Tactic:
eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)

Premises used: not_exists, SimplexCategory.eq_comp_δ_of_not_surjective', Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ :
  ¬Function.Surjective (α := Fin (Δ.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1))
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ (a : Fin (Δ.len + 1)), (Hom.toOrderHom θ : (a : Fin (Δ.len + 1)) → Fin (⦋n + 1⦌.len + 1)) a = i
⊢ ∃ (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i

Tactic:
exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)

Premises used: not_exists, SimplexCategory.eq_comp_δ_of_not_surjective', Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
i : x ⟶ x
inst : Mono i
⊢ i = 𝟙 x

Tactic:
have := (isIso_iff_of_mono i).mpr rfl
  eq_id_of_isIso _

Premises used: Iff.mpr, SimplexCategory.eq_id_of_isIso, SimplexCategory.isIso_iff_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
i : x ⟶ x
inst : Epi i
⊢ i = 𝟙 x

Tactic:
have := (isIso_iff_of_epi i).mpr rfl
  eq_id_of_isIso _

Premises used: Iff.mpr, SimplexCategory.eq_id_of_isIso, SimplexCategory.isIso_iff_of_epi, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
rw : ¬Mono θ
⊢ ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (⦋n⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))

Tactic:
rw [← mono_iff_injective]

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
⊢ ¬Mono θ

Tactic:
grind [→ le_of_mono]

Premises used: SimplexCategory.le_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
obtain : ∀ (i : Fin (n + 1)) (θ' : ⦋n⦌ ⟶ ⦋n⦌) (h : θ = σ i ≫ θ'), ∃ (i : Fin (n + 1)), θ = σ i
⊢ ∃ (i : Fin (n + 1)), θ = σ i

Tactic:
obtain ⟨i, θ', h⟩ := eq_σ_comp_of_not_injective θ (by
    rw [← mono_iff_injective]
    grind [→ le_of_mono])

Premises used: SimplexCategory.eq_σ_comp_of_not_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
h₁ : θ = σ i
⊢ ∃ (i : Fin (n + 1)), θ = σ i

Tactic:
use i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
rw : Epi θ
⊢ Epi (σ i ≫ θ')

Tactic:
rw [← h]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi θ

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi (σ i ≫ θ')

Tactic:
haveI : Epi (σ i ≫ θ') := by
    rw [← h]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ Epi θ'

Tactic:
haveI := CategoryTheory.epi_of_epi (σ i) θ'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
this_1 : Epi (σ i ≫ θ')
this : Epi θ'
h₁ : σ i ≫ θ' = σ i
h₂ : σ i ≫ 𝟙 ⦋n⦌ = σ i
h₃ h₄ : σ i = σ i
⊢ θ = σ i

Tactic:
rw [h, eq_id_of_epi θ', Category.comp_id]

Premises used: SimplexCategory.eq_id_of_epi, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
rw : ¬Epi θ
⊢ ¬Function.Surjective (α := Fin (⦋n⦌.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
      (⇑(Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))

Tactic:
rw [← epi_iff_surjective]

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
⊢ ¬Epi θ

Tactic:
grind [→ le_of_epi]

Premises used: SimplexCategory.le_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
obtain : ∀ (i : Fin (n + 2)) (θ' : ⦋n⦌ ⟶ ⦋n⦌) (h : θ = θ' ≫ δ i), ∃ (i : Fin (n + 2)), θ = δ i
⊢ ∃ (i : Fin (n + 2)), θ = δ i

Tactic:
obtain ⟨i, θ', h⟩ := eq_comp_δ_of_not_surjective θ (by
    rw [← epi_iff_surjective]
    grind [→ le_of_epi])

Premises used: SimplexCategory.eq_comp_δ_of_not_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
h₁ : θ = δ i
⊢ ∃ (i : Fin (n + 2)), θ = δ i

Tactic:
use i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
rw : Mono θ
⊢ Mono (θ' ≫ δ i)

Tactic:
rw [← h]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono θ

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono (θ' ≫ δ i)

Tactic:
haveI : Mono (θ' ≫ δ i) := by
    rw [← h]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ Mono θ'

Tactic:
haveI := CategoryTheory.mono_of_mono θ' (δ i)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this_1 : Mono (θ' ≫ δ i)
this : Mono θ'
h₁ : θ' ≫ δ i = δ i
h₂ : 𝟙 ⦋n⦌ ≫ δ i = δ i
h₃ h₄ : δ i = δ i
⊢ θ = δ i

Tactic:
rw [h, eq_id_of_mono θ', Category.id_comp]

Premises used: SimplexCategory.eq_id_of_mono, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst : Mono i
hi' : Δ ≠ Δ'
⊢ Δ'.len < Δ.len

Tactic:
grind [→ len_le_of_mono, SimplexCategory.ext]

Premises used: SimplexCategory.len_le_of_mono, SimplexCategory.ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ SplitEpiCategory SimplexCategory

Tactic:
skeletalEquivalence.inverse.splitEpiCategoryImpOfIsEquivalence

Premises used: SimplexCategory.skeletalEquivalence, CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ HasStrongEpiMonoFactorisations SimplexCategory

Tactic:
Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence
    SimplexCategory.skeletalEquivalence.inverse

Premises used: SimplexCategory.skeletalEquivalence, CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ HasStrongEpiImages SimplexCategory

Tactic:
Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations

Premises used: CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ' : SimplexCategory
θ : Δ ⟶ Δ'
⊢ Epi (Y := image θ) (factorThruImage θ)

Tactic:
StrongEpi.epi

Premises used: CategoryTheory.StrongEpi.epi
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst : Epi e
i : Δ' ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
⊢ StrongEpi e

Tactic:
haveI := strongEpi_of_epi e
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e_1 : Δ ⟶ Δ'
inst : Epi e_1
i : Δ' ⟶ Δ''
inst_1 : Mono i
fac : e_1 ≫ i = φ
this : StrongEpi e_1
e : Δ' ≅ image φ := image.isoStrongEpiMono e_1 i fac
len : (image φ).len = Δ'.len
⊢ image φ = Δ'

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e_1 : Δ ⟶ Δ'
inst : Epi e_1
i : Δ' ⟶ Δ''
inst_1 : Mono i
fac : e_1 ≫ i = φ
this : StrongEpi e_1
e : Δ' ≅ image φ := image.isoStrongEpiMono e_1 i fac
⊢ (image φ).len = Δ'.len

Tactic:
le_antisymm (len_le_of_epi e.hom) (len_le_of_mono e.hom)

Premises used: SimplexCategory.len_le_of_mono, SimplexCategory.len_le_of_epi, le_antisymm, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e_1 : Δ ⟶ Δ'
inst : Epi e_1
i : Δ' ⟶ Δ''
inst_1 : Mono i
fac : e_1 ≫ i = φ
this : StrongEpi e_1
e : Δ' ≅ image φ := image.isoStrongEpiMono e_1 i fac
⊢ (image φ).len = Δ'.len

Tactic:
exact le_antisymm (len_le_of_epi e.hom) (len_le_of_mono e.hom)

Premises used: SimplexCategory.len_le_of_mono, SimplexCategory.len_le_of_epi, le_antisymm, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
⊢ StrongEpi e

Tactic:
haveI := strongEpi_of_epi e
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst : Epi e
i : image φ ⟶ Δ''
inst_1 : Mono i
fac : e ≫ i = φ
this : StrongEpi e
rw :
  image.ι φ =
    CategoryStruct.comp (Y := image φ) (Iso.hom (image.isoStrongEpiMono e i fac) : image φ ⟶ image φ)
      (image.ι φ : image φ ⟶ Δ'')
rw₁ : image.ι φ = 𝟙 (image φ) ≫ image.ι φ
rw₂ rw₃ : Eq (α := image φ ⟶ Δ'') (image.ι φ) (image.ι φ)
⊢ image.ι φ = i

Tactic:
rw [← image.isoStrongEpiMono_hom_comp_ι e i fac,
    SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom, Category.id_comp]

Premises used: SimplexCategory.eq_id_of_isIso, CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι, CategoryTheory.Limits.image.isoStrongEpiMono, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp