awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Eq (α := (k : Fin ((unop Δ).len + 1)) × (Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1)))
    ((fun (A : IndexSet Δ) ↦
        (Sigma.mk (β := fun (k : Fin ((unop Δ).len + 1)) ↦ Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))
            ⟨(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len, ⋯⟩
            (⇑(Hom.toOrderHom A.e) : (a : Fin ((unop Δ).len + 1)) → Fin ((unop A.fst).len + 1)) :
          (k : Fin ((unop Δ).len + 1)) × (Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))
    ((fun (A : IndexSet Δ) ↦
        (Sigma.mk (β := fun (k : Fin ((unop Δ).len + 1)) ↦ Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))
            ⟨(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len, ⋯⟩
            (⇑(Hom.toOrderHom A.e) : (a : Fin ((unop Δ).len + 1)) → Fin ((unop A.fst).len + 1)) :
          (k : Fin ((unop Δ).len + 1)) × (Fin ((unop Δ).len + 1) → Fin ((↑k : ℕ) + 1))))
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))
⊢ Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂)
have h₂ : Δ₁.len = Δ₂.len ∧
  HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
    (⇑(Hom.toOrderHom
          (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
      (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
    (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
    (⇑(Hom.toOrderHom
          (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
      (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
Tactic: simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
⊢ Δ₁ = Δ₂
have len : Δ₁.len = Δ₂.len
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
⊢ Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂)
have h₂ : Δ₁ = Δ₂
Tactic: have h₂ : Δ₁ = Δ₂ := by
        ext1
        simpa only [Fin.mk_eq_mk] using h₁.1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
Δ₂ : SimplexCategory
α₂ : { α : unop Δ ⟶ unop (op Δ₂) // Epi α }
h₁ :
  Δ₁.len = Δ₂.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₂.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₂.len + 1))
h₂ : Δ₁ = Δ₂
⊢ Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₂) α₂)
have subst : ∀ (α₂ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α })
  (h₁ :
    Δ₁.len = Δ₁.len ∧
      HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
        (⇑(Hom.toOrderHom
              (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
          (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
        (β := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
        (⇑(Hom.toOrderHom
              (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))) :
          (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))),
  Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂)
Tactic: subst h₂
Cleared hypotheses: Δ₂, α₂, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ α₂ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
h₁ :
  Δ₁.len = Δ₁.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
⊢ Eq (α := IndexSet Δ) (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂)
have refine : Eq (α :=
  unop Δ ⟶
    unop
      (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂)))
  (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁) ≫ eqToHom sorry)
  (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))
Tactic: refine ext _ _ rfl ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ₁ : SimplexCategory
α₁ α₂ : { α : unop Δ ⟶ unop (op Δ₁) // Epi α }
h₁ :
  Δ₁.len = Δ₁.len ∧
    HEq (α := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
      (β := Fin ((unop Δ).len + 1) → Fin (Δ₁.len + 1))
      (⇑(Hom.toOrderHom
            (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))) :
        (a : Fin ((unop Δ).len + 1)) → Fin (Δ₁.len + 1))
⊢ Eq (α :=
    unop Δ ⟶
      unop
        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
          (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂)))
    (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁) ≫ eqToHom ⋯)
    (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))
have a : Eq (α :=
  (a : Fin ((unop Δ).len + 1)) →
    Fin
      ((unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
              (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))).len +
        1))
  (⇑(Hom.toOrderHom
        (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₁) ≫ eqToHom sorry)) :
    (a : Fin ((unop Δ).len + 1)) → Fin ((unop ⟨op Δ₁, α₂⟩.fst).len + 1))
  (⇑(Hom.toOrderHom (e (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) (op Δ₁) α₂))) :
    (a : Fin ((unop Δ).len + 1)) → Fin ((unop ⟨op Δ₁, α₂⟩.fst).len + 1))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
have mp : A.EqId → A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp : A.EqId → A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
⊢ A.EqId ↔ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
have mpr : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ → A.EqId
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
have mp : (id Δ).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
⊢ A.EqId
have mpr : ∀ (fst : SimplexCategoryᵒᵖ) (f : unop Δ ⟶ unop fst) (hf : Epi f)
  (h :
    Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) fst
          (Subtype.mk (p := fun (α : unop Δ ⟶ unop fst) ↦ Epi α) f hf)) =
      Δ),
  EqId (Δ := Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop fst) ↦ Epi α) f hf))
Tactic: rcases A with ⟨_, ⟨f, hf⟩⟩
Cleared hypotheses: A, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ fst : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst
hf : Epi f
h : fst = Δ
⊢ EqId (Δ := Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop fst) ↦ Epi α) f hf))
have mpr : ∀ (f : unop fst ⟶ unop fst) (hf : Epi f),
  EqId (Δ := fst)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop fst ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop fst ⟶ unop fst) ↦ Epi α) f hf))
Tactic: subst h
Cleared hypotheses: Δ, f, hf, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
fst : SimplexCategoryᵒᵖ
f : unop fst ⟶ unop fst
hf : Epi f
⊢ EqId (Δ := fst)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop fst ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop fst ⟶ unop fst) ↦ Epi α) f hf))
have mpr : e
      (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop fst ⟶ unop Δ' // Epi α }) fst
        (Subtype.mk (p := fun (α : unop fst ⟶ unop fst) ↦ Epi α) f hf)) ≫
    eqToHom sorry =
  (id fst).e
Tactic: refine ext _ _ rfl ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
fst : SimplexCategoryᵒᵖ
f : unop fst ⟶ unop fst
hf : Epi f
⊢ e
        (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop fst ⟶ unop Δ' // Epi α }) fst
          (Subtype.mk (p := fun (α : unop fst ⟶ unop fst) ↦ Epi α) f hf)) ≫
      eqToHom ⋯ =
    (id fst).e
have mpr : e
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop fst ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop fst ⟶ unop fst) ↦ Epi α) f hf)) =
  (id fst).e
Tactic: simp only [eqToHom_refl, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
have rw : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ ↔
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
Tactic: rw [eqId_iff_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ ↔
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
have mp : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ →
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp :
  A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ →
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ ↔
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
have mpr : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len →
  A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
have mp : (unop Δ).len = (unop Δ).len
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
have mpr : unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) = unop Δ
Tactic: rw [← unop_inj_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have rw : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len ↔
  (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
Tactic: rw [eqId_iff_len_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len ↔
    (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have mp : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len →
  (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp :
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len →
    (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len ↔
    (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have mpr : (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len →
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
have mp : (unop Δ).len ≤ (unop Δ).len
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ Mono A.e
have mp : A.EqId → Mono A.e
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp : A.EqId → Mono A.e
⊢ A.EqId ↔ Mono A.e
have mpr : Mono A.e → A.EqId
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono A.e
have mp : Mono (id Δ).e
Tactic: subst h
Cleared hypotheses: A, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
⊢ Mono (id Δ).e
have mp : Mono (𝟙 (unop Δ))
Tactic: dsimp only [id, e]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ A.EqId
have mpr : (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
Tactic: rw [eqId_iff_len_le]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
s : X.Splitting
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ f.app Δ =
    s.φ f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫ Y.map A.e.op
have simp : s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    X.map A.e.op ≫ f.app Δ =
  s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    f.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
      Y.map A.e.op
Tactic: simp only [cofan_inj_eq_assoc, φ, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
s : X.Splitting
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ f.app Δ =
    s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      f.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
        Y.map A.e.op
have rw : s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    f.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
      Y.map A.e.op =
  s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
    f.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
      Y.map A.e.op
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
⊢ f = g
have h₁ : ∀ (Δ : SimplexCategory), Eq (α := X.obj (op Δ) ⟶ Y.obj (op Δ)) (f.app (op Δ)) (g.app (op Δ))
Tactic: ext ⟨Δ⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
⊢ Eq (α := X.obj (op Δ) ⟶ Y.obj (op Δ)) (f.app (op Δ)) (g.app (op Δ))
have h₁ : ∀ (A : IndexSet (op Δ)),
  Eq (α := summand s.N (op Δ) A ⟶ Y.obj (op Δ))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op Δ))) (s.cofan (op Δ)))
      (Cofan.inj (s.cofan (op Δ)) A) (f.app (op Δ)))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op Δ))) (s.cofan (op Δ)))
      (Cofan.inj (s.cofan (op Δ)) A) (g.app (op Δ)))
Tactic: apply s.hom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
s : X.Splitting
f g : X ⟶ Y
h : ∀ (n : ℕ), s.φ f n = s.φ g n
Δ : SimplexCategory
A : IndexSet (op Δ)
⊢ Eq (α := summand s.N (op Δ) A ⟶ Y.obj (op Δ))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op Δ))) (s.cofan (op Δ)))
      (Cofan.inj (s.cofan (op Δ)) A) (f.app (op Δ)))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op Δ))) (s.cofan (op Δ)))
      (Cofan.inj (s.cofan (op Δ)) A) (g.app (op Δ)))
have h₁ : ∀ (n : ℕ) (A : IndexSet (op ⦋n⦌)),
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ Y _⦋n⦌)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (f.app (op ⦋n⦌)))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (g.app (op ⦋n⦌)))
Tactic: induction Δ using SimplexCategory.rec with | _ n
Cleared hypotheses: Δ, A
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst_1 : Epi p.unop
⊢ (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)
have dsimp : (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ₁ ⟶ unop Δ' // Epi α }))).len ≫ X.map A.e.op) ≫
    X.map p =
  s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ₁ ⟶ unop Δ' // Epi α }))).len ≫
    X.map (A.epiComp p).e.op
Tactic: dsimp [cofan]