mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ cyclesMap (S.f ≫ S.g) i = 0

Tactic:
S.zero,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ cyclesMap 0 i = 0
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ HomologicalComplex.homologyMap (S.f ≫ S.g) i = 0

Tactic:
S.zero,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ HomologicalComplex.homologyMap 0 i = 0
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this : Epi S.g
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

Tactic:
have : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i) :=
      fun K => ShortComplex.isIso_homologyι (K.sc i) (K.shape _ _ h)

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: case e_a
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
⊢ F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
            (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
              (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X)) =
    F'.map ((shiftFunctor D b).map ((commShiftIso L a).hom.app X)) ≫
      (commShiftOfLocalization.iso L W F F' b).hom.app ((shiftFunctor D a).obj (L.obj X)) ≫
        (shiftFunctor E b).map (F'.map ((commShiftIso L a).inv.app X)) ≫
          (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
                (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))

Tactic:
conv_rhs =>
      erw [← NatTrans.naturality_assoc]
      dsimp
      rw [← Functor.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app]
      dsimp
      rw [map_id, map_id, Category.id_comp, commShiftOfLocalization.iso_hom_app,
        Category.assoc, Category.assoc, Category.assoc, ← map_comp_assoc,
        Iso.inv_hom_id_app, map_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ (ofHom W f).map F hF = F.map f

Tactic:
map_ofHom

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ F.map f = F.map f
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁷ : Category.{v_1, u_1} C
inst✝¹⁶ : HasShift C ℤ
inst✝¹⁵ : Category.{v_2, u_2} D
inst✝¹⁴ : HasZeroObject D
inst✝¹³ : HasShift D ℤ
inst✝¹² : Preadditive D
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : Pretriangulated D
inst✝⁹ : Category.{v_3, u_3} A
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
this✝ : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact

Tactic:
rw [L.distTriang_iff] at hT

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁷ : Category.{v_1, u_1} C
inst✝¹⁶ : HasShift C ℤ
inst✝¹⁵ : Category.{v_2, u_2} D
inst✝¹⁴ : HasZeroObject D
inst✝¹³ : HasShift D ℤ
inst✝¹² : Preadditive D
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : Pretriangulated D
inst✝⁹ : Category.{v_3, u_3} A
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
this✝ : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
T : Triangle D
hT✝ : T ∈ distinguishedTriangles
hT : T ∈ L.essImageDistTriang
⊢ ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : W.LeftFraction X Y
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk g) ≫ e.hom.app Y = g.map L ⋯

Tactic:
rw [← MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk,
    MorphismProperty.LeftFraction.Localization.homMk_eq g,
    g.map_compatibility (MorphismProperty.LeftFraction.Localization.Q W) L,
    assoc, assoc, Iso.inv_hom_id_app, comp_id, Iso.inv_hom_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ RightFractionRel φ ψ

Tactic:
rw [← leftFractionRel_op_iff, ← LeftFraction.map_eq_iff L.op W.op φ.op ψ.op,
    ← φ.op_map L (Localization.inverts _ _), ← ψ.op_map L (Localization.inverts _ _)]

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ (φ.map L ⋯).op = (ψ.map L ⋯).op
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
h : P T.obj₁
⊢ P.trW T.mor₂

Tactic:
rw [trW_iff']

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
h : P T.obj₁
⊢ ∃ X f h, ∃ (_ : Triangle.mk f T.mor₂ h ∈ distinguishedTriangles), P X
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
⊢ K.op.IsStrictlySupported e.op

Tactic:
isStrictlySupported_op_iff

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
K L : HomologicalComplex C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
⊢ K.IsStrictlySupported e
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).op = 0

Tactic:
by rw [X.shape j i hij, op_zero]

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c.symm
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).op = 0

Tactic:
by rw [X.shape j i hij, op_zero]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ inr (map f (f ≫ g) (𝟙 X₁) g ⋯) ≫ (mappingConeCompHomotopyEquiv f g).inv = (mappingConeCompTriangle f g).mor₂

Tactic:
simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.inv]

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso ((unopFunctor V c).map φ.op)

Tactic:
quasiIso_unopFunctor_map_iff

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso φ
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
⊢ ¬e.BoundaryLE i

Tactic:
by
  by_cases hij : c.Rel i j
  · exact e.not_boundaryLE_prev hij
  · subst hk
    simpa only [c.prev_eq_self j hij] using hj

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj' : ∃ j, e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
obtain ⟨j, hj⟩ := hj'
        rw [f_eq φ hj, L.extend_d_eq e hi hj]
        subst hi hj
        simp [HomologicalComplex.restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
by
  by_cases hjk : c.Rel j k
  · rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]
  · rw [shape _ _ _ hjk, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
⊢ (K.sc' i' j' k').HasHomology

Tactic:
subst hi'' hk''

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
hi' : e.f i = c'.prev j'
hk' : e.f k = c'.next j'
⊢ (K.sc' (c'.prev j') j' (c'.next j')).HasHomology
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ (K.restrictionToTruncGE' e ≫ truncGE'Map φ e).f i = (restrictionMap φ e ≫ L.restrictionToTruncGE' e).f i

Tactic:
simp [restrictionToTruncGE'_f_eq_iso_hom_iso_inv _ e rfl hi,
      truncGE'Map_f_eq φ e hi rfl, restrictionXIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ QuasiIsoAt (K.ιTruncLE e) j'

Tactic:
have := K.op.quasiIsoAt_πTruncGE e.op hj'
  exact inferInstanceAs (QuasiIsoAt ((unopFunctor _ _).map (K.op.πTruncGE e.op).op) j')

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₂.f i₂))) (e₂.f i₂) ⋯) (ac.desc' x₁ x₂ (ac.equiv.symm (e₂.f i₂))) = x₂ i₂

Tactic:
ac.desc'_inr _ _ _ i₂ (ac.equiv.injective (by simp)),

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₂.f i₂))) (e₂.f i₂) ⋯)
      ((desc.aux X (e₂.f i₂) (ac.equiv (ac.equiv.symm (e₂.f i₂))) ⋯) (x₂ i₂)) =
    x₂ i₂
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Tactic:
· rw [quasiIsoAt_iff_exactAt]
      all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ φ = 0

Tactic:
by
  apply ac.hom_ext'
  · rw [ac.isStrictlySupportedOutside₂_iff]
    infer_instance
  · rw [ac.isStrictlySupportedOutside₁_iff]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: case e_β
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝⁵ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝⁴ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
this✝ : HasSmallLocalizedHom W₂ Y' (Φ.functor.obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Y)
⊢ (Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom) =
    (SmallHom.mk W₂ eY.hom).comp ((SmallHom.mk W₂ eY.inv).comp ((Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom)))

Tactic:
← SmallHom.comp_assoc,

Goal state after:
case e_β
C₁ : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁸ : HasSmallLocalizedHom W₁ X Y
inst✝⁷ : HasSmallLocalizedHom W₁ Y Z
inst✝⁶ : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst✝⁵ : HasSmallLocalizedHom W₂ X' X'
inst✝⁴ : HasSmallLocalizedHom W₂ Y' Y'
inst✝³ : HasSmallLocalizedHom W₂ Z' Z'
inst✝² : HasSmallLocalizedHom W₂ X' Y'
inst✝¹ : HasSmallLocalizedHom W₂ Y' Z'
inst✝ : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor.obj X ≅ X'
eY : Φ.functor.obj Y ≅ Y'
eZ : Φ.functor.obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this✝⁵ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
this✝⁴ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Y'
this✝³ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) Z'
this✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
this✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) Z'
this✝ : HasSmallLocalizedHom W₂ Y' (Φ.functor.obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Y)
⊢ (Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom) =
    ((SmallHom.mk W₂ eY.hom).comp (SmallHom.mk W₂ eY.inv)).comp ((Φ.smallHomMap g).comp (SmallHom.mk W₂ eZ.hom))
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

Tactic:
exact h₂ j hij

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
⊢ Function.Bijective mk₀

Tactic:
let := HasDerivedCategory.standard C
  have h : (singleFunctor C 0).FullyFaithful := Functor.FullyFaithful.ofFullyFaithful _
  let e : (X ⟶ Y) ≃ Ext X Y 0 :=
    (h.homEquiv.trans (ShiftedHom.homEquiv _ (by simp))).trans homEquiv.symm
  have he : e.toFun = mk₀ := by
    ext f : 1
    dsimp [e]
    apply homEquiv.injective
    apply (Equiv.apply_symm_apply _ _).trans
    symm
    apply SmallShiftedHom.equiv_mk₀
  rw [← he]
  exact e.bijective

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ QuasiIsoAt (descShortComplex S) n

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]
    let φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅
        (triangleh S.f) n _ rfl).δlast ⟶ (composableArrows₅ hS n _ rfl).δlast :=
      homMk₄ ((homologyFunctorFactors C (up ℤ) _).hom.app _)
        ((homologyFunctorFactors C (up ℤ) _).hom.app _)
        ((homologyFunctorFactors C (up ℤ) _).hom.app _ ≫
          HomologicalComplex.homologyMap (descShortComplex S) n)
        ((homologyFunctorFactors C (up ℤ) _).hom.app _)
        ((homologyFunctorFactors C (up ℤ) _).hom.app _)
        ((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
        (by
          erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc]
          -- Disable `Fin.reduceFinMk`, otherwise `Precomp.obj_succ` does not fire. (https://github.com/leanprover-community/mathlib4/issues/27382)
          dsimp [-Fin.reduceFinMk]
          rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex])
        (by
          -- Disable `Fin.reduceFinMk`, otherwise `Precomp.obj_succ` does not fire. (https://github.com/leanprover-community/mathlib4/issues/27382)
          dsimp [-Fin.reduceFinMk]
          erw [homologySequenceδ_triangleh hS]
          simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj, assoc,
            Iso.inv_hom_id_app, comp_id])
        ((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f)
    have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) := by
      apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
        ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
          (mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
        (composableArrows₅_exact hS n _ rfl).δlast φ
      all_goals dsimp [φ]; infer_instance
    apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f))

Goal state after: