awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A : IndexSet (op Δ)
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⦌)))
⊢ 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:
induction Δ using SimplexCategory.rec with | _ n
-- 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
n : ℕ
A : IndexSet (op ⦋n⦌)
h₁ :
  Eq (α := s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶ 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⦌)))
⊢ 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:
dsimp
-- 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
n : ℕ
A : IndexSet (op ⦋n⦌)
⊢ Eq (α := s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶ 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:
simp only [s.cofan_inj_comp_app, h]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_app
-- 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 :
  (A : IndexSet Δ) → s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Z
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.desc Δ F = F A

Tactic:
apply Cofan.IsColimit.fac

Premises used: CategoryTheory.Limits.Cofan.IsColimit.fac
-- 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
X Y : SimplicialObject.{v_1, u_1} C
s : X.Splitting
e : X ≅ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ (e.app Δ).hom = (cofan' s.N Y (fun (n : ℕ) ↦ s.ι n ≫ e.hom.app (op ⦋n⦌)) Δ).inj A

Tactic:
simp [cofan, cofan']

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan, CategoryTheory.SimplicialObject.Splitting.cofan'
-- 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 Δ₁
p : Δ₁ ⟶ Δ₂
inst_1 : Epi p.unop
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
⊢ (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)

Tactic:
dsimp [cofan]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan
-- 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 Δ₁
p : Δ₁ ⟶ Δ₂
inst_1 : Epi p.unop
rw :
  s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ₁ ⟶ unop Δ' // Epi α }))).len ≫ X.map (A.e.op ≫ p) =
    s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ₁ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (A.epiComp p).e.op
⊢ (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:
rw [assoc, ← X.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- 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 Δ₁
p : Δ₁ ⟶ Δ₂
inst_1 : Epi p.unop
⊢ s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ₁ ⟶ unop Δ' // Epi α }))).len ≫ X.map (A.e.op ≫ p) =
    s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ₁ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (A.epiComp p).e.op

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ₁ Φ₂ : S₁.Hom S₂
h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
rcases :
  ∀ (F₁ : S₁.X ⟶ S₂.X) (f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
    (c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n)
    (h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = Φ₂.f n),
    { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = Φ₂
⊢ Φ₁ = Φ₂

Tactic:
rcases Φ₁ with ⟨F₁, f₁, c₁⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ₂ : S₁.Hom S₂
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = Φ₂.f n
rcases :
  ∀ (F₂ : S₁.X ⟶ S₂.X) (f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
    (c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n)
    (h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n),
    { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₂, comm := c₂ }
⊢ { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = Φ₂

Tactic:
rcases Φ₂ with ⟨F₂, f₂, c₂⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
h₁ : ∀ (x : ℕ), f₁ x = f₂ x
⊢ f₁ = f₂

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
x : ℕ
⊢ f₁ x = f₂ x

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
⊢ f₁ = f₂

Tactic:
have h' : f₁ = f₂ := by
    ext
    apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
f₂ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₂ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₂, comm := c₂ }.f n
h' : f₁ = f₂
subst :
  ∀ (c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n)
    (h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n),
    { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₁, comm := c₂ }
⊢ { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₂, comm := c₂ }

Tactic:
subst h'
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
simp : F₁ = F₂
⊢ { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₁, comm := c₂ }

Tactic:
simp only [mk.injEq, and_true]

Premises used: and_true, CategoryTheory.SimplicialObject.Split.Hom.mk.injEq
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
h₁ : ∀ (n : ℕ), S₁.s.φ F₁ n = S₁.s.φ F₂ n
⊢ F₁ = F₂

Tactic:
apply S₁.s.hom_ext

Premises used: CategoryTheory.SimplicialObject.Split.s, CategoryTheory.SimplicialObject.Splitting.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
n : ℕ
h₁ : S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
⊢ S₁.s.φ F₁ n = S₁.s.φ F₂ n

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
n : ℕ
h₁ : f₁ n ≫ S₂.s.ι n = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
h₂ h₃ : f₁ n ≫ S₂.s.ι n = f₁ n ≫ S₂.s.ι n
⊢ S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)

Tactic:
rw [c₁, c₂]
-- 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
X Y Z : Split.{v_1, u_1} C
Φ₁₂ : X.Hom Y
Φ₂₃ : Y.Hom Z
n : ℕ
dsimp : X.s.ι n ≫ Φ₁₂.F.app (op ⦋n⦌) ≫ Φ₂₃.F.app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z.s.ι n
⊢ X.s.ι n ≫ (Φ₁₂.F ≫ Φ₂₃.F).app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z.s.ι n

Tactic:
dsimp
-- 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
X Y Z : Split.{v_1, u_1} C
Φ₁₂ : X.Hom Y
Φ₂₃ : Y.Hom Z
n : ℕ
⊢ X.s.ι n ≫ Φ₁₂.F.app (op ⦋n⦌) ≫ Φ₂₃.F.app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z.s.ι n

Tactic:
simp only [assoc, Split.Hom.comm_assoc, Split.Hom.comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Split.Hom.comm, CategoryTheory.SimplicialObject.Split.Hom.comm_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : ∀ (n : ℕ), Φ₁.f n = Φ₂.f n
⊢ Φ₁ = Φ₂

Tactic:
Hom.ext _ _ h

Premises used: CategoryTheory.SimplicialObject.Split.Hom.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
rw rw₁ : Φ₂.f = Φ₂.f
⊢ Φ₁.f = Φ₂.f

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
rw rw₁ : Φ₂.f n = Φ₂.f n
⊢ Φ₁.f n = Φ₂.f n

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : Split.{v_1, u_1} C
⊢ Hom.F (𝟙 S) = 𝟙 S.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : Split.{v_1, u_1} C
n : ℕ
⊢ Hom.f (𝟙 S) n = 𝟙 (S.s.N n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ S₃ : Split.{v_1, u_1} C
Φ₁₂ : S₁ ⟶ S₂
Φ₂₃ : S₂ ⟶ S₃
⊢ (Φ₁₂ ≫ Φ₂₃).F = Φ₁₂.F ≫ Φ₂₃.F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ S₃ : Split.{v_1, u_1} C
Φ₁₂ : S₁ ⟶ S₂
Φ₂₃ : S₂ ⟶ S₃
n : ℕ
⊢ (Φ₁₂ ≫ Φ₂₃).f n = Φ₁₂.f n ≫ Φ₂₃.f n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Split
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
rw :
  (S₁.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        S₁.X.map A.e.op) ≫
      Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A
rw₁ :
  (S₁.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        S₁.X.map A.e.op) ≫
      Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      S₂.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        S₂.X.map A.e.op
rw₂ :
  S₁.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      S₁.X.map A.e.op ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      S₂.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        S₂.X.map A.e.op
rw₃ :
  S₁.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      Φ.F.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
        S₂.X.map A.e.op =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      S₂.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        S₂.X.map A.e.op
rw₄ rw₅ :
  S₁.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      Φ.F.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
        S₂.X.map A.e.op =
    S₁.s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      Φ.F.app (op ⦋(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len⦌) ≫
        S₂.X.map A.e.op
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A

Tactic:
rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq, CategoryTheory.SimplicialObject.Split.s, CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Split.Hom.F, CategoryTheory.NatTrans.naturality, CategoryTheory.SimplicialObject.Split.Hom.comm_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
⊢ anodyneExtensions f

Tactic:
MorphismProperty.of_isIso anodyneExtensions f

Premises used: CategoryTheory.MorphismProperty.of_isIso, SSet.anodyneExtensions
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
⊢ anodyneExtensions = modelCategoryQuillen.J.rlp.llp

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, SSet.anodyneExtensions, CategoryTheory.MorphismProperty.rlp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ modelCategoryQuillen.J.rlp.llp Λ[n, i].ι

Tactic:
le_llp_rlp _ _ (modelCategoryQuillen.horn_ι_mem_J n i)

Premises used: SSet.modelCategoryQuillen.horn_ι_mem_J, CategoryTheory.MorphismProperty.le_llp_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ modelCategoryQuillen.J.rlp.llp Λ[n, i].ι

Tactic:
exact le_llp_rlp _ _ (modelCategoryQuillen.horn_ι_mem_J n i)

Premises used: SSet.modelCategoryQuillen.horn_ι_mem_J, CategoryTheory.MorphismProperty.le_llp_rlp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
n : ℕ
⊢ IsSmall.{u, u, u + 1} (C := SSet)
    (ofHoms (X := fun (i : Fin (n + 2)) ↦ Λ[n + 1, i].toSSet) (Y := fun (i : Fin (n + 2)) ↦ Δ[n + 1])
      fun (i : Fin (n + 2)) ↦ Λ[n + 1, i].ι)

Tactic:
isSmall_ofHoms ..

Premises used: CategoryTheory.MorphismProperty.isSmall_ofHoms
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
⊢ IsSmall.{u, u, u + 1} modelCategoryQuillen.J

Tactic:
isSmall_iSup ..

Premises used: SSet.modelCategoryQuillen.J, CategoryTheory.MorphismProperty.isSmall_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
hi : modelCategoryQuillen.J i
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑modelCategoryQuillen.J.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ modelCategoryQuillen.J.homFamily) f
⊢ ∃ (i_1 : ℕ),
    ofHoms (X := fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].toSSet) (Y := fun (i : Fin (i_1 + 2)) ↦ Δ[i_1 + 1])
      (fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].ι) i

Tactic:
simp only [modelCategoryQuillen.J, iSup_iff] at hi

Premises used: SSet.modelCategoryQuillen.J, CategoryTheory.MorphismProperty.iSup_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑modelCategoryQuillen.J.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ modelCategoryQuillen.J.homFamily) f
hi :
  ∃ (i_1 : ℕ),
    ofHoms (X := fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].toSSet) (Y := fun (i : Fin (i_1 + 2)) ↦ Δ[i_1 + 1])
      (fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].ι) i
obtain : ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : Fin (n + 2)), IsFinitelyPresentable Λ[n + 1, i].toSSet
⊢ IsFinitelyPresentable A

Tactic:
obtain ⟨n, ⟨i⟩⟩ := hi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
X_1 Y_1 : SSet
f : X_1 ⟶ Y_1
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑modelCategoryQuillen.J.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ modelCategoryQuillen.J.homFamily) f
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ IsFinitelyPresentable Λ[n + 1, i].toSSet

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
hi : modelCategoryQuillen.J i
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑modelCategoryQuillen.J.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ modelCategoryQuillen.J.homFamily) f
⊢ IsFinitelyPresentable A

Tactic:
have : IsFinitelyPresentable.{u} A := by
      simp only [modelCategoryQuillen.J, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
A B X Y : SSet
i : A ⟶ B
hi : modelCategoryQuillen.J i
f : X ⟶ Y
hf :
  RelativeCellComplex (α := fun (x : Cardinal.aleph0.ord.ToType) ↦ (↑modelCategoryQuillen.J.toSet : Type (u + 1))) (A :=
    fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦ (↑i : Arrow SSet).left)
    (B := fun (x : Cardinal.aleph0.ord.ToType) (i : (↑modelCategoryQuillen.J.toSet : Type (u + 1))) ↦
    (↑i : Arrow SSet).right) (fun (x : Cardinal.aleph0.ord.ToType) ↦ modelCategoryQuillen.J.homFamily) f
this : IsFinitelyPresentable A
⊢ Limits.PreservesColimit
    hf.toTransfiniteCompositionOfShape (α := fun (x : Cardinal.aleph0.ord.ToType) ↦
        (↑modelCategoryQuillen.J.toSet : Type (u + 1))).F
    (Functor.obj coyoneda (Opposite.op A))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
⊢ modelCategoryQuillen.J.HasSmallObjectArgument

Tactic:
⟨.aleph0, inferInstance, inferInstance, inferInstance⟩

Premises used: inferInstance, Cardinal.aleph0, CategoryTheory.MorphismProperty.HasSmallObjectArgument.mk, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
Goal:
rw :
  modelCategoryQuillen.J.rlp.llp =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts
rw₁ rw₂ :
  (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts
⊢ anodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts

Tactic:
rw [anodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]

Premises used: CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument, SSet.anodyneExtensions_eq_llp_rlp