awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 0] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 0]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 0] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
have a : ∀ (i : (↑{0}ᶜ : Type)),
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
Tactic: rw [horn_eq_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
i : (↑{0}ᶜ : Type)
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
have a : LE.le.{u} (α := Δ[2].Subcomplex)
  (stdSimplex.face
    {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
              ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋2⦌.len + 1))) sorry) :
          Fin (2 + 1))}ᶜ)
  (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
i : (↑{0}ᶜ : Type)
a :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex)
  (stdSimplex.face
    {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {0}ᶜ x)
              ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, sorry⟩ : Fin (⦋2⦌.len + 1))) sorry) :
          Fin (2 + 1))}ᶜ)
  (stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2})
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂
have commf : Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE sorry = stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 1 sorry)
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂
have commg : Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE sorry = stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 2 sorry)
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)
⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂
have comminl : Iso.hom (stdSimplex.facePairIso 0 1 sorry) ≫ Subcomplex.homOfLE sorry =
  ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 0) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)
comminl :
  Iso.hom (stdSimplex.facePairIso 0 1 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))
⊢ IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂
have comminr : Iso.hom (stdSimplex.facePairIso 0 2 sorry) ≫ Subcomplex.homOfLE sorry =
  ι₀₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 0]))
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 1] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}) Λ[2, 1]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1] ∧
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]
Tactic: rw [sup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 1}) Λ[2, 1] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 1]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 1] (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
have a : ∀ (i : (↑{1}ᶜ : Type)),
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
Tactic: rw [horn_eq_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
i : (↑{1}ᶜ : Type)
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
have a : LE.le.{u} (α := Δ[2].Subcomplex)
  (stdSimplex.face
    {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
              ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋2⦌.len + 1))) sorry) :
          Fin (2 + 1))}ᶜ)
  (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
i : (↑{1}ᶜ : Type)
a :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex)
  (stdSimplex.face
    {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {1}ᶜ x)
              ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, sorry⟩ : Fin (⦋2⦌.len + 1))) sorry) :
          Fin (2 + 1))}ᶜ)
  (stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2})
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂
have commf : Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE sorry = stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 1 sorry)
Tactic: apply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂
have commg : Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE sorry = stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 1 2 sorry)
Tactic: apply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 1 2 ⋯)
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂
have comminl : Iso.hom (stdSimplex.facePairIso 0 1 sorry) ≫ Subcomplex.homOfLE sorry =
  ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))
Tactic: apply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 1 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 1) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 1 ≫ Iso.hom (stdSimplex.facePairIso 1 2 ⋯)
comminl :
  Iso.hom (stdSimplex.facePairIso 0 1 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₁ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂
have comminr : Iso.hom (stdSimplex.facePairIso 1 2 sorry) ≫ Subcomplex.homOfLE sorry =
  ι₁₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 1]))
Tactic: apply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]
⊢ Eq.{u + 1} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 2] (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}) Λ[2, 2]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2] ∧
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]
Tactic: rw [sup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]
have a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
a : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2]
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {0, 2}) Λ[2, 2] ∧
    LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {1, 2}) Λ[2, 2]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ LE.le.{u} (α := Δ[2].Subcomplex) Λ[2, 2] (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
have a : ∀ (i : (↑{2}ᶜ : Type)),
  LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
Tactic: rw [horn_eq_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
i : (↑{2}ᶜ : Type)
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
have a : LE.le.{u} (α := Δ[2].Subcomplex)
  (stdSimplex.face
    {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {2}ᶜ x)
              ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋2⦌.len + 1))) sorry) :
          Fin (2 + 1))}ᶜ)
  (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
i : (↑{2}ᶜ : Type)
a :
  LE.le.{u} (α := Δ[2].Subcomplex)
    (stdSimplex.face
      {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
                Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {2}ᶜ x)
                ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) ⋯) :
            Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
⊢ LE.le.{u} (α := Δ[2].Subcomplex) (stdSimplex.face {(↑i : Fin (2 + 1))}ᶜ)
    (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
have a₁ : LE.le.{u} (α := Δ[2].Subcomplex)
  (stdSimplex.face
    {(↑(Subtype.mk (p := fun (x : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦
              Membership.mem (γ := Set (Fin (HAdd.hAdd (α := ℕ) 2 1))) {2}ᶜ x)
              ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋2⦌.len + 1))) sorry) :
          Fin (2 + 1))}ᶜ)
  (stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2})
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂
have commf : Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE sorry = stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 2 sorry)
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂
have commg : Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE sorry = stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 1 2 sorry)
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 1 2 ⋯)
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂
have comminl : Iso.hom (stdSimplex.facePairIso 0 2 sorry) ≫ Subcomplex.homOfLE sorry =
  ι₀₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 2]))
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
commf :
  Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 0 2 ⋯)
commg :
  Iso.hom (stdSimplex.faceSingletonIso 2) ≫ Subcomplex.homOfLE ⋯ =
    stdSimplex.δ 0 ≫ Iso.hom (stdSimplex.facePairIso 1 2 ⋯)
comminl :
  Iso.hom (stdSimplex.facePairIso 0 2 ⋯) ≫ Subcomplex.homOfLE ⋯ =
    ι₀₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 2]))
⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂
have comminr : Iso.hom (stdSimplex.facePairIso 1 2 sorry) ≫ Subcomplex.homOfLE sorry =
  ι₁₂ ≫ Iso.hom (Iso.refl (Subcomplex.toSSet (X := Δ[2]) Λ[2, 2]))
Tactic: fapply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ ⨆ (i_1 : (↑{i}ᶜ : Type)), stdSimplex.face {(↑i_1 : Fin (n + 1))}ᶜ = Λ[n, i]
have rw : Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (⨆ (i_1 : (↑{i}ᶜ : Type)), stdSimplex.face {(↑i_1 : Fin (n + 1))}ᶜ)
  (⨆ (j : (↑{i}ᶜ : Type)), stdSimplex.face {(↑j : Fin (n + 1))}ᶜ)
Tactic: rw [horn_eq_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j k : (↑{i}ᶜ : Type)
⊢ Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (stdSimplex.face {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ)
    (stdSimplex.face {(↑j : Fin (n + 1))}ᶜ ⊓ stdSimplex.face {(↑k : Fin (n + 1))}ᶜ)
have rw : Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (stdSimplex.face {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ)
  (stdSimplex.face ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ))
Tactic: rw [stdSimplex.face_inter_face]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j k : (↑{i}ᶜ : Type)
⊢ Eq.{u_1 + 1} (α := Δ[n].Subcomplex) (stdSimplex.face {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ)
    (stdSimplex.face ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ))
have e_S : Eq (α := Finset (Fin (n + 1))) {(↑j : Fin (n + 1)), (↑k : Fin (n + 1))}ᶜ ({(↑j : Fin (n + 1))}ᶜ ⊓ {(↑k : Fin (n + 1))}ᶜ)
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f g : Λ[n + 1, i].toSSet ⟶ X
h : ∀ (j : Fin (n + 2)) (hj : j ≠ i), ι i j hj ≫ f = ι i j hj ≫ g
⊢ f = g
have refine : ∀ (x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R) (j : Fin (n + 1 + 1))
  (hj : Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ j),
  Eq (α :=
    MultispanIndex.right (J := MultispanShape.ofLinearOrder (↑{i}ᶜ : Type))
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex sorry).toLinearOrder
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ⟶
      X)
    (Multicofork.π
        (Multicofork.map (CompleteLattice.MulticoequalizerDiagram.multicofork sorry).toLinearOrder Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ≫
      f)
    (Multicofork.π
        (Multicofork.map (CompleteLattice.MulticoequalizerDiagram.multicofork sorry).toLinearOrder Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : Fin (n + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1))) {i}ᶜ x) j hj) ≫
      g)
Tactic: refine Multicofork.IsColimit.hom_ext (isColimit i) (fun ⟨j, hj⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
g : Λ[n + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible.{u} (n := n) (X := X) (i := i) fun (j : Fin (n + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
have zero : ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 2)} (g : Λ[HAdd.hAdd (α := ℕ) 0 1, i].toSSet ⟶ X),
  horn.IsCompatible.{u} (n := 0) (X := X) (i := i) fun (j : Fin (HAdd.hAdd (α := ℕ) 0 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
Tactic: obtain _ | n := n
Cleared hypotheses: n, i, g
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
g : Λ[n + 1, i].toSSet ⟶ X
zero :
  ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 2)} (g : Λ[HAdd.hAdd (α := ℕ) 0 1, i].toSSet ⟶ X),
    horn.IsCompatible.{u} (n := 0) (X := X) (i := i) fun (j : Fin (HAdd.hAdd (α := ℕ) 0 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
⊢ horn.IsCompatible.{u} (n := n) (X := X) (i := i) fun (j : Fin (n + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
have succ : ∀ (n : ℕ) {i : Fin (n + 1 + 2)} (g : Λ[n + 1 + 1, i].toSSet ⟶ X),
  horn.IsCompatible.{u} (n := n + 1) (X := X) (i := i) fun (j : Fin (n + 1 + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
Tactic: obtain _ | n := n
Cleared hypotheses: n, i, g
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible.{u} (n := n + 1) (X := X) (i := i) fun (j : Fin (n + 1 + 2)) (hj : j ≠ i) ↦ ι i j hj ≫ g
have succ : ∀ (j k : Fin (n + 3)) (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k),
  (stdSimplex.δ (k.pred sorry) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred sorry) ≫ ι i k hk) ≫ g
Tactic: simp only [isCompatible_iff, ← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
hj : j ≠ i
hk : k ≠ i
hjk : j < k
⊢ (stdSimplex.δ (k.pred ⋯) ≫ ι i j hj) ≫ g = (stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk) ≫ g
have succ : stdSimplex.δ (k.pred sorry) ≫ ι i j hj = stdSimplex.δ (j.castPred sorry) ≫ ι i k hk
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j k : Fin (n + 3)
hj : j ≠ i
hk : k ≠ i
hjk : j < k
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j hj = stdSimplex.δ (j.castPred ⋯) ≫ ι i k hk
have succ : ∀ (j : Fin (n + 2)) (hj : j.castSucc ≠ i) (hjk : j.castSucc < k),
  stdSimplex.δ (k.pred sorry) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred sorry) ≫ ι i k hk
Tactic: obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (Fin.ne_last_of_lt hjk)
Cleared hypotheses: j, hj, hjk