awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.ι (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
have 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
Tactic: rw [assoc, ← X.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ Φ₁ = Φ₂
have 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₁⟩
Cleared hypotheses: Φ₁, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = Φ₂
have 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₂ }
Tactic: rcases Φ₂ with ⟨F₂, f₂, c₂⟩
Cleared hypotheses: Φ₂, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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₂
have h₁ : ∀ (x : ℕ), f₁ x = f₂ x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (hypothesis)
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₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₂, comm := c₂ }
have h' : f₁ = f₂
Tactic: have h' : f₁ = f₂ := by
    ext
    apply h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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₂
⊢ { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₂, comm := c₂ }
have 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₂ }
Tactic: subst h'
Cleared hypotheses: f₂, c₂, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ { F := F₁, f := f₁, comm := c₁ : S₁.Hom S₂ } = { F := F₂, f := f₁, comm := c₂ }
have simp : F₁ = F₂
Tactic: simp only [mk.injEq, and_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ F₁ = F₂
have h₁ : ∀ (n : ℕ), S₁.s.φ F₁ n = S₁.s.φ F₂ n
Tactic: apply S₁.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
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 : ℕ
⊢ S₁.s.φ F₁ n = S₁.s.φ F₂ n
have h₁ : S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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 : ℕ
⊢ S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
have h₁ : f₁ n ≫ S₂.s.ι n = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
Tactic: rw [c₁, c₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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⦌)
⊢ S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
have h₂ : f₁ n ≫ S₂.s.ι n = f₁ n ≫ S₂.s.ι n
Tactic: rw [c₁, c₂]
-- 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
X Y Z : Split.{v_1, u_1} C
Φ₁₂ : X.Hom Y
Φ₂₃ : Y.Hom Z
n : ℕ
⊢ X.s.ι n ≫ (Φ₁₂.F ≫ Φ₂₃.F).app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z.s.ι n
have dsimp : X.s.ι n ≫ Φ₁₂.F.app (op ⦋n⦌) ≫ Φ₂₃.F.app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z.s.ι n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f
have rw : Φ₂.f = Φ₂.f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
have rw : Φ₂.f n = Φ₂.f n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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 Δ
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A
have 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
Tactic: rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A
have 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
Tactic: rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A
have 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
Tactic: rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A
have 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
Tactic: rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Split (goal)
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
⊢ (S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ =
    Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (S₂.s.cofan Δ).inj A
have 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
Tactic: rw [S₁.s.cofan_inj_eq, S₂.s.cofan_inj_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (hypothesis)
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
have 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
Tactic: simp only [modelCategoryQuillen.J, iSup_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
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
⊢ IsFinitelyPresentable A
have obtain : ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : Fin (n + 2)), IsFinitelyPresentable Λ[n + 1, i].toSSet
Tactic: obtain ⟨n, ⟨i⟩⟩ := hi
Cleared hypotheses: A, B, i, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (hypothesis)
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
⊢ Limits.PreservesColimit
    hf.toTransfiniteCompositionOfShape (α := fun (x : Cardinal.aleph0.ord.ToType) ↦
        (↑modelCategoryQuillen.J.toSet : Type (u + 1))).F
    (Functor.obj coyoneda (Opposite.op A))
have this : IsFinitelyPresentable A
Tactic: have : IsFinitelyPresentable.{u} A := by
      simp only [modelCategoryQuillen.J, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
⊢ anodyneExtensions =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts
have rw : modelCategoryQuillen.J.rlp.llp =
  (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts
Tactic: rw [anodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
rw :
  modelCategoryQuillen.J.rlp.llp =
    (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
have 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
Tactic: rw [anodyneExtensions_eq_llp_rlp, llp_rlp_of_hasSmallObjectArgument]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
⊢ anodyneExtensions =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
have rw : modelCategoryQuillen.J.rlp.llp =
  ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Tactic: rw [anodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
rw :
  modelCategoryQuillen.J.rlp.llp =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
⊢ anodyneExtensions =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
have rw₁ : ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
  ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Tactic: rw [anodyneExtensions_eq_llp_rlp,
    SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
⊢ ∃ (P : (range A.ι).Pairing), P.IsRegular
have generalize : ∀ (B : X.Subcomplex) (h : range A.ι = B), ∃ (P : B.Pairing), P.IsRegular
Tactic: generalize h : Subcomplex.range A.ι = B
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
B : X.Subcomplex
h : range A.ι = B
⊢ ∃ (P : B.Pairing), P.IsRegular
have obtain : ∀ (P : B.Pairing) [P.IsRegular] (h : range B.ι = B), ∃ (P : B.Pairing), P.IsRegular
Tactic: obtain rfl : B = A := by simpa using h.symm
Cleared hypotheses: A, P, inst, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X : SSet
A : X.Subcomplex
hA : strongAnodyneExtensions A.ι
⊢ ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A
have obtain : Mono A.ι →
  ∀ (P : (Subcomplex.range A.ι).Pairing), P.IsRegular → ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A
Tactic: obtain ⟨_, P, _⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X : SSet
A : X.Subcomplex
hA : strongAnodyneExtensions A.ι
⊢ ∃ (P : A.Pairing), P.IsRegular
have obtain : ∀ (w : X.Subcomplex) (P : w.Pairing), P.IsRegular → ∀ (hA : strongAnodyneExtensions w.ι), ∃ (P : w.Pairing), P.IsRegular
Tactic: obtain ⟨_, P, _, rfl⟩ :
        ∃ (B : X.Subcomplex) (P : B.Pairing), P.IsRegular ∧ B = A := by
      obtain ⟨_, P, _⟩ := hA
      exact ⟨_, P, inferInstance, by simp⟩
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
⊢ SSet.anodyneExtensions (Y :=
    (TransfiniteCompositionOfShape.F
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := P.rankFunction.Cell) (A :=
            fun (j : ℕ) (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) P.rankFunction.relativeCellComplex)).obj
      (Order.succ j))
    ((TransfiniteCompositionOfShape.F
          (RelativeCellComplex.toTransfiniteCompositionOfShape (α := P.rankFunction.Cell) (A :=
            fun (j : ℕ) (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) P.rankFunction.relativeCellComplex)).map
      (CategoryTheory.homOfLE ⋯))
have refine : (coproducts.{u, u, u + 1}
      (ofHoms (X := fun (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) (P.rankFunction.basicCell j))).pushouts ≤
  SSet.anodyneExtensions
Tactic: refine (?_ : (_ : MorphismProperty _) ≤ _ ) _
        (P.rankFunction.relativeCellComplex.attachCells j hj).pushouts_coproducts
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
j : ℕ
hj : ¬IsMax j
⊢ (coproducts.{u, u, u + 1}
        (ofHoms (X := fun (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) (P.rankFunction.basicCell j))).pushouts ≤
    SSet.anodyneExtensions
have simp : ofHoms (X := fun (i : P.rankFunction.Cell j) ↦ i.horn.toSSet) (P.rankFunction.basicCell j) ≤ SSet.anodyneExtensions
Tactic: simp only [pushouts_le_iff, coproducts_le_iff]