mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
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.IsGE X a
h : ¬a ≤ b
this : t.IsGE X b
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
exact t.isGE_of_iso (show X ≅ _ from asIso ((t.truncGEπ b).app X)) _

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: 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
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsLE X b
⊢ t.IsLE ((t.truncGE a).obj X) b

Tactic:
rw [t.isLE_iff_isZero_truncGE_obj b (b + 1) rfl]

Goal state after:
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
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsLE X b
⊢ IsZero ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
⊢ Function.Bijective fun f ↦ f.postcomp g

Tactic:
have hi : Function.Bijective (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp h.i) := by
    rw [← Function.Bijective.of_comp_iff'
      (postcomp_bijective_of_fibration_of_weakEquivalence X h.r)]
    convert! Function.bijective_id
    ext φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    simp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi : Function.Bijective fun f ↦ f.postcomp h.i
⊢ Function.Bijective fun f ↦ f.postcomp g
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
⊢ IsIso (Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

Tactic:
by
  rw [NatTrans.isIso_iff_isIso_app]
  intro X
  apply Localization.inverts L (weakEquivalences _)
  rw [← weakEquivalence_iff]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
⊢ IsIso (HoCat.resolutionCompToLocalizationNatTrans L)

Tactic:
by
  rw [NatTrans.isIso_iff_isIso_app]
  intro X
  apply Localization.inverts L (weakEquivalences _)
  rw [← weakEquivalence_iff]
  infer_instance

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

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
a✝ : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
⊢ w.GuitartExact

Tactic:
let w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 _

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
a✝ : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 (B.op.op ⋙ unopUnop C₄)
⊢ w.GuitartExact
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f : w.StructuredArrowRightwards g
⊢ ∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm

Tactic:
obtain ⟨g, φ, rfl⟩ := StructuredArrow.mk_surjective f
  obtain ⟨X₁, b, rfl⟩ := g.mk_surjective
  obtain ⟨a, ha, rfl⟩ := CostructuredArrow.homMk_surjective φ
  exact ⟨X₁, a, b, by simpa using ha, rfl⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
⊢ P g

Tactic:
by
  let X₀ : Paths (LocQuiver W) := ⟨X⟩
  suffices ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀),
      P (StructuredArrow.mk ((Quotient.functor (relations W)).map f)) by
    obtain ⟨Y, g, rfl⟩ := g.mk_surjective
    obtain ⟨g, rfl⟩ := (Quotient.functor (relations W)).map_surjective g
    exact this g
  intro Y₀ f
  induction f with
  | nil => exact hP₀
  | cons f g hf =>
      obtain (g | ⟨w, hw⟩) := g
      · exact hP₁ g _ hf
      · simpa only [← Construction.wInv_eq_isoOfHom_inv w hw] using! hP₂ w hw _ hf

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
X : C
inst✝ : F.HasPointwiseRightDerivedFunctorAt W X
⊢ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

Tactic:
by
  rwa [← hasPointwiseRightDerivedFunctorAt_iff F L W]

Goal state after:
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₂
⊢ F.HasPointwiseRightDerivedFunctor W₂

Tactic:
rw [Φ.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure]

Goal state after:
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₂
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsLeftDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
this : B.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
⊢ B.IsLeftDerivabilityStructure

Tactic:
let e' := CatCommSq.iso B.functor W₁'.Q W₂'.Q F

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsLeftDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
this : B.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
⊢ B.IsLeftDerivabilityStructure
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
⊢ T.IsLeftDerivabilityStructure

Tactic:
let e' := CatCommSq.iso B.functor W₁'.Q W₂'.Q F

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
⊢ T.IsLeftDerivabilityStructure
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)

Tactic:
have : K.obj.IsGE n := (K.isGE_ι_obj_iff n).2 (by assumption)

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
this : K.obj.IsGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: 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
inst✝ : EnoughInjectives C
⊢ (localizerMorphism C).IsRightDerivabilityStructure

Tactic:
by
  rw [LocalizerMorphism.isRightDerivabilityStructure_iff_of_equivalences
    (T := localizerMorphism C) (B := FibrantObject.localizerMorphism (Plus C))
    (R := .id _) (L := fibrantObjectLocalizerMorphism C) (Iso.refl _)]
  infer_instance

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

Goal state before:
pp: 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✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ mapExactFunctor F (mk₀ f) = mk₀ (F.map f)

Tactic:
dsimp [Ext.mapExactFunctor, mk₀]

Goal state after:
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✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).smallShiftedHomMap
      ((F.mapCochainComplexSingleFunctor 0).app X) ((F.mapCochainComplexSingleFunctor 0).app Y)
      (SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) 0 mk₀._proof_1
        ((CochainComplex.singleFunctor C 0).map f)) =
    SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 mk₀._proof_1
      ((CochainComplex.singleFunctor D 0).map (F.map f))
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

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
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
⊢ IsZero ((K.stupidTrunc e).X i')

Tactic:
by_cases hi'' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi''
      exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso (K.stupidTruncXIso e hi)
    · apply isZero_stupidTrunc_X
      simpa using hi''

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : ¬j = i₁
⊢ ((if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
      if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
    0

Tactic:
· rw [dif_neg (by tauto), zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| η.app X✝.obj ≫ (F ⋙ shiftFunctor D 1).map f.f

pp: case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d

Tactic:
← η.naturality f.f

Goal state after:
case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| (shiftFunctor C 1 ⋙ F).map f.f ≫ η.app Y✝.obj

case a
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
| F.map X✝.d
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : ¬i = i₀
⊢ ((if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
      if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
    0

Tactic:
· rw [dif_neg (by tauto), zero_comp]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i✝ : ℤ
⊢ (i✝ + 1).negOnePow = -i✝.negOnePow

Tactic:
Int.negOnePow_succ

Goal state after:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i✝ : ℤ
⊢ -i✝.negOnePow = -i✝.negOnePow
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.negSucc.succ.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc (0 + 1) + 1 = m
⊢ h.d (Int.negSucc (0 + 1)) m ≫ h.d m p = 0

Tactic:
obtain rfl : m = -1 := by lia

Goal state after:
case pos.negSucc.succ.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
hmp : -1 + 1 = p
hnm : Int.negSucc (0 + 1) + 1 = -1
⊢ h.d (Int.negSucc (0 + 1)) (-1) ≫ h.d (-1) p = 0
Module: Mathlib.Algebra.Homology.ExactSequenceFour

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.Exact
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
this✝ : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
this : Epi (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
apply isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi (P.π.f (n✝ + 1))

Tactic:
rw [π_f_succ]

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi 0
Module: Mathlib.CategoryTheory.Abelian.Ext

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
x : Opposite.unop (Opposite.op ((ProjectiveResolution.self X).complex.X (n + 1))) ⟶ Y
⊢ (ModuleCat.Hom.hom (𝟙 (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂))
      x =
    (ModuleCat.Hom.hom 0) x

Tactic:
obtain rfl : x = 0 := (HomologicalComplex.isZero_single_obj_X
    (ComplexShape.down ℕ) 0 X (n + 1) (by simp)).eq_of_src _ _

Goal state after:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ (ModuleCat.Hom.hom (𝟙 (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂))
      0 =
    (ModuleCat.Hom.hom 0) 0
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case refine_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).inv ≫
      (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).hom ≫
          X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
            (shiftFunctor C 1).map (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso f).inv)) ≫
        (shiftFunctor C 1).map (X.ω₁.map (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso g).inv ≫
      X.ω₁.map (isoMk₁ (Iso.refl (F.obj w✝¹)) (Iso.refl (F.obj w✝)) ⋯).hom ≫ X.δ'.app (mk₂ (F.map f) (F.map g))

Tactic:
simp only [← Functor.map_comp_assoc, ← Functor.map_comp, Category.assoc,
        Iso.inv_hom_id, Functor.map_id, Category.id_comp] at this ⊢

Goal state after:
case refine_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map
        (X.ω₁.map
          ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom)) =
    X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso g).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝¹)) (Iso.refl (F.obj w✝)) ⋯).hom) ≫
      X.δ'.app (mk₂ (F.map f) (F.map g))
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i₀ i₁ i₂ : ι
f : i₀ ⟶ i₁
g : i₁ ⟶ i₂
fg : i₀ ⟶ i₂
hfg : f ≫ g = fg
h₁ : IsZero ((X.H n₀).obj (mk₁ f))
h₂ : IsZero ((X.H n₁).obj (mk₁ f))
this✝ : Mono ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
this : Epi ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))
⊢ IsIso ((X.H n₀).map (twoδ₁Toδ₀ f g fg hfg))

Tactic:
apply isIso_of_mono_of_epi

Goal state after: