awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
⊢ Factors (X := HomologicalComplex.X (obj X) (n + 1)) (objX Y (n + 1)) (arrow (objX X (n + 1)) ≫ f.app (op ⦋n + 1⦌))
have succ : Factors (X :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
    (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)))
  (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
  (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
⊢ Factors (X :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)))
    (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌))
have succ : ∀ (i : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
    Eq (α :=
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
          (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
        Y _⦋n⦌)
      ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌)) ≫
        Y.δ i.succ)
      0
Tactic: refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌)) ≫
      Y.δ i.succ)
    0
have succ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    Y _⦋n⦌)
  ((kernelSubobject (X.δ i.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
  0
Tactic: rw [Category.assoc, SimplicialObject.δ, ← f.naturality,
          ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
          Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
    0
have succ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    Y _⦋n⦌)
  ((kernelSubobject (X.δ i.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    (kernelSubobject (X.δ i.succ)).arrow ≫ X.δ i.succ ≫ f.app (op ⦋n⦌))
  0
Tactic: rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
succ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.δ i.succ ≫ f.app (op ⦋n⦌))
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
    0
have succ₁ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    Y _⦋n⦌)
  ((kernelSubobject (X.δ i.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    0 ≫ f.app (op ⦋n⦌))
  0
Tactic: rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
succ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.δ i.succ ≫ f.app (op ⦋n⦌))
    0
succ₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0 ≫ f.app (op ⦋n⦌))
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
    0
have succ₂ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    Y _⦋n⦌)
  ((kernelSubobject (X.δ i.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    0)
  0
Tactic: rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
succ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.δ i.succ ≫ f.app (op ⦋n⦌))
    0
succ₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0 ≫ f.app (op ⦋n⦌))
    0
succ₂ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0)
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      Y _⦋n⦌)
    ((kernelSubobject (X.δ i.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n⦌))
    0
have succ₃ : Eq.{v_1 + 1} (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    Y _⦋n⦌)
  0 0
Tactic: rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1) ⟶ HomologicalComplex.X (obj Y) n)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1))
      (HomologicalComplex.d (obj Y) (n + 1) n))
    (HomologicalComplex.d (obj X) (n + 1) n ≫
      (fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) n)
have zero : Eq (α := HomologicalComplex.X (obj X) (HAdd.hAdd (α := ℕ) 0 1) ⟶ HomologicalComplex.X (obj Y) 0)
  (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (HAdd.hAdd (α := ℕ) 0 1))
    ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) sorry) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.d (obj Y) (HAdd.hAdd (α := ℕ) 0 1) 0))
  (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) 0) (HomologicalComplex.d (obj X) (HAdd.hAdd (α := ℕ) 0 1) 0)
    ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) sorry) 0))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
zero :
  Eq (α := HomologicalComplex.X (obj X) (HAdd.hAdd (α := ℕ) 0 1) ⟶ HomologicalComplex.X (obj Y) 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (HAdd.hAdd (α := ℕ) 0 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.d (obj Y) (HAdd.hAdd (α := ℕ) 0 1) 0))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) 0) (HomologicalComplex.d (obj X) (HAdd.hAdd (α := ℕ) 0 1) 0)
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) 0))
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1) ⟶ HomologicalComplex.X (obj Y) n)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1))
      (HomologicalComplex.d (obj Y) (n + 1) n))
    (HomologicalComplex.d (obj X) (n + 1) n ≫
      (fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) n)
have succ : ∀ (n : ℕ),
  Eq (α := HomologicalComplex.X (obj X) (n + 1 + 1) ⟶ HomologicalComplex.X (obj Y) (n + 1))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) sorry) (n + 1 + 1))
      (HomologicalComplex.d (obj Y) (n + 1 + 1) (n + 1)))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) (n + 1)) (HomologicalComplex.d (obj X) (n + 1 + 1) (n + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) sorry) (n + 1)))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
⊢ Eq (α := HomologicalComplex.X (obj X) (HAdd.hAdd (α := ℕ) 0 1) ⟶ HomologicalComplex.X (obj Y) 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (HAdd.hAdd (α := ℕ) 0 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.d (obj Y) (HAdd.hAdd (α := ℕ) 0 1) 0))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) 0) (HomologicalComplex.d (obj X) (HAdd.hAdd (α := ℕ) 0 1) 0)
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) 0))
have zero : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤))
  (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (Y.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋1⦌)) sorry ≫
      𝟙
          (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋1⦌)) underlying
            (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (Y.δ k.succ))) ≫
        arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (Y.δ k.succ)) ≫ Y.δ 0 ≫ inv (arrow ⊤) :
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤))
  (CategoryStruct.comp (Y := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤)
      (𝟙
            (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
              (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))) ≫
          arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤) :
        Quiver.Hom.{v_1, u_1} (V := C)
          (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
            (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
          (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
      (factorThru ⊤ (arrow ⊤ ≫ f.app (op ⦋0⦌)) sorry :
        Quiver.Hom.{v_1, u_1} (V := C) (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤)
          (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤)) :
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋0⦌)) underlying ⊤))
Tactic: dsimp [objD, objX, ChainComplex.of.d]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
⊢ Eq (α := HomologicalComplex.X (obj X) (n + 1 + 1) ⟶ HomologicalComplex.X (obj Y) (n + 1))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj Y) (n + 1 + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1 + 1))
      (HomologicalComplex.d (obj Y) (n + 1 + 1) (n + 1)))
    (CategoryStruct.comp (Y := HomologicalComplex.X (obj X) (n + 1)) (HomologicalComplex.d (obj X) (n + 1 + 1) (n + 1))
      ((fun (n : ℕ) ↦ (objX Y n).factorThru ((objX X n).arrow ≫ f.app (op ⦋n⦌)) ⋯) (n + 1)))
have succ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))))
  (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (Y.δ k.succ))
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1 + 1⦌))
      sorry ≫
    if n + 1 + 1 = n + 1 + 1 then
      𝟙
          (Functor.obj (C := Subobject.{v_1, u_1} (Y _⦋n + 1 + 1⦌)) underlying
            (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (Y.δ k.succ))) ≫
        factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (Y.δ k.succ)) ≫ Y.δ 0) sorry
    else 0)
  ((if n + 1 + 1 = n + 1 + 1 then
      𝟙
          (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
            (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ≫
        factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) sorry
    else 0) ≫
    factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (Y.δ k.succ))
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ f.app (op ⦋n + 1⦌)) sorry)
Tactic: dsimp [objD, objX, ChainComplex.of.d]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.Basic (goal)
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ
have obtain : ∀ (σ : S _⦋n + 2⦌)
  (h :
    ∀ (j : Fin (n + 3)) (h : j ≠ i),
      Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            σ :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            (horn.face i j h) :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))),
  ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ
Tactic: obtain ⟨σ, h⟩ := filler σ₀ h₀ hₙ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.Basic (goal)
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          σ :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
⊢ ∃ (σ : Δ[n + 2] ⟶ S), σ₀ = Λ[n + 2, i].ι ≫ σ
have refine : σ₀ = Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ
Tactic: refine ⟨yonedaEquiv.symm σ, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.Basic (goal)
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          σ :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
⊢ σ₀ = Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ
have h₁ : ∀ (j : Fin (n + 1 + 2)) (h : j ≠ i),
  Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        (horn.face i j h) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ)
              (Opposite.op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        (horn.face i j h) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
Tactic: apply horn.hom_ext