awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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
rw : HasLiftingProperty (e.functor.map x) (e.functor.map x_1)
⊢ HasLiftingProperty x x_1

Tactic:
rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.hasLiftingProperty_iff_of_isEquivalence
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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 (e.functor.map x) (e.functor.map x_1)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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)
rw :
  (MorphismProperty.inverseImage (trivialCofibrations D) e.functor).HasFactorization
    (MorphismProperty.inverseImage (fibrations D) e.functor)
⊢ MorphismProperty.HasFactorization.{v_1, u_1} (trivialCofibrations C) (fibrations C)

Tactic:
rw [h₁', h₂]
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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.inverseImage (trivialCofibrations D) e.functor).HasFactorization
    (MorphismProperty.inverseImage (fibrations D) e.functor)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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)
rw :
  (MorphismProperty.inverseImage (cofibrations D) e.functor).HasFactorization
    (MorphismProperty.inverseImage (trivialFibrations D) e.functor)
⊢ MorphismProperty.HasFactorization.{v_1, u_1} (cofibrations C) (trivialFibrations C)

Tactic:
rw [h₁, h₂']
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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.inverseImage (cofibrations D) e.functor).HasFactorization
    (MorphismProperty.inverseImage (trivialFibrations D) e.functor)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.ModelCategory.Transport
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)
⊢ ModelCategory.{v_1, u_1} C

Tactic:
exact {
    cm1a := ⟨fun _ _ _ ↦ Adjunction.hasLimitsOfShape_of_equivalence e.functor⟩
    cm1b := ⟨fun _ _ _ ↦ Adjunction.hasColimitsOfShape_of_equivalence e.functor⟩
    cm2 := by rw [h₃]; infer_instance
    cm3a := by rw [h₃]; infer_instance
    cm3b := by rw [h₂]; infer_instance
    cm3c := by rw [h₁]; infer_instance
    cm4a _ _ _ _ _ := by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance
    cm4b _ _ _ _ _ := by
      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
      infer_instance
    cm5a := by rw [h₁', h₂]; infer_instance
    cm5b := by rw [h₁, h₂']; infer_instance }
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
⊢ Eq (α := Subobject.{v_1, u_1} (X _⦋0⦌)) (objX X 0) ⊤

Tactic:
rfl

Premises used: AlgebraicTopology.NormalizedMooreComplex.objX, rfl
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
⊢ Eq (α := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) (objX X (n + 1))
    (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))

Tactic:
rfl

Premises used: AlgebraicTopology.NormalizedMooreComplex.objX, rfl
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
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)
⊢ 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))

Tactic:
refine factorThru _ (arrow _ ≫ X.δ (0 : Fin (n + 3))) ?_

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.factorThru, CategoryTheory.CategoryStruct.comp, CategoryTheory.SimplicialObject.δ, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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)

Tactic:
(finset_inf_factors _).mpr fun i _ => ?_

Premises used: Iff.mpr, CategoryTheory.Subobject.finset_inf_factors, AlgebraicTopology.NormalizedMooreComplex.objX
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
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)
⊢ 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 (finset_inf_factors _).mpr fun i _ => ?_

Premises used: Iff.mpr, CategoryTheory.Subobject.finset_inf_factors
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 (objX X (n + 1 + 1)) ⟶ X _⦋n⦌)
    ((arrow (objX X (n + 1 + 1)) ≫ X.δ 0) ≫ X.δ i.succ) 0
⊢ (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:
apply kernelSubobject_factors

Premises used: CategoryTheory.Limits.kernelSubobject_factors
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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⦌)
    ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ i.succ) 0
⊢ 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:
dsimp [objX]

Premises used: AlgebraicTopology.NormalizedMooreComplex.objX
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ 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.δ 0) ≫ X.δ i.succ) 0

Tactic:
rw [Category.assoc, ← Fin.castSucc_zero, ← X.δ_comp_δ (Fin.zero_le i.succ)]

Premises used: CategoryTheory.Category.assoc, Fin.succ, Fin.zero_le, Fin.castSucc_zero, CategoryTheory.SimplicialObject.δ_comp_δ
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
⊢ Membership.mem (γ := Finset (Fin (n + 1 + 1))) Finset.univ i.succ

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
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)
    0
w₄ w₅ :
  Eq.{v_1 + 1} (α :=
    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⦌)
    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

Tactic:
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Premises used: CategoryTheory.Category.assoc, Finset.univ, Fin.succ, CategoryTheory.Limits.comp_zero, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Subobject.finset_inf_arrow_factors
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
zero :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋HAdd.hAdd (α := ℕ) 0 1 + 1⦌)) underlying
        (objX X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying (objX X 0))
    (objD X (HAdd.hAdd (α := ℕ) 0 1) ≫ objD X 0) 0
succ :
  ∀ (n : ℕ),
    Eq (α :=
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying (objX X (n + 1 + 1 + 1)) ⟶
        Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying (objX X (n + 1)))
      (objD X (n + 1 + 1) ≫ objD X (n + 1)) 0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)) ⟶
      Functor.obj underlying (objX X n))
    (objD X (n + 1) ≫ objD X n) 0

Tactic:
rcases n with _ | n
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
zero :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋HAdd.hAdd (α := ℕ) 0 1 + 1⦌)) underlying
        (objX X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying (objX X 0))
    (objD X (HAdd.hAdd (α := ℕ) 0 1) ≫ objD X 0) 0

Tactic:
dsimp [objD]

Premises used: AlgebraicTopology.NormalizedMooreComplex.objD
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
succ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (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))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      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) ⋯)
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying (objX X (n + 1 + 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying (objX X (n + 1)))
    (objD X (n + 1 + 1) ≫ objD X (n + 1)) 0

Tactic:
dsimp [objD]

Premises used: AlgebraicTopology.NormalizedMooreComplex.objD
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
⊢ Membership.mem (γ := Finset (Fin 2)) Finset.univ 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
⊢ Membership.mem (γ := Finset (Fin (n + 3))) Finset.univ 0

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : Factors (X := HomologicalComplex.X (obj X) 0) (objX Y 0) (arrow (objX X 0) ≫ f.app (op ⦋0⦌))
succ :
  ∀ (n : ℕ),
    Factors (X := HomologicalComplex.X (obj X) (n + 1)) (objX Y (n + 1)) (arrow (objX X (n + 1)) ≫ f.app (op ⦋n + 1⦌))
⊢ (objX Y n).Factors ((objX X n).arrow ≫ f.app (op ⦋n⦌))

Tactic:
cases n
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
zero : Factors (X := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤) ⊤ (arrow ⊤ ≫ f.app (op ⦋0⦌))
⊢ Factors (X := HomologicalComplex.X (obj X) 0) (objX Y 0) (arrow (objX X 0) ≫ f.app (op ⦋0⦌))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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 : ℕ
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⦌))
⊢ Factors (X := HomologicalComplex.X (obj X) (n + 1)) (objX Y (n + 1)) (arrow (objX X (n + 1)) ≫ f.app (op ⦋n + 1⦌))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.MooreComplex
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
⊢ Factors (X := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤) ⊤ (arrow ⊤ ≫ f.app (op ⦋0⦌))

Tactic:
apply top_factors

Premises used: CategoryTheory.Subobject.top_factors