awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : HasZeroObject.{v, u} V
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (𝟙 (Functor.obj (quotient V c) 0)) 0
⊢ IsZero (C := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0)
have rw₁ : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
  (CategoryTheory.Functor.map (quotient V c) (𝟙 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : HasZeroObject.{v, u} V
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (𝟙 (Functor.obj (quotient V c) 0)) 0
rw₁ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 0)) 0
⊢ IsZero (C := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0)
have rw₂ : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
  (CategoryTheory.Functor.map (quotient V c) 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : HasZeroObject.{v, u} V
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (𝟙 (Functor.obj (quotient V c) 0)) 0
rw₁ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 0)) 0
rw₂ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0))
    (CategoryTheory.Functor.map (quotient V c) 0) 0
⊢ IsZero (C := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0)
have rw₃ : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Functor.obj (quotient V c) 0) (Functor.obj (quotient V c) 0)) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : C ⟶ D
⊢ Homotopy (Quot.out (r := HomRel.CompClosure (homotopic V c)) (CategoryTheory.Functor.map (quotient V c) f)) f
have w : Eq (α :=
  Functor.obj (quotient V c) ((Functor.obj (quotient V c) C).as (r := homotopic V c)) ⟶
    Functor.obj (quotient V c) ((Functor.obj (quotient V c) D).as (r := homotopic V c)))
  (CategoryTheory.Functor.map (quotient V c)
    (Quot.out (r := HomRel.CompClosure (homotopic V c)) (CategoryTheory.Functor.map (quotient V c) f)))
  (CategoryTheory.Functor.map (quotient V c) f)
Tactic: apply homotopyOfEq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
⊢ CategoryTheory.Functor.map (quotient V c) f.hom ≫ CategoryTheory.Functor.map (quotient V c) f.inv =
    𝟙 (Functor.obj (quotient V c) C)
have rw : Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
  (CategoryTheory.Functor.map (quotient V c) (f.hom ≫ f.inv)) (CategoryTheory.Functor.map (quotient V c) (𝟙 C))
Tactic: rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f : HomotopyEquiv C D
⊢ CategoryTheory.Functor.map (quotient V c) f.inv ≫ CategoryTheory.Functor.map (quotient V c) f.hom =
    𝟙 (Functor.obj (quotient V c) D)
have rw : Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
  (CategoryTheory.Functor.map (quotient V c) (f.inv ≫ f.hom)) (CategoryTheory.Functor.map (quotient V c) (𝟙 D))
Tactic: rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 C))
have rw : i.hom ≫ i.inv = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
Tactic: rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
rw : i.hom ≫ i.inv = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 C))
have rw₁ : 𝟙 (Functor.obj (quotient V c) C) = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
Tactic: rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
rw : i.hom ≫ i.inv = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
rw₁ : 𝟙 (Functor.obj (quotient V c) C) = CategoryTheory.Functor.map (quotient V c) (𝟙 C)
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 C))
have rw₂ : 𝟙 (Functor.obj (quotient V c) C) = 𝟙 (Functor.obj (quotient V c) C)
Tactic: rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
⊢ Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 D))
have rw : i.inv ≫ i.hom = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
Tactic: rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
rw : i.inv ≫ i.hom = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
⊢ Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 D))
have rw₁ : 𝟙 (Functor.obj (quotient V c) D) = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
Tactic: rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
i : Functor.obj (quotient V c) C ≅ Functor.obj (quotient V c) D
rw : i.inv ≫ i.hom = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
rw₁ : 𝟙 (Functor.obj (quotient V c) D) = CategoryTheory.Functor.map (quotient V c) (𝟙 D)
⊢ Eq (α := Functor.obj (quotient V c) D ⟶ Functor.obj (quotient V c) D)
    (CategoryTheory.Functor.map (quotient V c)
      (Quot.out (r := HomRel.CompClosure (homotopic V c)) i.inv ≫
        Quot.out (r := HomRel.CompClosure (homotopic V c)) i.hom))
    (CategoryTheory.Functor.map (quotient V c) (𝟙 D))
have rw₂ : 𝟙 (Functor.obj (quotient V c) D) = 𝟙 (Functor.obj (quotient V c) D)
Tactic: rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
⊢ Eq (α := MorphismProperty (HomologicalComplex.{v, u, u_2} V c))
    (MorphismProperty.inverseImage (MorphismProperty.isomorphisms (HomotopyCategory.{v, u, u_2} V c)) (quotient V c))
    (homotopyEquivalences V c)
have h : ∀ ⦃K L : HomologicalComplex.{v, u, u_2} V c⦄ (f : K ⟶ L),
  MorphismProperty.inverseImage (MorphismProperty.isomorphisms (HomotopyCategory.{v, u, u_2} V c)) (quotient V c) f ↔
    homotopyEquivalences V c f
Tactic: ext K L f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
⊢ IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f) ↔ homotopyEquivalences V c f
have h : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f) → homotopyEquivalences V c f
Tactic: refine ⟨fun _ ↦ ?_, fun hf ↦ quotient_inverts_homotopyEquivalences _ _ _ hf⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
h : IsIso (X := Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) f)
⊢ homotopyEquivalences V c f
have h : ∀ (g : L ⟶ K)
  (hg :
    Eq (α := Functor.obj (quotient V c) L ⟶ Functor.obj (quotient V c) K) (CategoryTheory.Functor.map (quotient V c) g)
      (inv (CategoryTheory.Functor.map (quotient V c) f))),
  homotopyEquivalences V c f
Tactic: obtain ⟨g, hg⟩ := (quotient V c).map_surjective (inv ((quotient _ _).map f))
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
⊢ IsZero (Functor.obj (quotient V c) C) ↔ Nonempty (Homotopy (𝟙 C) 0)
have rw : Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 ↔
  Nonempty (Homotopy (𝟙 C) 0)
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 ↔
    Nonempty (Homotopy (𝟙 C) 0)
have mp : Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 →
  Nonempty (Homotopy (𝟙 C) 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (goal)
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
mp :
  Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 →
    Nonempty (Homotopy (𝟙 C) 0)
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 ↔
    Nonempty (Homotopy (𝟙 C) 0)
have mpr : Nonempty (Homotopy (𝟙 C) 0) →
  Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : CategoryWithHomology.{v, u} V
i : ι
⊢ Functor.Additive (C := HomotopyCategory.{v, u, u_2} V c) (homologyFunctor V c i)
have this : Functor.Additive (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c ⋙ homologyFunctor V c i)
Tactic: have := Functor.additive_of_iso (homologyFunctorFactors V c i).symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
inst_4 : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
⊢ X φ i = biprod.{v_1, u_1} (F.X j) (G.X i)
have obtain : ∀ (hij : c.Rel i (c.next i)) [inst_5 : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)],
  X φ i = biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, hij, inst_4
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
⊢ IsZero.{v_1, u_1} (X φ i)
have pos : ∀ (h : c.Rel i (c.next i)), IsZero.{v_1, u_1} (X φ i)
Tactic: by_cases h : c.Rel i (c.next i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
pos : ∀ (h : c.Rel i (c.next i)), IsZero.{v_1, u_1} (X φ i)
⊢ IsZero.{v_1, u_1} (X φ i)
have neg : ∀ (h : ¬c.Rel i (c.next i)), IsZero.{v_1, u_1} (X φ i)
Tactic: by_cases h : c.Rel i (c.next i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
⊢ IsZero.{v_1, u_1} (X φ i)
have this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
Tactic: haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ IsZero.{v_1, u_1} (X φ i)
have pos : IsZero.{v_1, u_1} (biprod.{v_1, u_1} (F.X (c.next i)) (G.X i))
Tactic: refine IsZero.of_iso ?_ (XIsoBiprod φ _ _ h)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ IsZero.{v_1, u_1} (biprod.{v_1, u_1} (F.X (c.next i)) (G.X i))
have pos : IsZero.{v_1, u_1} (F.X (c.next i)) ∧ IsZero.{v_1, u_1} (G.X i)
Tactic: simp only [biprod_isZero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (sndX φ i) = 𝟙 (G.X i)
have dsimp : Eq.{v_1 + 1} (α := G.X i ⟶ G.X i)
  (CategoryStruct.comp (Y := X φ i)
    (if hi : c.Rel i (c.next i) then
      CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
        (Iso.inv (XIsoBiprod φ i (c.next i) hi))
    else Iso.inv (XIso φ i hi))
    (if hi : c.Rel i (c.next i) then
      CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
        biprod.snd
    else Iso.hom (XIso φ i hi)))
  (𝟙 (G.X i))
Tactic: dsimp [sndX, inrX]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
⊢ Eq.{v_1 + 1} (α := G.X i ⟶ G.X i)
    (CategoryStruct.comp (Y := X φ i)
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi))
      else Iso.inv (XIso φ i hi))
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd
      else Iso.hom (XIso φ i hi)))
    (𝟙 (G.X i))
have pos : ∀ (hi : c.Rel i (c.next i)),
  CategoryStruct.comp (Y := X φ i)
      (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
        (Iso.inv (XIsoBiprod φ i (c.next i) hi)))
      (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
        biprod.snd) =
    𝟙 (G.X i)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
pos :
  ∀ (hi : c.Rel i (c.next i)),
    CategoryStruct.comp (Y := X φ i)
        (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi)))
        (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd) =
      𝟙 (G.X i)
⊢ Eq.{v_1 + 1} (α := G.X i ⟶ G.X i)
    (CategoryStruct.comp (Y := X φ i)
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi))
      else Iso.inv (XIso φ i hi))
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd
      else Iso.hom (XIso φ i hi)))
    (𝟙 (G.X i))
have neg : ∀ (hi : ¬c.Rel i (c.next i)),
  CategoryStruct.comp (Y := X φ i) (Iso.inv (XIso φ i hi)) (Iso.hom (XIso φ i hi)) = 𝟙 (G.X i)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ sndX φ i ≫ inrX φ i = 𝟙 (X φ i)
have dsimp : Eq.{v_1 + 1} (α := X φ i ⟶ X φ i)
  (CategoryStruct.comp (Y := G.X i)
    (if hi : c.Rel i (c.next i) then
      CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
        biprod.snd
    else Iso.hom (XIso φ i hi))
    (if hi : c.Rel i (c.next i) then
      CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
        (Iso.inv (XIsoBiprod φ i (c.next i) hi))
    else Iso.inv (XIso φ i hi)))
  (𝟙 (X φ i))
Tactic: dsimp [sndX, inrX]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ i j hij) (sndX φ j) = 0
have obtain : ∀ (hij : c.Rel j (c.next j)), CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hij) (sndX φ j) = 0
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (fstX φ i j hij) = 0
have obtain : ∀ (hij : c.Rel i (c.next i)), CategoryStruct.comp (Y := X φ i) (inrX φ i) (fstX φ i (c.next i) hij) = 0
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g
have this : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
Tactic: haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij