mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (commShiftIso G (m + n)).hom.app ((Φ a'').obj X) ≫
      (shiftFunctor E (m + n)).map ((hΦ a'').hom.app X) ≫ (F.shiftIso (m + n) a a'' ⋯).hom.app X ≫ (hΦ a).inv.app X =
    G.map ((shiftFunctorAdd D m n).hom.app ((Φ a'').obj X)) ≫
      G.map (𝟙 ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((Φ a'').obj X)))) ≫
        (commShiftIso G n).hom.app ((shiftFunctor D m).obj ((Φ a'').obj X)) ≫
          ((shiftFunctor E n).map ((commShiftIso G m).hom.app ((Φ a'').obj X)) ≫
              (shiftFunctor E n).map ((shiftFunctor E m).map ((hΦ a'').hom.app X)) ≫
                (shiftFunctor E n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                  (shiftFunctor E n).map ((hΦ a').inv.app X)) ≫
            (shiftFunctor E n).map ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X

Tactic:
F.shiftIso_add n m a a' a'' ha' ha''

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (commShiftIso G (m + n)).hom.app ((Φ a'').obj X) ≫
      (shiftFunctor E (m + n)).map ((hΦ a'').hom.app X) ≫
        ((F.functor a'').isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
                  ((F.functor a'').associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
                    isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor E n) ≪≫ F.shiftIso n a a' ha').hom.app
            X ≫
          (hΦ a).inv.app X =
    G.map ((shiftFunctorAdd D m n).hom.app ((Φ a'').obj X)) ≫
      G.map (𝟙 ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((Φ a'').obj X)))) ≫
        (commShiftIso G n).hom.app ((shiftFunctor D m).obj ((Φ a'').obj X)) ≫
          ((shiftFunctor E n).map ((commShiftIso G m).hom.app ((Φ a'').obj X)) ≫
              (shiftFunctor E n).map ((shiftFunctor E m).map ((hΦ a'').hom.app X)) ≫
                (shiftFunctor E n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                  (shiftFunctor E n).map ((hΦ a').inv.app X)) ≫
            (shiftFunctor E n).map ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : ¬c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
⊢ (F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) ⋯) ≫
      mapBifunctor.d₂ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂.π c₃ c₂₃ (i₂, i₃)) j' =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' + d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
· rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁, comp_zero]
    trans 0 + 0
    · simp only [add_zero]
    · congr 1
      · rw [d₂_eq_zero]
        intro h₂
        apply h₁
        simpa only [← ComplexShape.next_π₁ c₃ c₂₃ h₂ i₃]
          using ComplexShape.rel_π₁ c₃ c₂₃ h₂ i₃
      · rw [d₃_eq_zero]
        intro h₂
        apply h₁
        simpa only [i₂₃, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₂]
          using ComplexShape.rel_π₂ c₂ c₂₃ i₂ h₂

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ T.mor₁ ≫ (Iso.refl T.obj₂).hom = (Iso.refl T.obj₁).hom ≫ (CochainComplex.mappingCone.triangleh f).mor₁

Tactic:
· simp [hf]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
this :
  Triangle.mk o.m₃.op o.m₁.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          ((((shiftFunctor C 1).map w₂₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂) ≫ v₁₂)) ∈
    Pretriangulated.distinguishedTriangles
⊢ w₂₃ ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂ =
    (opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
      (shiftFunctor Cᵒᵖ 1).map ((shiftFunctor C 1).map w₂₃.unop).op ≫
        (shiftFunctor Cᵒᵖ 1).map ((opShiftFunctorEquivalence C 1).unitIso.inv.app X₂) ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂

Tactic:
← opShiftFunctorEquivalence_counitIso_hom_app_shift,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
this :
  Triangle.mk o.m₃.op o.m₁.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          ((((shiftFunctor C 1).map w₂₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂) ≫ v₁₂)) ∈
    Pretriangulated.distinguishedTriangles
⊢ w₂₃ ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂ =
    (opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
      (shiftFunctor Cᵒᵖ 1).map ((shiftFunctor C 1).map w₂₃.unop).op ≫
        (opShiftFunctorEquivalence C 1).counitIso.hom.app ((shiftFunctor Cᵒᵖ 1).obj X₂) ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : Plus C
f : K ⟶ L
M : Plus C
g : L ⟶ M
h : M ⟶ (shiftFunctor (Plus C) 1).obj K
mem : Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
this :
  (HomotopyCategory.subcategoryAcyclic C).trW ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).mor₁ ↔
    HomotopyCategory.subcategoryAcyclic C ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).obj₃
⊢ quasiIso C f ↔ (subcategoryAcyclic C).trW f

Tactic:
rw [← HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic] at this

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : Plus C
f : K ⟶ L
M : Plus C
g : L ⟶ M
h : M ⟶ (shiftFunctor (Plus C) 1).obj K
mem : Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
this :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).mor₁ ↔
    HomotopyCategory.subcategoryAcyclic C ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).obj₃
⊢ quasiIso C f ↔ (subcategoryAcyclic C).trW f
Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
a✝ : Injective I
A B : C
⊢ ∀ (g : A ⟶ B), MorphismProperty.monomorphisms C g → HasLiftingProperty g 0

Tactic:
i

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
a✝ : Injective I
A B : C
i : A ⟶ B
⊢ MorphismProperty.monomorphisms C i → HasLiftingProperty i 0
Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
⊢ ∀ (f_1 : A ⟶ B) [Mono f_1], ∃ h, f_1 ≫ h = f

Tactic:
i

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
⊢ ∀ [Mono i], ∃ h, i ≫ h = f
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case h₂
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₂ = TriangleMorphism.hom₂ 0

pp: case h₃
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0

Tactic:
· simp [hf]

Goal state after:
case h₃
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case pos
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
inst✝ : t.IsLE X b
h : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b

pp: case neg
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
inst✝ : t.IsLE X b
h : ¬a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
· exact t.isLE_truncLT_obj ..

Goal state after:
case neg
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
inst✝ : t.IsLE X b
h : ¬a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (toHoCatLocalizerMorphism C).IsLocalizedEquivalence

Tactic:
apply (factorsThroughLocalization C).isLocalizedEquivalence

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ weakEquivalences (FibrantObject C) = (weakEquivalences (HoCat C)).inverseImage (Quotient.functor (homRel C))
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
q : ℤ
hq : q ≤ n
⊢ QuasiIsoAt (ι f n) q

Tactic:
by
  obtain hq | rfl := hq.lt_or_eq'
  · have := quasiIsoAt_π f n q hq
    rw [← quasiIsoAt_iff_comp_right _ (π f n), mappingCocone.lift_fst]
    exact hf q hq
  · have := mono_homologyMap_π f n n (by lia)
    have : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n) := by
      dsimp; infer_instance
    have h₁ := (exact_homologyShortComplex f n).fIsKernel
    have h₂ := (CochainComplex.homologyMap_exact₂_of_distTriang _
      (DerivedCategory.mappingCocone_triangle_distinguished (α f n)) n).fIsKernel
    have : homologyMap (ι f n) n = (IsLimit.conePointUniqueUpToIso h₁ h₂).hom := by
      simp [← cancel_mono (homologyMap (π f n) n),
        dsimp% IsLimit.conePointUniqueUpToIso_hom_comp h₁ h₂ .zero,
        ← homologyMap_comp, mappingCocone.lift_fst]
    rw [quasiIsoAt_iff_isIso_homologyMap, this]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this✝ : Nonempty (w.CostructuredArrowDownwards y)
this : ∀ (X : w.CostructuredArrowDownwards y), ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)
⊢ IsConnected
    ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y)

Tactic:
refine zigzag_isConnected (fun X X' => ?_)
    obtain ⟨Y, hX⟩ := this X
    obtain ⟨Y', hX'⟩ := this X'
    exact hX.trans ((zigzag_obj_of_zigzag _ (isPreconnected_zigzag Y Y')).trans hX'.symm)

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : K.IsStrictlyGE n₁
this : K.IsStrictlyGE (n₀ + 1)
⊢ ∃ L i, ∃ (_ : Mono i) (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀

Tactic:
obtain ⟨L, hL, i, p, hi, hi', hp, _⟩ := cm5a (0 : K ⟶ 0) n₀

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : K.IsStrictlyGE n₁
this : K.IsStrictlyGE (n₀ + 1)
L : CochainComplex C ℤ
hL : L.IsStrictlyGE n₀
i : K ⟶ L
p : L ⟶ 0
hi : Mono i
hi' : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
right✝ : i ≫ p = 0
⊢ ∃ L i, ∃ (_ : Mono i) (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} C₁
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
⊢ IsIso (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)

Tactic:
by
  have : F.HasPointwiseRightDerivedFunctor W₂ := by
    rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]
    infer_instance
  dsimp only [rightDerivedFunctorComparison]
  rw [← isRightDerivedFunctor_iff_isIso_rightDerivedDesc,
    isRightDerivedFunctor_iff_isLeftKanExtension]
  exact ((F₂.isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor α₂ W₂).compTwoSquare
    ((Φ.catCommSq L₁ L₂).iso).hom).isLeftKanExtension

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: case zero
C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y X : C
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y 0)

Tactic:
simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: case zero
C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X Y : C
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y 0)

Tactic:
simpa [Ext.mapExactFunctor₀] using ⟨Faithful.map_injective, Full.map_surjective⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_2
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
K L : CochainComplex.Plus C
f : K ⟶ L
hf : (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) f
⊢ CochainComplex.Plus.quasiIso C f

Tactic:
exact homotopyEquivalences_le_quasiIso _ _ _ hf

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy (double (𝟙 X) ⋯)

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy ((single C c j).obj X)

Tactic:
· exact evalCompCoyonedaCorepresentableByDoubleId _
      (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ (eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy ((single C c j).obj X)
Module: Mathlib.Algebra.Homology.ExactSequenceFour

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
⊢ Mono (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
have := hS'.hasZeroObject
  have := hS'.hasHomology
  let h := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
  have := h.exact_iff_mono_g'.1 hS'
  have fac : hS.cokerToKer' k hk cc kf hcc hkf ≫ kf.ι = h.g' := by
    rw [← cancel_epi h.p, h.p_g', ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p,
      cokerToKer'_fac]
  exact mono_of_mono_fac fac

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = (F.map P.decompId_i ≫ F.map P.decompId_p) ≫ φ.app P

Tactic:
← F.map_comp

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P

Tactic:
conv_lhs => rw [← id_comp (φ.app P), ← F.map_id]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ (f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      { X₁ := Q.complex.X (0 + 2), X₂ := Q.complex.X (0 + 1), X₃ := Q.complex.X 0, f := Q.complex.d (0 + 2) (0 + 1),
          g := Q.complex.d (0 + 1) 0, zero := ⋯ }.g =
    0

Tactic:
rw [Preadditive.sub_comp, assoc, HomologicalComplex.Hom.comm,
              liftHomotopyZeroZero_comp, sub_self]

Goal state after: