awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
⊢ ModelCategory.{v_1, u_1} C
have this₁ : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
Tactic: have {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f] : WeakEquivalence (e.functor.map f) := by
    simpa [weakEquivalence_iff, h₃] using hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ MorphismProperty.HasTwoOutOfThreeProperty.{v_1, u_1} (weakEquivalences C)
have rw : (MorphismProperty.inverseImage (weakEquivalences D) e.functor).HasTwoOutOfThreeProperty
Tactic: rw [h₃]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ MorphismProperty.IsStableUnderRetracts.{v_1, u_1} (weakEquivalences C)
have rw : (MorphismProperty.inverseImage (weakEquivalences D) e.functor).IsStableUnderRetracts
Tactic: rw [h₃]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ MorphismProperty.IsStableUnderRetracts.{v_1, u_1} (fibrations C)
have rw : (MorphismProperty.inverseImage (fibrations D) e.functor).IsStableUnderRetracts
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ MorphismProperty.IsStableUnderRetracts.{v_1, u_1} (cofibrations C)
have rw : (MorphismProperty.inverseImage (cofibrations D) e.functor).IsStableUnderRetracts
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
A B X Y : C
x : A ⟶ B
x_1 : X ⟶ Y
h : Cofibration x
h_1 : WeakEquivalence x
h_2 : Fibration x_1
⊢ HasLiftingProperty x x_1
have rw : HasLiftingProperty (e.functor.map x) (e.functor.map x_1)
Tactic: rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
A B X Y : C
x : A ⟶ B
x_1 : X ⟶ Y
h : Cofibration x
h_1 : Fibration x_1
h_2 : WeakEquivalence x_1
⊢ HasLiftingProperty x x_1
have rw : HasLiftingProperty (e.functor.map x) (e.functor.map x_1)
Tactic: rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ MorphismProperty.HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)
have rw : (MorphismProperty.inverseImage (trivialCofibrations D) e.functor).HasFactorization
  (MorphismProperty.inverseImage (fibrations D) e.functor)
Tactic: rw [h₁', h₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.ModelCategory.Transport (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
inst_2 : ModelCategory.{v_2, u_2} D
inst_3 : CategoryWithCofibrations.{v_1, u_1} C
inst_4 : CategoryWithFibrations.{v_1, u_1} C
inst_5 : CategoryWithWeakEquivalences.{v_1, u_1} C
e : CategoryTheory.Equivalence.{v_1, v_2, u_1, u_2} C D
h₁ : cofibrations C = MorphismProperty.inverseImage (cofibrations D) e.functor
h₂ : fibrations C = MorphismProperty.inverseImage (fibrations D) e.functor
h₃ : weakEquivalences C = MorphismProperty.inverseImage (weakEquivalences D) e.functor
h₁' : trivialCofibrations C = MorphismProperty.inverseImage (trivialCofibrations D) e.functor
h₂' : trivialFibrations C = MorphismProperty.inverseImage (trivialFibrations D) e.functor
this_1 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Cofibration f], Cofibration (e.functor.map f)
this_2 : ∀ {X Y : C} (f : X ⟶ Y) [hf : Fibration f], Fibration (e.functor.map f)
this : ∀ {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f], WeakEquivalence (e.functor.map f)
⊢ MorphismProperty.HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)
have rw : (MorphismProperty.inverseImage (cofibrations D) e.functor).HasFactorization
  (MorphismProperty.inverseImage (trivialFibrations D) e.functor)
Tactic: rw [h₁, h₂']
-- 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 : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)) ⟶
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying (objX X (n + 1))
have refine : Factors (X := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1))) (objX X (n + 1))
  (arrow (objX X (n + 1 + 1)) ≫ X.δ 0)
Tactic: refine factorThru _ (arrow _ ≫ X.δ (0 : Fin (n + 3))) ?_
-- 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 : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Factors (X := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)))
    (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ X.δ 0)
have refine : ∀ (i : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
    (kernelSubobject (X.δ i.succ)).Factors (X :=
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)))
      (arrow (objX X (n + 1 + 1)) ≫ X.δ 0)
Tactic: refine (finset_inf_factors _).mpr fun i _ => ?_
-- 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 : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ (kernelSubobject (X.δ i.succ)).Factors (X :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)))
    (arrow (objX X (n + 1 + 1)) ≫ X.δ 0)
have w : Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)) ⟶ X _⦋n⦌)
  ((arrow (objX X (n + 1 + 1)) ≫ X.δ 0) ≫ X.δ i.succ) 0
Tactic: apply 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 : SimplicialObject.{v_1, u_1} C
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 + 1⦌)) underlying (objX X (n + 1 + 1)) ⟶ X _⦋n⦌)
    ((arrow (objX X (n + 1 + 1)) ≫ X.δ 0) ≫ X.δ i.succ) 0
have w : Eq (α :=
  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)) ⟶
    X _⦋n⦌)
  ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ i.succ) 0
Tactic: dsimp [objX]
-- 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 : SimplicialObject.{v_1, u_1} C
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 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ i.succ) 0
have w : Eq (α :=
  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)) ⟶
    X _⦋n⦌)
  (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ i.succ.succ ≫ X.δ 0) 0
Tactic: rw [Category.assoc, ← Fin.castSucc_zero, ← X.δ_comp_δ (Fin.zero_le i.succ)]
-- 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 : SimplicialObject.{v_1, u_1} C
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 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
have w : Eq (α :=
  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)) ⟶
    X _⦋n⦌)
  (((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
      (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
    X.δ i.succ.succ ≫ X.δ 0)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, 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 : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
w :
  Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    (((kernelSubobject (X.δ i.succ.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
      X.δ i.succ.succ ≫ X.δ 0)
    0
⊢ Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
have w₁ : Eq (α :=
  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)) ⟶
    X _⦋n⦌)
  ((kernelSubobject (X.δ i.succ.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    (kernelSubobject (X.δ i.succ.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, 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 : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
w :
  Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    (((kernelSubobject (X.δ i.succ.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
      X.δ i.succ.succ ≫ X.δ 0)
    0
w₁ :
  Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    ((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
⊢ Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
have w₂ : Eq (α :=
  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)) ⟶
    X _⦋n⦌)
  ((kernelSubobject (X.δ i.succ.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    0 ≫ X.δ 0)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, 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 : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
w :
  Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    (((kernelSubobject (X.δ i.succ.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
      X.δ i.succ.succ ≫ X.δ 0)
    0
w₁ :
  Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    ((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
w₂ :
  Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    ((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0 ≫ X.δ 0)
    0
⊢ Eq (α :=
    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)) ⟶
      X _⦋n⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
have w₃ : Eq (α :=
  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)) ⟶
    X _⦋n⦌)
  ((kernelSubobject (X.δ i.succ.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    0)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]