awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1⦌
⊢ X.spine m
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    (X.spine (m + 1) x).interval 1 m ⋯
have zero : ∀ (x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌),
  X.spine 0
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        x) =
    (X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 sorry
Tactic: obtain _ | m := m
Cleared hypotheses: m, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1⦌
zero :
  ∀ (x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌),
    X.spine 0
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          x) =
      (X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯
⊢ X.spine m
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m⦌))
        x) =
    (X.spine (m + 1) x).interval 1 m ⋯
have succ : ∀ (m : ℕ) (x : X _⦋m + 1 + 1⦌),
  X.spine (m + 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
        x) =
    (X.spine (m + 1 + 1) x).interval 1 (m + 1) sorry
Tactic: obtain _ | m := m
Cleared hypotheses: m, x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
⊢ X.spine 0
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        x) =
    (X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯
have zero : Path.vertex (n := 0)
    (X.spine 0
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        x))
    0 =
  ((X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 sorry).vertex 0
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
x : X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
⊢ Path.vertex (n := 0)
      (X.spine 0
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          x))
      0 =
    ((X.spine (HAdd.hAdd (α := ℕ) 0 1) x).interval 1 0 ⋯).vertex 0
have zero : Eq (α := X _⦋0⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (X _⦋0⦌)) : (a : X _⦋0⦌) → X _⦋0⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋1⦌) → X _⦋0⦌) x : X _⦋0⦌) :
    X _⦋0⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) : (a : X _⦋1⦌) → X _⦋0⦌) x : X _⦋0⦌)
Tactic: simp [spine, Path.vertex, Truncated.Path.vertex, SimplicialObject.truncation,
      Truncated.spine, Path.interval, Truncated.Path.interval, Truncated.inclusion,
      Truncated.Hom.tr, ← SimplexCategory.δ_zero_eq_const, ← SimplicialObject.δ_def]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
        x) =
    (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯
have succ : ∀ (i : Fin (m + 1)),
  Path.arrow
      (X.spine (m + 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
          x))
      i =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) sorry).arrow i
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ Path.arrow
      (X.spine (m + 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋m + 1⦌))
          x))
      i =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
have succ : (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) sorry).arrow i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (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
have 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) sorry).arrow i
Tactic: rw [SimplicialObject.δ_def, ← Functor.map_comp_apply, ← op_comp,
      SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (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
have succ : ((X.spine (m + 1 + 1) x).interval 1 (m + 1) sorry).arrow i =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc i.succ).op) : (a : X _⦋m + 1 + 1⦌) → X _⦋1⦌) x
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 1 + (↑i : ℕ) = (↑i.succ : ℕ)
have rw : 1 + (↑i : ℕ) = (↑i : ℕ) + 1
Tactic: rw [Fin.val_succ, add_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
rw : 1 + (↑i : ℕ) = (↑i : ℕ) + 1
⊢ 1 + (↑i : ℕ) = (↑i.succ : ℕ)
have rw₁ : (↑i : ℕ) + 1 = (↑i : ℕ) + 1
Tactic: rw [Fin.val_succ, add_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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⦌)) (Path.arrow (stdSimplex.spineId (n + 2)) j)
have h : Path.arrow (stdSimplex.spineId (n + 2)) j = (↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌)
Tactic: convert! (horn.primitiveEdge.{u} h₀ hₙ j).2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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 = (↑(primitiveEdge h₀ hₙ j) : Δ[n + 2] _⦋1⦌)
have 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) : ℕ)
Tactic: ext a
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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)
⊢ (↑((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) : ℕ)
have h : (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩)) :
    ℕ)
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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, ⋯⟩)) :
      ℕ)
⊢ (↑((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) : ℕ)
have h₁ : (↑((Path.arrow (stdSimplex.spineId (n + 2)) j : (a : Fin (1 + 1)) → Fin (n + 2 + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩)) :
    ℕ)
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
Goal:
X : SSet
x : X.π₀
⊢ mapπ₀ (𝟙 X) x = x
have mk : ∀ (x : X _⦋0⦌), mapπ₀ (𝟙 X) (π₀.mk x) = π₀.mk x
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
Goal:
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
x : X.π₀
⊢ mapπ₀ (f ≫ g) x = mapπ₀ g (mapπ₀ f x)
have mk : ∀ (x : X _⦋0⦌), mapπ₀ (f ≫ g) (π₀.mk x) = mapπ₀ g (mapπ₀ f (π₀.mk x))
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
Goal:
X Y Z : SSet
⊢ SimplicialObject.δ X 1 ≫ ↾π₀.mk = SimplicialObject.δ X 0 ≫ ↾π₀.mk
have 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
Tactic: ext s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
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.π
⊢ 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
have 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)
                  sorry :
              Cocone.pt (F :=
                  parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                  coforkπ₀ ⟶
                s.pt))
          s))
      x
Tactic: ext (x : π₀ X)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
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.π₀
⊢ (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
have 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)
                  sorry :
              Cocone.pt (F :=
                  parallelPair (X := X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) (SimplicialObject.δ X 1) (SimplicialObject.δ X 0))
                  coforkπ₀ ⟶
                s.pt))
          s))
      (π₀.mk x)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
Goal:
X Y Z : SSet
⊢ SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 1)) ≫ toπ₀NatTrans =
    SSet.evaluation.map (Quiver.Hom.op (SimplexCategory.δ 0)) ≫ toπ₀NatTrans
have 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
Tactic: ext X s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
Goal:
X : SSet
⊢ X.IsConnected ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)
have rw : X.IsPreconnected ∧ X.Nonempty ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)
Tactic: rw [isConnected_iff, unique_iff_subsingleton_and_nonempty, π₀.nonempty_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
Goal:
X : SSet
rw : X.IsPreconnected ∧ X.Nonempty ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)
⊢ X.IsConnected ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)
have rw₁ : X.IsPreconnected ∧ X.Nonempty ↔ Subsingleton.{u + 1} X.π₀ ∧ Nonempty.{u + 1} X.π₀
Tactic: rw [isConnected_iff, unique_iff_subsingleton_and_nonempty, π₀.nonempty_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.PiZero (goal)
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.π₀
⊢ X.IsConnected ↔ Nonempty.{max 1 (u + 1)} (Unique X.π₀)
have rw₂ : X.IsPreconnected ∧ X.Nonempty ↔ Subsingleton.{u + 1} X.π₀ ∧ X.Nonempty
Tactic: rw [isConnected_iff, unique_iff_subsingleton_and_nonempty, π₀.nonempty_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
⊢ ∃ (Y : SSet.{u}) (_ : Y.Finite) (_ : IsFinitelyPresentable Y) (p : Y ⟶ X), Epi p
have refine_1 : IsFinitelyPresentable.{u, u, u + 1} (C := SSet) (∐ fun (s : X.N) ↦ Δ[s.dim])
Tactic: refine ⟨∐ (fun (s : X.N) ↦ Δ[s.dim]), inferInstance, ?_,
    Sigma.desc (fun s ↦ yonedaEquiv.symm s.simplex), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
refine_1 : IsFinitelyPresentable.{u, u, u + 1} (C := SSet) (∐ fun (s : X.N) ↦ Δ[s.dim])
⊢ ∃ (Y : SSet.{u}) (_ : Y.Finite) (_ : IsFinitelyPresentable Y) (p : Y ⟶ X), Epi p
have 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)
Tactic: refine ⟨∐ (fun (s : X.N) ↦ Δ[s.dim]), inferInstance, ?_,
    Sigma.desc (fun s ↦ yonedaEquiv.symm s.simplex), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
⊢ IsFinitelyPresentable.{u, u, u + 1} (C := SSet) (∐ fun (s : X.N) ↦ Δ[s.dim])
have refine_1 : HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0
Tactic: apply +allowSynthFailures isCardinalPresentable_of_isColimit' _ (coproductIsCoproduct _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
refine_1 : HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0
⊢ IsFinitelyPresentable.{u, u, u + 1} (C := SSet) (∐ fun (s : X.N) ↦ Δ[s.dim])
have inst : ∀ (k : Discrete X.N),
  IsCardinalPresentable (C := SSet) (Functor.obj (Discrete.functor fun (s : X.N) ↦ Δ[s.dim]) k) Cardinal.aleph0
Tactic: apply +allowSynthFailures isCardinalPresentable_of_isColimit' _ (coproductIsCoproduct _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
⊢ IsFinitelyPresentable X
have obtain : ∀ (Y : SSet.{u}), Y.Finite → IsFinitelyPresentable Y → ∀ (p : Y ⟶ X), Epi p → IsFinitelyPresentable X
Tactic: obtain ⟨Y, _, _, p, _⟩ := exists_epi_from_isCardinalPresentable X
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
⊢ IsFinitelyPresentable X
have obtain : ∀ (Z : SSet.{u}), Z.Finite → IsFinitelyPresentable Z → ∀ (q : Z ⟶ pullback p p), Epi q → IsFinitelyPresentable X
Tactic: obtain ⟨Z, _, _, q, _⟩ := exists_epi_from_isCardinalPresentable (pullback p p)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (hypothesis)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
⊢ IsFinitelyPresentable X
have this : Fact Cardinal.aleph0.IsRegular
Tactic: have := Cardinal.fact_isRegular_aleph0.{u}
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (hypothesis)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this : Fact Cardinal.aleph0.IsRegular
⊢ IsFinitelyPresentable X
have this₁ : IsRegularEpi p
Tactic: have := IsRegularEpiCategory.regularEpiOfEpi p
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsFinitelyPresentable X
have hK : HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0
Tactic: apply +allowSynthFailures isCardinalPresentable_of_isColimit' _
      (isCoequalizerEpiComp ((EffectiveEpi.getStruct p).isColimitCoforkOfIsPullback
        (IsPullback.of_hasPullback p p)) q) _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
hK : HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0
⊢ IsFinitelyPresentable X
have inst : ∀ (k : WalkingParallelPair),
  IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0
Tactic: apply +allowSynthFailures isCardinalPresentable_of_isColimit' _
      (isCoequalizerEpiComp ((EffectiveEpi.getStruct p).isColimitCoforkOfIsPullback
        (IsPullback.of_hasPullback p p)) q) _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.zero)
    Cardinal.aleph0
have inst : IsCardinalPresentable Z Cardinal.aleph0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Presentable (goal)
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.one)
    Cardinal.aleph0
have inst : IsCardinalPresentable Y Cardinal.aleph0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    Function.Injective (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
have rw : Function.Injective (α := Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (β := Fin (p + 1) × Fin (q + 1))
    (ULift.down ∘
      Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve p q).hom.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1))) _⦋n⦌))
          z)) ↔
  Function.Injective (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
    (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
              (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
            z :
          Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
      (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
Tactic: rw [← nonDegenerate_iff_of_mono (isoNerve p q).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_injective,
    ← Function.Injective.of_comp_iff ULift.down_injective]