awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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))
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 ⋯)
    (e (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 Δ₁) α₂)

Tactic:
refine ext _ _ rfl ?_

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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))
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 ⋯)) :
      (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))
⊢ 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 Δ₁) α₂))

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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 (α :=
    (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 ⋯)) :
      (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:
eq_of_heq h₁.2

Premises used: And.right, eq_of_heq
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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 (α :=
    (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 ⋯)) :
      (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:
exact eq_of_heq h₁.2

Premises used: And.right, eq_of_heq
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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 Δ
⊢ Epi (𝟙 (unop Δ))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp : A.EqId → A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
mpr : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ → A.EqId
⊢ A.EqId ↔ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
mp : (id Δ).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
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))
⊢ A.EqId

Tactic:
rcases A with ⟨_, ⟨f, hf⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ fst : SimplexCategoryᵒᵖ
f : unop Δ ⟶ unop fst
hf : Epi f
h : fst = Δ
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))
⊢ EqId (Δ := Δ)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop Δ ⟶ unop fst) ↦ Epi α) f hf))

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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))

Tactic:
ext _ _ rfl ?_

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.ext, CategoryTheory.SimplicialObject.Splitting.IndexSet.EqId, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
fst : SimplexCategoryᵒᵖ
f : unop fst ⟶ unop fst
hf : Epi f
mpr :
  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
⊢ EqId (Δ := fst)
    (Sigma.mk (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop fst ⟶ unop Δ' // Epi α }) fst
      (Subtype.mk (p := fun (α : unop fst ⟶ unop fst) ↦ Epi α) f hf))

Tactic:
refine ext _ _ rfl ?_

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.ext, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
fst : SimplexCategoryᵒᵖ
f : unop fst ⟶ unop fst
hf : Epi f
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
⊢ 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

Tactic:
simp only [eqToHom_refl, comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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)) =
    (id fst).e

Tactic:
eq_id_of_epi f

Premises used: SimplexCategory.eq_id_of_epi, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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)) =
    (id fst).e

Tactic:
exact eq_id_of_epi f

Premises used: SimplexCategory.eq_id_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
rw :
  A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ ↔
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ A.EqId ↔ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
rw [eqId_iff_eq]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp :
  A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ →
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
mpr :
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len →
    A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ ↔
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ
mp mp₁ : (unop Δ).len = (unop Δ).len
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
mpr : unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) = unop Δ
⊢ A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }) = Δ

Tactic:
rw [← unop_inj_iff]

Premises used: Opposite.unop_inj_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h mpr : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })) = unop Δ

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
exact h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
rw :
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len ↔
    (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
⊢ A.EqId ↔ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
rw [eqId_iff_len_eq]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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
mpr :
  (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len →
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len ↔
    (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len
mp mp₁ : (unop Δ).len ≤ (unop Δ).len
⊢ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len →
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
le_antisymm (len_le_of_epi A.e)

Premises used: SimplexCategory.len_le_of_epi, le_antisymm, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len →
    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len = (unop Δ).len

Tactic:
exact le_antisymm (len_le_of_epi A.e)

Premises used: SimplexCategory.len_le_of_epi, le_antisymm, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
mp : A.EqId → Mono A.e
mpr : Mono A.e → A.EqId
⊢ A.EqId ↔ Mono A.e

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
mp : Mono (id Δ).e
⊢ Mono A.e

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
mp : Mono (𝟙 (unop Δ))
⊢ Mono (id Δ).e

Tactic:
dsimp only [id, e]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 (unop Δ))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
mpr : (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
⊢ A.EqId

Tactic:
rw [eqId_iff_len_le]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_len_le
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
len_le_of_mono A.e

Premises used: SimplexCategory.len_le_of_mono, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono A.e
⊢ (unop Δ).len ≤ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
exact len_le_of_mono A.e

Premises used: SimplexCategory.len_le_of_mono, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
⊢ (A.pull θ).e ≫ image.ι (θ.unop ≫ A.e) = θ.unop ≫ A.e

Tactic:
image.fac _

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Limits.image.fac, CategoryTheory.Limits.image, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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 Δ
⊢ (s.cofan Δ).inj A =
    s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫ X.map A.e.op

Tactic:
rfl

Premises used: CategoryTheory.SimplicialObject.Splitting.summand, CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
⊢ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) = s.ι n

Tactic:
simp [IndexSet.id, IndexSet.e, cofan_inj_eq]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq, CategoryTheory.SimplicialObject.Splitting.IndexSet.id, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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 Δ
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
⊢ (s.cofan Δ).inj A ≫ f.app Δ =
    s.φ f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫ Y.map A.e.op

Tactic:
simp only [cofan_inj_eq_assoc, φ, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.φ, CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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 Δ
rw 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
⊢ 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:
rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
Z : C
Δ : SimplexCategoryᵒᵖ
f g : X.obj Δ ⟶ Z
h : ∀ (A : IndexSet Δ), (s.cofan Δ).inj A ≫ f = (s.cofan Δ).inj A ≫ g
⊢ f = g

Tactic:
Cofan.IsColimit.hom_ext (s.isColimit Δ) _ _ h

Premises used: CategoryTheory.SimplicialObject.Splitting.isColimit, CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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
h₁ : ∀ (Δ : SimplexCategory), Eq (α := X.obj (op Δ) ⟶ Y.obj (op Δ)) (f.app (op Δ)) (g.app (op Δ))
⊢ f = g

Tactic:
ext ⟨Δ⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
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
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 Δ)))
⊢ Eq (α := X.obj (op Δ) ⟶ Y.obj (op Δ)) (f.app (op Δ)) (g.app (op Δ))

Tactic:
apply s.hom_ext'

Premises used: CategoryTheory.SimplicialObject.Splitting.hom_ext'