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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
p : ℤ
r_f : (σ (p + 1 + 1)).r ≫ S.f.f (p + 1 + 1) = 𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ (σ (p + 1 + 1)).s
s_g : (σ (p + 1)).s ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))
⊢ p + 1 + -1 = ?m.127

Tactic:
by linarith

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ (∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)) → T ∈ distinguishedTriangles

Tactic:
rintro ⟨S, σ, ⟨e⟩⟩
    rw [rotate_distinguished_triangle, rotate_distinguished_triangle]
    refine isomorphic_distinguished _ ?_ _
      ((rotate _ ⋙ rotate _).mapIso e ≪≫
        CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso S σ)
    exact ⟨_, _, _, ⟨Iso.refl _⟩⟩

Goal state after:
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✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
⊢ { l // opcyclesMap S.g i ≫ l = k }

Tactic:
have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_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✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
H : { l // Cofork.π (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯) ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ { l // opcyclesMap S.g i ≫ l = k }
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
⊢ W.multiplicativeClosure = W.paths.strictMap (pathComposition C)

Tactic:
by
  refine le_antisymm ?_ fun _ _ _ ⟨h⟩ ↦ ?_
  · refine (W.multiplicativeClosure_le_iff _).2 fun X Y f hf ↦ ?_
    simpa using! W.paths.map_mem_strictMap (pathComposition C) f.toPath (by simpa)
  · exact composePath_mem _ <| monotone_paths W.le_multiplicativeClosure _ h

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

Goal state before:
pp: case pos
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)
⊢ { 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:
exact (snakeInput hS i _ h).L₀_exact

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

Goal state before:
pp: case pos
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)
⊢ { 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

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)
⊢ { 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:
· exact (snakeInput hS i _ h).L₀_exact

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)
⊢ { 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.Category.Quiv

Goal state before:
pp: V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
G : V ⥤q C
⊢ G ⋙q (Paths.of C ⋙q (pathComposition C).toPrefunctor) = G

Tactic:
pathsOf_pathComposition_toPrefunctor,

Goal state after:
V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
G : V ⥤q C
⊢ G ⋙q 𝟭q C = G
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂

Tactic:
by
    refine Functor.ext ?_ ?_
    · rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h
    · rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
      apply Functor.congr_hom h'

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

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E).IsEquivalence

Tactic:
let iso : (whiskeringLeft (MorphismProperty.Localization W) D E).obj
    (equivalenceFromModel L W).functor ⋙
      (Construction.whiskeringLeftEquivalence W E).functor ≅ whiskeringLeftFunctor L W E :=
    NatIso.ofComponents (fun F => eqToIso (by
      ext
      change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
      rw [Construction.fac])) (fun τ => by
        ext
        dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
        rw [ObjectProperty.eqToHom_hom, ObjectProperty.eqToHom_hom, eqToHom_app, eqToHom_app,
          eqToHom_refl, eqToHom_refl]
        dsimp
        rw [comp_id, id_comp]
        rfl)
  exact Functor.isEquivalence_of_iso iso

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
⊢ MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤

Tactic:
refine morphismProperty_eq_top'
      (MorphismProperty.naturalityProperty (NatTransExtension.app τ))
      ?_ (MorphismProperty.naturalityProperty.stableUnderInverse _)

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app τ) (W.Q.map f)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows

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
n : ℕ
Y : ComposableArrows D n
this : L.EssSurj
⊢ (L.mapComposableArrows n).essImage Y

Tactic:
induction n with
    | zero =>
      obtain ⟨Y, rfl⟩ := mk₀_surjective Y
      exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩
    | succ n hn =>
      obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y
      obtain ⟨Y', ⟨e⟩⟩ := hn Y
      obtain ⟨f', hf'⟩ := exists_rightFraction L W
        ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)
      refine ⟨Y'.precomp f'.f,
        ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩
      dsimp at hf' ⊢
      simp [← cancel_mono (e.inv.app 0), hf']

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
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ LeftFractionRel z₂ z₁

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
  exact ⟨Z, t₂, t₁, hst.symm, hft.symm, by simpa only [← hst] using ht⟩

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

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
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
⊢ ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u

Tactic:
rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']

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

Goal state before:
pp: 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
inst✝ : W.IsCompatibleWithShift A
a : A
⊢ W ≤ W.inverseImage (shiftFunctor C a)

Tactic:
rw [MorphismProperty.IsCompatibleWithShift.condition]

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

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
⊢ AddCommGroup (X' ⟶ Y')

Tactic:
by
  have := Localization.essSurj L W
  letI := addCommGroup' L W (L.objPreimage X') (L.objPreimage Y')
  exact Equiv.addCommGroup (homEquiv (L.objObjPreimageIso X') (L.objObjPreimageIso Y'))

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

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
inst✝⁷ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ L.map (f - g) = 0

Tactic:
exact h _ (by rw [L.map_sub, F.map_sub, hfg, sub_self])

Goal state after:
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
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ distinguishedTriangles
X₁ : C
h₁ : P X₁
e₁ : T.obj₁ ≅ X₁
X₃ : C
h₃ : P X₃
e₃ : T.obj₃ ≅ X₃
⊢ (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom) ≫ (shiftFunctor C 1).map e₁.inv = e₃.inv ≫ T.mor₃

Tactic:
simp only [assoc, ← Functor.map_comp, e₁.hom_inv_id,
            Functor.map_id, comp_id]

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : IsIso (homologyMap φ' i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ i)

Tactic:
exact IsIso.of_isIso_comp_right (homologyMap φ i) (homologyMap φ' i)

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
E : Type u_3
inst✝ : Category.{v_2, u_3} E
F : HomologicalComplex C c ⥤ E
hF : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy F
⊢ ∀ (x y : HomologicalComplex C c) (f₁ f₂ : x ⟶ y), homotopic C c f₁ f₂ → F.map f₁ = F.map f₂

Tactic:
by
    intro K L f g ⟨h⟩
    have : DecidableRel c.Rel := by classical infer_instance
    exact h.map_eq_of_inverts_homotopyEquivalences hc F hF

Goal state after:
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
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulated
⊢ P.trW.IsStableUnderFiniteProducts

Tactic:
rw [← trW_isoClosure]
  exact ⟨fun J _ => by
    refine MorphismProperty.IsStableUnderProductsOfShape.mk _ _ ?_
    intro _ _ X₁ X₂ f hf
    exact trW.mk _ (productTriangle_distinguished _
      (fun j => (hf j).choose_spec.choose_spec.choose_spec.choose))
      (P.isoClosure.prop_pi _
        (fun j => (hf j).choose_spec.choose_spec.choose_spec.choose_spec))⟩

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

Goal state before:
pp: case mpr
ι : 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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ (𝟙 K).f n = Hom.f 0 n

Tactic:
apply IsZero.eq_of_src

Goal state after:
case mpr
ι : 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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ IsZero (K.X n)
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
a b : ι
⊢ d K (some a) (some b) = (XIso K ⋯).hom ≫ K.d a b ≫ (XIso K ⋯).inv

Tactic:
simp [XIso, X, d]

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

Goal state before:
pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
· rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]

Goal state after:
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 M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ (if hi : e.BoundaryGE i then
        (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ opcyclesMap φ (e.f i) ≫ (L.truncGE'XIsoOpcycles e ⋯ hi).inv
      else (K.truncGE'XIso e ⋯ hi).hom ≫ φ.f (e.f i) ≫ (L.truncGE'XIso e ⋯ hi).inv) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ (K.truncGE'XIso e ⋯ ⋯).hom ≫ φ.f (e.f j) ≫ (L.truncGE'XIso e ⋯ ⋯).inv

Tactic:
· rw [dif_neg hi]
      simp [truncGE'_d_eq _ e hij rfl rfl hi]

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 : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Tactic:
have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)

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.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))
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'
inst✝ : HasZeroObject C
hK : (K.truncGE e).Acyclic
i : ι
⊢ K.ExactAt (e.f i)

Tactic:
by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
hi : ¬∃ j', c'.Rel (e.f i) j'
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
hi : ¬∃ j', c'.Rel (e.f i) j'
this : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i))
⊢ IsZero ((K.shortComplexTruncLE e).X₃.homology (e.f i))
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
⊢ mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯ = 𝟙 K

Tactic:
by
        ext i
        obtain hi | rfl | hi := lt_trichotomy i n
        · apply (K.isZero_of_isStrictlyGE n i (by lia)).eq_of_src
        · simp
        · apply (K.isZero_of_isStrictlyLE n i (by lia)).eq_of_tgt

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
h : (singleFunctor C n).map f₁ = (singleFunctor C n).map f₂
⊢ f₁ = f₂

Tactic:
have eq₁ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₁
    have eq₂ := NatIso.naturality_1 (singleFunctorCompHomologyFunctorIso C n) f₂
    dsimp at eq₁ eq₂
    rw [← eq₁, ← eq₂, h]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ IsIso (Q.map (CochainComplex.truncLEMap s n ≫ X.ιTruncLE n))

Tactic:
rw [Q.map_comp]
    infer_instance

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ IsIso (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))

Tactic:
rw [Q.map_comp]
    infer_instance

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a)))

Tactic:
rw [Q.map_comp]
    infer_instance

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
rw [Q.map_comp]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
rw [← cancel_mono (app' φ 3 _), assoc, NatTrans.naturality, reassoc_of% h₁,
      zero_comp, zero_comp]

Goal state after: