awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : (j : J) → ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)
⊢ ∃ (n : ℤ), ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n

Tactic:
exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
obtain :
  ∀ (n : ℤ) (hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n),
    CochainComplex.plus C K
⊢ CochainComplex.plus C K

Tactic:
obtain ⟨n, hn⟩ : ∃ (n : ℤ), ∀ (j : J), (p.diag.obj j).IsStrictlyGE n := by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ CochainComplex.plus C K

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
refine : K.IsStrictlyGE n
⊢ CochainComplex.plus C K

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE n

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
rw : Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0

Tactic:
(isLimitOfPreserves (HomologicalComplex.eval _ _ i) p.isLimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_tgt _ _)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.CategoryStruct.id, HomologicalComplex.eval, Int, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitPresentation.isLimit, CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.CategoryStruct.comp, HomologicalComplex.X, CategoryTheory.Functor.mapCone, OfNat.ofNat, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.LimitPresentation.π, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasLimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.LimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toLimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0

Tactic:
exact (isLimitOfPreserves (HomologicalComplex.eval _ _ i) p.isLimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_tgt _ _)

Premises used: CategoryTheory.Limits.Cone.π, HomologicalComplex.eval, Int, CategoryTheory.ObjectProperty.LimitOfShape.toLimitPresentation, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitPresentation.isLimit, CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.LimitPresentation.diag, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.LimitPresentation.π, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
choose :
  ∀ (n : (j : J) → ℤ)
    (hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)),
    ∃ (n : ℤ), ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ ∃ (n : ℤ), ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n

Tactic:
choose n hn using p.prop_diag_obj

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : (j : J) → ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)
⊢ 0 ∈ Finset.image n ⊤ ∪ {0}

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : (j : J) → ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)
j : J
⊢ n j ∈ Finset.image n ⊤ ∪ {0}

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : (j : J) → ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE (n j)
⊢ ∃ (n : ℤ), ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n

Tactic:
exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
obtain :
  ∀ (n : ℤ) (hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n),
    CochainComplex.plus C K
⊢ CochainComplex.plus C K

Tactic:
obtain ⟨n, hn⟩ : ∃ (n : ℤ), ∀ (j : J), (p.diag.obj j).IsStrictlyGE n := by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
⊢ CochainComplex.plus C K

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
refine : K.IsStrictlyGE n
⊢ CochainComplex.plus C K

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE n

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
rw : Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0

Tactic:
(isColimitOfPreserves (HomologicalComplex.eval _ _ i) p.isColimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_src _ _)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.CategoryStruct.id, HomologicalComplex.eval, CategoryTheory.Limits.Cocone.mk, Int, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.Cocone.ι, CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.CategoryStruct.comp, HomologicalComplex.X, OfNat.ofNat, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Limits.isColimitOfPreserves, ComplexShape.up, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
J : Type u_2
inst_2 : SmallCategory J
inst_3 : FinCategory J
inst_4 : HasColimitsOfShape.{u_2, u_2, v_1, u_1} J C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p : ObjectProperty.ColimitOfShape (CochainComplex.plus C) J K
n : ℤ
hn : ∀ (j : J), (p.toColimitPresentation (P := CochainComplex.plus C).diag.obj j).IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) 0

Tactic:
exact (isColimitOfPreserves (HomologicalComplex.eval _ _ i) p.isColimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_src _ _)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.IsColimit.hom_ext, HomologicalComplex.eval, CategoryTheory.Limits.Cocone.mk, Int, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.Cocone.ι, CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Limits.isColimitOfPreserves, ComplexShape.up, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteLimits.{v_1, u_1} C
J : Type
x : SmallCategory J
x_1 : FinCategory J
⊢ HasLimitsOfShape J (Plus.{v_1, u_1} C)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteColimits.{v_1, u_1} C
J : Type
x : SmallCategory J
x_1 : FinCategory J
⊢ HasColimitsOfShape J (Plus.{v_1, u_1} C)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasLimitsOfShape.{0, 0, v_1, u_1} WalkingCospan C
X Y : Plus.{v_1, u_1} C
f : X ⟶ Y
h : Mono f.hom
⊢ Mono (X := Functor.obj (ι C) X) (CategoryTheory.Functor.map (ι C) f)

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasLimitsOfShape.{0, 0, v_1, u_1} WalkingCospan C
X Y : Plus.{v_1, u_1} C
f : X ⟶ Y
inst_3 rwa rwa₁ rwa₂ rwa₃ : Mono f
⊢ Mono f.hom

Tactic:
rwa [← mono_iff]

Premises used: CochainComplex.Plus.mono_iff
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
⊢ MorphismProperty.HasTwoOutOfThreeProperty (C := Plus.{v_1, u_1} C)
    (MorphismProperty.inverseImage (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (ι C))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
⊢ MorphismProperty.IsStableUnderRetracts (C := Plus.{v_1, u_1} C)
    (MorphismProperty.inverseImage (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (ι C))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
h : CochainComplex.plus C K
k : ℤ
hk : K.IsStrictlyGE k
⊢ n + (k - n) = k

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
obtain :
  ∀ (i : ℤ) (hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i),
    CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)
⊢ CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)

Tactic:
obtain ⟨i, hi⟩ := K.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
i : ℤ
hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i
⊢ CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)

Tactic:
⟨i, ?_⟩

Premises used: Exists.intro, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
i : ℤ
hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i
refine : CochainComplex.IsStrictlyGE (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K) i
⊢ CochainComplex.plus D (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K)

Tactic:
refine ⟨i, ?_⟩
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
i : ℤ
hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i
dsimp :
  CochainComplex.IsStrictlyGE (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) (K.obj (P := CochainComplex.plus C))) i
⊢ CochainComplex.IsStrictlyGE (obj (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)) K) i

Tactic:
dsimp [CochainComplex.Plus.ι]

Premises used: CochainComplex.Plus.ι
-- Module: Mathlib.Algebra.Homology.CochainComplexPlus
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
inst_4 : F.PreservesZeroMorphisms
K : CochainComplex.Plus.{v_1, u_1} C
i : ℤ
hi : K.obj (P := CochainComplex.plus C).IsStrictlyGE i
⊢ CochainComplex.IsStrictlyGE (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) (K.obj (P := CochainComplex.plus C))) i

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) (biprod.desc inl inr) = 0

Tactic:
simp [sq.w]

Premises used: CategoryTheory.CommSq.w
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
rw : HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
⊢ f ≫ biprod.inl ≫ s.π = g ≫ biprod.inr ≫ s.π

Tactic:
rw [← sub_eq_zero, ← assoc, ← assoc, ← Preadditive.sub_comp]

Premises used: CategoryTheory.Category.assoc, sub_eq_zero, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
⊢ biprod.lift f (-g) ≫ s.π = 0 ≫ s.π

Tactic:
s.condition

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
h₁ : HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) = biprod.lift f (-g)
h₂ : Eq (α := X₁ ⟶ s.pt) 0 (0 ≫ s.π)
⊢ HSub.hSub (α := X₁ ⟶ biprod.{v_1, u_1} X₂ X₃) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0

Tactic:
convert! s.condition

Premises used: CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.Algebra.Homology.CommSq
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
inst_2 : HasBinaryBiproduct.{v_1, u_1} X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0
dsimp : biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) sq.cokernelCofork)
      (Cofork.π sq.cokernelCofork)
      ((fun (s : Cofork (Y := biprod.{v_1, u_1} X₂ X₃) (biprod.lift f (-g)) 0) ↦
          PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯)
        s) =
    s.π

Tactic:
dsimp