awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
succ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋m + 1 + 1⦌) → X _⦋1⦌) x =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i).op) : (a : X _⦋m + 1⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋m + 1 + 1⦌) → X _⦋m + 1⦌) x :
        X _⦋m + 1⦌) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
rw [SimplicialObject.δ_def, ← Functor.map_comp_apply, ← op_comp,
      SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)]

Premises used: CategoryTheory.op_comp, CategoryTheory.SimplicialObject.δ_def, CategoryTheory.Functor.map_comp_apply, SimplexCategory.mkOfSucc_δ_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
succ :
  ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋m + 1 + 1⦌) → X _⦋1⦌) x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋m + 1 + 1⦌) → X _⦋1⦌) x =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
rw : 1 + (↑i : ℕ) = (↑i : ℕ) + 1
rw₁ rw₂ : (↑i : ℕ) + 1 = (↑i : ℕ) + 1
⊢ 1 + (↑i : ℕ) = (↑i.succ : ℕ)

Tactic:
rw [Fin.val_succ, add_comm]

Premises used: Fin.val_succ, add_comm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋m + 1 + 1⦌) → X _⦋1⦌) x

Tactic:
exact Path.arrow_interval _ _ _ _ _ _ (by rw [Fin.val_succ, add_comm])

Premises used: SSet.Path.arrow_interval
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n m : ℕ
h : m ≤ n + 1
⊢ Truncated.spine (Functor.obj (truncation (n + 1)) X) m h = X.spine m

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, SSet.Truncated.spine, CategoryTheory.ObjectProperty.ι, Quiver.Hom.op, CategoryTheory.ObjectProperty.ιOfLE, CategoryTheory.Functor.comp, CategoryTheory.inducedFunctor, CategoryTheory.ObjectProperty.homMk, SSet.spine, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
Δ : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ n ≤ max m n + 1

Tactic:
omega
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n : ℕ
Δ : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ m ≤ max m n + 1

Tactic:
omega
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
n j l : ℕ
h : j + l ≤ n
Δ : X _⦋n⦌
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (spineId n).vertex i = (Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i

Tactic:
rfl

Premises used: SSet.stdSimplex.const, OrderHom.comp, SimplexCategory.Hom.comp, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin n
⊢ ((spineId n).arrow i : (a : Fin (1 + 1)) → Fin (n + 1)) 0 = i.castSucc

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin n
⊢ ((spineId n).arrow i : (a : Fin (1 + 1)) → Fin (n + 1)) 1 = i.succ

Tactic:
rfl

Premises used: Fin.succ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
p : X.Path n
hp₀ : ∀ (j : Fin (n + 1)), Membership.mem (γ := Set (X _⦋0⦌)) (A.obj (op ⦋0⦌)) (p.vertex j)
hp₁ : ∀ (j : Fin n), Membership.mem (γ := Set (X _⦋1⦌)) (A.obj (op ⦋1⦌)) (p.arrow j)
⊢ (A.liftPath p hp₀ hp₁).map A.ι = p

Tactic:
rfl

Premises used: SSet.Path.map, SSet.Truncated.Path, SSet.Truncated.Path.map, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∀ (j : Fin (n + 2 + 1)),
    Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌)) (Path.vertex (stdSimplex.spineId (n + 2)) j)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (op ⦋1⦌)) (↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌)

Tactic:
(horn.primitiveEdge.{u} h₀ hₙ j).2

Premises used: SSet.horn.primitiveEdge, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
h : Path.arrow (stdSimplex.spineId (n + 2)) j = (↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌)
⊢ Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (op ⦋1⦌)) (Path.arrow (stdSimplex.spineId (n + 2)) j)

Tactic:
convert! (horn.primitiveEdge.{u} h₀ hₙ j).2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
h :
  ∀ (a : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1)) a) : ℕ) =
      (↑(((↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌) : (a : Fin (1 + 1)) → Fin (n + 2 + 1)) a) : ℕ)
⊢ Path.arrow (stdSimplex.spineId (n + 2)) j = (↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌)

Tactic:
ext a
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
a : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑(((↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌) : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
h₁ :
  (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑(((↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌) : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
⊢ (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1)) a) : ℕ) =
    (↑(((↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌) : (a : Fin (1 + 1)) → Fin (n + 2 + 1)) a) : ℕ)

Tactic:
fin_cases a
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑(((↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌) : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑(((↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌) : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ (spineId i h₀ hₙ).map Λ[n + 2, i].ι = stdSimplex.spineId (n + 2)

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, SSet.Truncated.spine, Quiver.Hom.op, CategoryTheory.ObjectProperty.ιOfLE, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.homMk, SSet.spine, rfl, SSet.stdSimplex.spineId
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
⊢ Function.Surjective.{u + 1, u + 1} (α := X _⦋0⦌) mk

Tactic:
Quot.mk_surjective

Premises used: SSet.π₀, Quot.mk_surjective, SSet.π₀.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ mk x₀ = mk x₁

Tactic:
Quot.sound ⟨e⟩

Premises used: Quot.sound, SSet.π₀, Nonempty.intro, SSet.π₀.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
⊢ mk x₀ = mk x₁ ↔ Relation.EqvGen π₀Rel x₀ x₁

Tactic:
Quot.eq

Premises used: SSet.π₀, SSet.π₀.mk, Quot.eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X.π₀
obtain : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
⊢ motive x

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective

Premises used: SSet.π₀.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X _⦋0⦌
⊢ motive (π₀.mk x)

Tactic:
mk x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X _⦋0⦌
⊢ motive (π₀.mk x)

Tactic:
exact mk x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
x y : X _⦋0⦌
e : Edge x y
⊢ f x = f y

Tactic:
hf e
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
x y : X _⦋0⦌
e : Edge x y
⊢ f x = f y

Tactic:
exact hf e
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
x : X _⦋0⦌
⊢ lift f hf (mk x) = f x

Tactic:
rfl

Premises used: SSet.π₀.lift, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y : SSet
f : X ⟶ Y
x₀ : X _⦋0⦌
⊢ mapπ₀ f (π₀.mk x₀) =
    π₀.mk
      ((ConcreteCategory.hom (FC := Fun) (f.app (op ⦋0⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y _⦋0⦌))
        x₀)

Tactic:
rfl

Premises used: SSet.mapπ₀, SSet.π₀.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
x : X.π₀
mk : ∀ (x : X _⦋0⦌), mapπ₀ (𝟙 X) (π₀.mk x) = π₀.mk x
⊢ mapπ₀ (𝟙 X) x = x

Tactic:
induction x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
x : X _⦋0⦌
⊢ mapπ₀ (𝟙 X) (π₀.mk x) = π₀.mk x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
x : X.π₀
mk : ∀ (x : X _⦋0⦌), mapπ₀ (f ≫ g) (π₀.mk x) = mapπ₀ g (mapπ₀ f (π₀.mk x))
⊢ mapπ₀ (f ≫ g) x = mapπ₀ g (mapπ₀ f x)

Tactic:
induction x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
x : X _⦋0⦌
⊢ mapπ₀ (f ≫ g) (π₀.mk x) = mapπ₀ g (mapπ₀ f (π₀.mk x))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
h :
  ∀ (s : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌),
    (ConcreteCategory.hom (FC := Fun) (SimplicialObject.δ X 1 ≫ ↾π₀.mk)).toFun s =
      (ConcreteCategory.hom (FC := Fun) (SimplicialObject.δ X 0 ≫ ↾π₀.mk)).toFun s
⊢ SimplicialObject.δ X 1 ≫ ↾π₀.mk = SimplicialObject.δ X 0 ≫ ↾π₀.mk

Tactic:
ext s
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
⊢ (ConcreteCategory.hom (FC := Fun) (SimplicialObject.δ X 1 ≫ ↾π₀.mk)).toFun s =
    (ConcreteCategory.hom (FC := Fun) (SimplicialObject.δ X 0 ≫ ↾π₀.mk)).toFun s

Tactic:
π₀.sound (Edge.mk' s)

Premises used: SSet.π₀.sound, SSet.Edge.mk', SSet.π₀.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
⊢ (ConcreteCategory.hom (FC := Fun) (SimplicialObject.δ X 1 ≫ ↾π₀.mk)).toFun s =
    (ConcreteCategory.hom (FC := Fun) (SimplicialObject.δ X 0 ≫ ↾π₀.mk)).toFun s

Tactic:
exact π₀.sound (Edge.mk' s)

Premises used: SSet.π₀.sound, SSet.Edge.mk'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ Eq (α := s.pt)
    ((ConcreteCategory.hom (FC := Fun) s.π : (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt) x₀ :
      (fun (X : Type u) ↦ X) s.pt)
    ((ConcreteCategory.hom (FC := Fun) s.π : (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt) x₁ :
      (fun (X : Type u) ↦ X) s.pt)

Tactic:
simpa only [← e.src_eq, ← e.tgt_eq] using
        ConcreteCategory.congr_hom s.condition e.edge

Premises used: SSet.Edge.tgt_eq, CategoryTheory.Limits.Cofork.condition, CategoryTheory.ConcreteCategory.congr_hom, SSet.Edge.src_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
m :
  Cocone.pt (F := parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
      coforkπ₀ ⟶
    s.pt
hm : Cofork.π coforkπ₀ ≫ m = s.π
h :
  ∀ (x : X.π₀),
    (ConcreteCategory.hom (FC := Fun) m).toFun x =
      Fun.toFun
        (@ConcreteCategory.hom _ types Fun _ _ _ _ _
          ((fun (s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)) ↦
              (↾π₀.lift
                    (⇑(ConcreteCategory.hom (FC := Fun) s.π) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt)
                    ⋯ :
                Cocone.pt (F :=
                    parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                    coforkπ₀ ⟶
                  s.pt))
            s))
        x
⊢ m =
    (fun (s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)) ↦
        (↾π₀.lift
              (⇑(ConcreteCategory.hom (FC := Fun) s.π) :
                (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt)
              ⋯ :
          Cocone.pt (F :=
              parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
              coforkπ₀ ⟶
            s.pt))
      s

Tactic:
ext (x : π₀ X)

Premises used: SSet.π₀
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
m :
  Cocone.pt (F := parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
      coforkπ₀ ⟶
    s.pt
hm : Cofork.π coforkπ₀ ≫ m = s.π
x : X.π₀
h :
  ∀ (x : X _⦋0⦌),
    (ConcreteCategory.hom (FC := Fun) m).toFun (π₀.mk x) =
      Fun.toFun
        (@ConcreteCategory.hom _ types Fun _ _ _ _ _
          ((fun (s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)) ↦
              (↾π₀.lift
                    (⇑(ConcreteCategory.hom (FC := Fun) s.π) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt)
                    ⋯ :
                Cocone.pt (F :=
                    parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                    coforkπ₀ ⟶
                  s.pt))
            s))
        (π₀.mk x)
⊢ (ConcreteCategory.hom (FC := Fun) m).toFun x =
    Fun.toFun
      (@ConcreteCategory.hom _ types Fun _ _ _ _ _
        ((fun (s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)) ↦
            (↾π₀.lift
                  (⇑(ConcreteCategory.hom (FC := Fun) s.π) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt)
                  ⋯ :
              Cocone.pt (F :=
                  parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                  coforkπ₀ ⟶
                s.pt))
          s))
      x

Tactic:
induction x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
m :
  Cocone.pt (F := parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
      coforkπ₀ ⟶
    s.pt
hm : Cofork.π coforkπ₀ ≫ m = s.π
x : X _⦋0⦌
⊢ (ConcreteCategory.hom (FC := Fun) m).toFun (π₀.mk x) =
    Fun.toFun
      (@ConcreteCategory.hom _ types Fun _ _ _ _ _
        ((fun (s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)) ↦
            (↾π₀.lift
                  (⇑(ConcreteCategory.hom (FC := Fun) s.π) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt)
                  ⋯ :
              Cocone.pt (F :=
                  parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                  coforkπ₀ ⟶
                s.pt))
          s))
      (π₀.mk x)

Tactic:
ConcreteCategory.congr_hom hm _

Premises used: SSet.π₀.lift, CategoryTheory.ConcreteCategory.congr_hom, SSet.π₀.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
m :
  Cocone.pt (F := parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
      coforkπ₀ ⟶
    s.pt
hm : Cofork.π coforkπ₀ ≫ m = s.π
x : X _⦋0⦌
⊢ (ConcreteCategory.hom (FC := Fun) m).toFun (π₀.mk x) =
    Fun.toFun
      (@ConcreteCategory.hom _ types Fun _ _ _ _ _
        ((fun (s : Cofork (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)) ↦
            (↾π₀.lift
                  (⇑(ConcreteCategory.hom (FC := Fun) s.π) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) s.pt)
                  ⋯ :
              Cocone.pt (F :=
                  parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                  coforkπ₀ ⟶
                s.pt))
          s))
      (π₀.mk x)

Tactic:
exact ConcreteCategory.congr_hom hm _

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
w :
  ∀ (X : SSet.{u}) (s : SSet.evaluation _⦋HAdd.hAdd (α := ℕ) 0 1⦌.obj X),
    (ConcreteCategory.hom (FC := Fun)
            ((SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 1)) ≫ toπ₀NatTrans).app X)).toFun
        s =
      (ConcreteCategory.hom (FC := Fun)
            ((SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 0)) ≫ toπ₀NatTrans).app X)).toFun
        s
⊢ SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 1)) ≫ toπ₀NatTrans =
    SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 0)) ≫ toπ₀NatTrans

Tactic:
ext X s
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X_1 Y Z X : SSet
s : SSet.evaluation _⦋HAdd.hAdd (α := ℕ) 0 1⦌.obj X
⊢ (ConcreteCategory.hom (FC := Fun)
          ((SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 1)) ≫ toπ₀NatTrans).app X)).toFun
      s =
    (ConcreteCategory.hom (FC := Fun)
          ((SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 0)) ≫ toπ₀NatTrans).app X)).toFun
      s

Tactic:
π₀.sound (Edge.mk' s)

Premises used: SSet.π₀.sound, SSet.Edge.mk', SSet.π₀.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X_1 Y Z X : SSet
s : SSet.evaluation _⦋HAdd.hAdd (α := ℕ) 0 1⦌.obj X
⊢ (ConcreteCategory.hom (FC := Fun)
          ((SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 1)) ≫ toπ₀NatTrans).app X)).toFun
      s =
    (ConcreteCategory.hom (FC := Fun)
          ((SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 0)) ≫ toπ₀NatTrans).app X)).toFun
      s

Tactic:
exact π₀.sound (Edge.mk' s)

Premises used: SSet.π₀.sound, SSet.Edge.mk'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
⊢ Nonempty.{u + 1} X.π₀ ↔ X.Nonempty

Tactic:
⟨fun _ ↦ ⟨(π₀.mk_surjective (Classical.arbitrary (π₀ X))).choose⟩,
    fun _ ↦ ⟨.mk (Classical.arbitrary _)⟩⟩

Premises used: SSet.π₀, Nonempty.intro, SSet.π₀.mk_surjective, SimplexCategory.mk, Opposite.op, Iff.intro, Classical.arbitrary, Exists.choose, OfNat.ofNat, SSet.π₀.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X Y Z : SSet
inst : X.IsConnected
⊢ Nonempty.{u + 1} X.π₀

Tactic:
⟨π₀.mk (Classical.arbitrary _)⟩

Premises used: Nonempty.intro, Classical.arbitrary, SSet.π₀.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
h : X.IsPreconnected ∧ X.Nonempty
left : X.IsPreconnected
right : X.Nonempty
⊢ X.Nonempty

Tactic:
assumption
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero
Goal:
X : SSet
rw : X.IsPreconnected ∧ X.Nonempty ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)
rw₁ : X.IsPreconnected ∧ X.Nonempty ↔ Subsingleton.{u + 1} X.π₀ ∧ Nonempty.{u + 1} X.π₀
rw₂ rw₃ : X.IsPreconnected ∧ X.Nonempty ↔ Subsingleton.{u + 1} X.π₀ ∧ X.Nonempty
⊢ X.IsConnected ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)

Tactic:
rw [isConnected_iff, unique_iff_subsingleton_and_nonempty, π₀.nonempty_iff]

Premises used: SSet.isConnected_iff, unique_iff_subsingleton_and_nonempty, SSet.π₀.nonempty_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
n : SimplexCategory
⊢ IsFinitelyPresentable (stdSimplex.obj n)

Tactic:
inferInstanceAs (IsFinitelyPresentable.{u} (uliftYoneda.obj n))

Premises used: _private.0.SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
⊢ ∃ (Y : SSet.{u}) (_ : Y.Finite) (_ : IsFinitelyPresentable Y) (p : Y ⟶ X), Epi p

Tactic:
⟨∐ (fun (s : X.N) ↦ Δ[s.dim]), inferInstance, ?_,
    Sigma.desc (fun s ↦ yonedaEquiv.symm s.simplex), ?_⟩

Premises used: SSet.yonedaEquiv, SSet.S.simplex, inferInstance, SSet.stdSimplex, SSet.N.toS, SimplexCategory.mk, SSet.S.dim, Exists.intro, CategoryTheory.Limits.Sigma.desc, CategoryTheory.Limits.sigmaObj, Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
refine_1 : IsFinitelyPresentable.{u, u, u + 1} (C := SSet) (∐ fun (s : X.N) ↦ Δ[s.dim])
refine_2 :
  Epi.{u, u + 1} (C := SSet) (X := ∐ fun (s : X.N) ↦ Δ[s.dim]) (Y := X)
    (Sigma.desc fun (s : X.N) ↦ (Equiv.symm yonedaEquiv : (a : X _⦋s.dim⦌) → Δ[s.dim] ⟶ X) s.simplex)
⊢ ∃ (Y : SSet.{u}) (_ : Y.Finite) (_ : IsFinitelyPresentable Y) (p : Y ⟶ X), Epi p

Tactic:
refine ⟨∐ (fun (s : X.N) ↦ Δ[s.dim]), inferInstance, ?_,
    Sigma.desc (fun s ↦ yonedaEquiv.symm s.simplex), ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst_1 : X.Finite
refine_1 : HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0
inst :
  ∀ (k : Discrete X.N),
    IsCardinalPresentable (C := SSet) (Functor.obj (Discrete.functor fun (s : X.N) ↦ Δ[s.dim]) k) Cardinal.aleph0
⊢ IsFinitelyPresentable.{u, u, u + 1} (C := SSet) (∐ fun (s : X.N) ↦ Δ[s.dim])

Tactic:
apply +allowSynthFailures isCardinalPresentable_of_isColimit' _ (coproductIsCoproduct _)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.isCardinalPresentable_of_isColimit'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
⊢ Cardinal.aleph0 ≤ Cardinal.aleph0

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
⊢ HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0

Tactic:
exact hasCardinalLT_of_finite _ _ (by rfl)

Premises used: hasCardinalLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
s : Discrete X.N
⊢ IsCardinalPresentable Δ[s.as.dim] Cardinal.aleph0

Tactic:
infer_instance