awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCone (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
H : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n : ℤ
⊢ Eq (α :=
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
    (Hom.f
        (CategoryStruct.comp (Y := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
          (Iso.hom (mapHomologicalComplexIso φ H)))
        n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
    (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n :
      X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
        X
          (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
            (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
          n)
have h : Eq (α :=
  H.obj (G.X n) ⟶
    X
      (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
        (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
      n)
  (CategoryStruct.comp (Y := H.obj ((mappingCone φ).X n)) (H.map (Hom.f (inr φ) n))
      (Iso.hom (mapHomologicalComplexXIso φ H n)) :
    H.obj (G.X n) ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
  (Hom.f (inr (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)) n :
    X (Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) G) n ⟶
      X
        (mappingCone (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
          (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
        n)
Tactic: dsimp [mapHomologicalComplexIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : CochainComplex.plus C K
⊢ CochainComplex.plus C (cylinder K)
have obtain : ∀ (n : ℤ) (hn : K.IsStrictlyGE n), CochainComplex.plus C (cylinder K)
Tactic: obtain ⟨n, hn⟩ := hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ CochainComplex.plus C (cylinder K)
have refine : IsStrictlyGE (cylinder K) (n - 1)
Tactic: refine ⟨n - 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ IsStrictlyGE (cylinder K) (n - 1)
have rw : ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((cylinder K).X i)
Tactic: rw [CochainComplex.isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((cylinder K).X i)
have dsimp : IsZero.{v_1, u_1} (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) i)
Tactic: dsimp [cylinder]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) i)
have refine_1 : IsZero.{v_1, u_1} ((K ⊞ K).X i)
Tactic: refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
refine_1 : IsZero.{v_1, u_1} ((K ⊞ K).X i)
⊢ IsZero.{v_1, u_1} (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) i)
have refine_2 : ∀ (j : ℤ) (hj : (ComplexShape.up ℤ).Rel i j), IsZero.{v_1, u_1} (K.X j)
Tactic: refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((K ⊞ K).X i)
have refine_1 : IsZero.{v_1, u_1}
  (biprod.{v_1, u_1} (Functor.obj (eval C (ComplexShape.up ℤ) i) K) (Functor.obj (eval C (ComplexShape.up ℤ) i) K))
Tactic: refine IsZero.of_iso ?_ ((HomologicalComplex.eval C (.up ℤ) i).mapBiprod _ _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : CochainComplex.plus C K
⊢ CochainComplex.plus C (pathObject K)
have obtain : ∀ (n : ℤ) (hn : K.IsStrictlyGE n), CochainComplex.plus C (pathObject K)
Tactic: obtain ⟨n, hn⟩ := hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ CochainComplex.plus C (pathObject K)
have refine : IsStrictlyGE (pathObject K) (n - 1)
Tactic: refine ⟨n - 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ IsStrictlyGE (pathObject K) (n - 1)
have rw : ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((pathObject K).X i)
Tactic: rw [CochainComplex.isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((pathObject K).X i)
have refine : ∀ (j : ℤ) (hj : (ComplexShape.up ℤ).Rel j i), IsZero.{v_1, u_1} (K.X j)
Tactic: refine pathObject.isZero_X _ _ (K.isZero_of_isStrictlyGE n i)
    (fun j hj ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
⊢ (mappingCone f).IsStrictlyGE n
have rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((mappingCone f).X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((mappingCone f).X i)
have hi₁ : i < n
Tactic: simp at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
i : ℤ
hi : i < n
⊢ IsZero.{v_1, u_1} ((mappingCone f).X i)
have simp : IsZero.{v_1, u_1} (K.X (i + 1)) ∧ IsZero.{v_1, u_1} (L.X i)
Tactic: simp only [mappingCone.isZero_X_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) ↔ CochainComplex.plus C K
have refine : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) → CochainComplex.plus C K
Tactic: refine ⟨?_, fun h ↦ ⟨_, h⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) → CochainComplex.plus C K
have simp : (∃ (X : CochainComplex.{v_1, u_1, 0} C ℤ),
    CochainComplex.plus C X ∧
      Functor.obj (quotient C (ComplexShape.up ℤ)) X = Functor.obj (quotient C (ComplexShape.up ℤ)) K) →
  CochainComplex.plus C K
Tactic: simp only [plus, ObjectProperty.strictMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
h : CochainComplex.plus C L
hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) K
⊢ CochainComplex.plus C K
have obtain : ∀ (hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) L),
  CochainComplex.plus C L
Tactic: obtain rfl : L = K := congr_arg Quotient.as hL
Cleared hypotheses: K, hL
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
⊢ plus.{v_1, u_1} C (Functor.obj (quotient C (ComplexShape.up ℤ)) 0)
have simp : CochainComplex.plus.{v_1, u_1} C 0
Tactic: simp only [plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : plus C K
⊢ ObjectProperty.shift (plus C) n K
have obtain : ∀ (K : CochainComplex.{v_1, u_1, 0} C ℤ) (hK : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K)),
  ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
Tactic: obtain ⟨K : CochainComplex _ _, rfl⟩ := K.quotient_obj_surjective
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
⊢ ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
have hK₁ : CochainComplex.plus C K
Tactic: simp only [plus_quotient_obj_iff] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : CochainComplex.plus C K
⊢ ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
have obtain : ∀ (q : ℤ), K.IsStrictlyGE q → ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
Tactic: obtain ⟨q, _⟩ := hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
q : ℤ
h : K.IsStrictlyGE q
⊢ ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
have rw : CochainComplex.plus C (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) K)
Tactic: rw [ObjectProperty.prop_shift_iff, shift_quotient_obj,
          plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
⊢ CochainComplex.plus C (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)))
have rwa : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))))
Tactic: rwa [← plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
⊢ ObjectProperty.isoClosure (plus C) T.obj₃
have obtain : ∀ (n₁ : ℤ),
  CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁ →
    ObjectProperty.isoClosure (plus C) T.obj₃
Tactic: obtain ⟨n₁, _⟩ : (CochainComplex.plus C) T.obj₁.as := by
      rwa [← plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
⊢ CochainComplex.plus C (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ)))
have rwa : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))))
Tactic: rwa [← plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
⊢ ObjectProperty.isoClosure (plus C) T.obj₃
have obtain : ∀ (n₂ : ℤ),
  CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂ →
    ObjectProperty.isoClosure (plus C) T.obj₃
Tactic: obtain ⟨n₂, _⟩ : (CochainComplex.plus C) T.obj₂.as := by
      rwa [← plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
n₂ : ℤ
h_1 : CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂
⊢ ObjectProperty.isoClosure (plus C) T.obj₃
have obtain : ∀ (f : T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ T.obj₂.as (r := homotopic C (ComplexShape.up ℤ)))
  (hf : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f = T.mor₁),
  ObjectProperty.isoClosure (plus C) T.obj₃
Tactic: obtain ⟨f : T.obj₁.as ⟶ T.obj₂.as, hf⟩ := (quotient _ _).map_surjective T.mor₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
n₂ : ℤ
h_1 : CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂
f : T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))
hf : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f = T.mor₁
⊢ ObjectProperty.isoClosure (plus C) T.obj₃
have refine_1 : plus C (Functor.obj Triangle.π₃ (CochainComplex.mappingCone.triangleh f))
Tactic: refine ⟨_, ?_,
      ⟨Triangle.π₃.mapIso (isoTriangleOfIso₁₂ T _ hT (mappingCone_triangleh_distinguished f)
        (Iso.refl _) (Iso.refl _) ?_)⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
n₂ : ℤ
h_1 : CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂
f : T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))
hf : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f = T.mor₁
refine_1 : plus C (Functor.obj Triangle.π₃ (CochainComplex.mappingCone.triangleh f))
⊢ ObjectProperty.isoClosure (plus C) T.obj₃
have refine_2 : T.mor₁ ≫ Iso.hom (Iso.refl T.obj₂) = Iso.hom (Iso.refl T.obj₁) ≫ (CochainComplex.mappingCone.triangleh f).mor₁
Tactic: refine ⟨_, ?_,
      ⟨Triangle.π₃.mapIso (isoTriangleOfIso₁₂ T _ hT (mappingCone_triangleh_distinguished f)
        (Iso.refl _) (Iso.refl _) ?_)⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
n₂ : ℤ
h_1 : CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂
f : T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))
hf : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f = T.mor₁
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f))
have refine_1 : CochainComplex.plus C (CochainComplex.mappingCone f)
Tactic: simp only [plus_quotient_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
a : ℤ
⊢ Eq (α := MorphismProperty (Plus.{v_2, u_2} A))
    (MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a)) (quasiIso A)
have h : ∀ ⦃X Y : Plus.{v_2, u_2} A⦄ (f : X ⟶ Y),
  MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔ quasiIso A f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Plus (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
a : ℤ
X Y : Plus.{v_2, u_2} A
f : X ⟶ Y
⊢ MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔ quasiIso A f
have h : MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔
  HomotopyCategory.quasiIso A (ComplexShape.up ℤ) (X :=
    Functor.obj (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) (X.obj (P := plus A)))
    (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) f.hom)
Tactic: simp only [quasiIso_iff, ← MorphismProperty.IsCompatibleWithShift.iff
      (HomotopyCategory.quasiIso _ _) f.hom a]