awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
⊢ Eq (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
have this : LE.le (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) j : Fin (⦋1⦌.len + 1))
  ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
Tactic: have := f.toOrderHom.monotone hij
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
this :
  LE.le (α := Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) j : Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
⊢ Eq (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
have neg : ∀
  (hS :
    Finset.Nonempty (α := Fin (n + 1))
      {x : Fin (n + 1) |
        Eq (α := Fin 2) ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) x : Fin 2)
          (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)})
  (hj :
    Eq (α := Fin 2) ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) j : Fin 2)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌))
  (hij : j ≤ i)
  (this :
    LE.le (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) i : Fin 2)),
  Eq (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) i : Fin 2)
Tactic: simp_all [ConcreteCategory.hom, S]
Cleared hypotheses: hS, hj, hij, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
⊢ ∃ (a : Fin (n + 2)), toMk₁ a = f
have neg : ∀ (i : Fin (⦋n⦌.len + 1)),
  Eq (α := Fin (⦋1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n⦌) (toMk₁ (Fin.last (n + 1))) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
Tactic: refine ⟨Fin.last _, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n⦌) (toMk₁ (Fin.last (n + 1))) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
have neg : Eq (α := Fin 2) (if i.castSucc < Fin.last (n + 1) then 0 else 1 : Fin 2)
  ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : Fin (n + 1)) → Fin 2)
      i :
    Fin 2)
Tactic: dsimp [toMk₁_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin 2) (if i.castSucc < Fin.last (n + 1) then 0 else 1 : Fin 2)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
have neg : Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
  ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : Fin (n + 1)) → Fin 2)
      i :
    Fin 2)
Tactic: rw [if_pos (by simp)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
have neg : ∀ (j : Fin 2)
  (hj :
    (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        i =
      j),
  Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
Tactic: obtain ⟨j, hj⟩ : ∃ (j : Fin 2), f i = j := ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin 2
hj :
  (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      i =
    j
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
have neg : ∀
  (hj :
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩ : Fin (⦋1⦌.len + 1))),
  Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
Tactic: fin_cases j
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin 2
hj :
  (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      i =
    j
neg :
  ∀
    (hj :
      Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
            i :
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))),
    Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin (n + 1)) → Fin 2)
          i :
        Fin 2)
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
have neg₁ : ∀
  (hj :
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩ : Fin (⦋1⦌.len + 1))),
  Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
Tactic: fin_cases j
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (hypothesis)
Goal:
n : ℕ
inst : NeZero n
⊢ (inclusion n).Initial
have this : 0 < n
Tactic: have := Nat.pos_of_neZero n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (goal)
Goal:
n : ℕ
inst : NeZero n
this : 0 < n
⊢ (inclusion n).Initial
have out : ∀ (d : SimplexCategory), IsConnected (CostructuredArrow (inclusion n) d)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (hypothesis)
Goal:
n : ℕ
inst : NeZero n
this : 0 < n
Δ : SimplexCategory
⊢ IsConnected (CostructuredArrow (inclusion n) Δ)
have this₁ : Nonempty (CostructuredArrow (inclusion n) Δ)
Tactic: have : Nonempty (CostructuredArrow (inclusion n) Δ) := ⟨⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ 0 ⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (goal)
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
⊢ IsConnected (CostructuredArrow (inclusion n) Δ)
have out : ∀ (j₁ j₂ : CostructuredArrow (inclusion n) Δ), Zigzag j₁ j₂
Tactic: apply zigzag_isConnected
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (goal)
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
⊢ Zigzag
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁,
      right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f : Comma (inclusion n) (Functor.fromPUnit Δ) }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
      right := { as := PUnit.unit }, hom := f' }
have out : Zigzag
  { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋0⦌ sorry,
    right := { as := PUnit.unit },
    hom :=
      ⦋0⦌.const (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} })
        ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₁, property := hΔ₁ })) →
              (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
          0) }
  { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
    right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }
Tactic: apply Zigzag.trans (j₂ := ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f 0)⟩)
    (.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Truncated (hypothesis)
Goal:
n m : ℕ
inst : NeZero n
hm : n ≤ m
⊢ (incl n m ⋯).Initial
have this : (incl n m hm ⋙ inclusion m).Initial
Tactic: have : (incl n m hm ⋙ inclusion m).Initial :=
    Functor.initial_of_natIso (inclCompInclusion (by lia)).symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
K x : PreAbstractSimplicialComplex ι
h :
  Eq.{u_1 + 1} (α := Set (Finset ι)) ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) K)
    ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) x)
⊢ K = x
have mk : ∀ (faces : Set (Finset ι)) (isRelLowerSet_faces : IsRelLowerSet faces Finset.Nonempty),
  Eq.{u_1 + 1} (α := Set (Finset ι))
      ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces)
        { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces })
      ((fun (K : PreAbstractSimplicialComplex ι) ↦ K.faces) x) →
    { faces := faces, isRelLowerSet_faces := isRelLowerSet_faces : PreAbstractSimplicialComplex ι } = x
Tactic: cases K
Cleared hypotheses: K, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : Membership.mem (γ := Set (Finset β)) ((fun (s : Finset α) ↦ Finset.image f s) '' K.faces) x
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset β⦄,
      b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset β)) ((fun (s : Finset α) ↦ Finset.image f s) '' K.faces) b
have h₁ : ∃ x_1 ∈ K.faces, Finset.image f x_1 = x
Tactic: simp only [Set.mem_image] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : ∃ x_1 ∈ K.faces, Finset.image f x_1 = x
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ≤ x → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
have obtain : ∀ (s' : Finset α) (hs' : s' ∈ K.faces),
  (Finset.image f s').Nonempty ∧
    ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
Tactic: obtain ⟨s', hs', rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty ∧
    ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
have left : (Finset.image f s').Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
left : (Finset.image f s').Nonempty
⊢ (Finset.image f s').Nonempty ∧
    ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
have right : ∀ ⦃b : Finset β⦄, b ≤ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
t : Finset β
hts : t ≤ Finset.image f s'
ht : t.Nonempty
⊢ ∃ x ∈ K.faces, Finset.image f x = t
have right : ∀ (t' : Finset α) (ht' : t' ⊆ s') (hts : Finset.image f t' ≤ Finset.image f s') (ht : (Finset.image f t').Nonempty),
  ∃ x ∈ K.faces, Finset.image f x = Finset.image f t'
Tactic: obtain ⟨t', ht', rfl⟩ := Finset.subset_image_iff.mp hts
Cleared hypotheses: t, hts, ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
have left : x.Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
left : x.Nonempty
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
have right : ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ x.Nonempty
have left : Finset.Nonempty (α := ι) {v}
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (hypothesis)
Goal:
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t
have x₁ : t = ∅ ∨ t = {v}
Tactic: cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
        | inl h => exact (ht.ne_empty h).elim
        | inr h => exact ⟨v, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x x_1 : AbstractSimplicialComplex ι
h :
  Eq.{u_1 + 1} (α := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) x)
    ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) x_1)
⊢ x = x_1
have faces : ∀ (x_2 : Finset ι), x_2 ∈ x.faces ↔ x_2 ∈ x_1.faces
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} b
have left : x.Nonempty
Tactic: constructor