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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0

Tactic:
have : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π _ j = 0 := by
        rw [← reassoc_of% hg, reassoc_of% hf, zero_comp]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
⊢ (G.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ G).hom =
    𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) ≫ inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

Tactic:
rw [map_inr, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : HasZeroObject C
X : HomotopyCategory C (ComplexShape.up ℤ)
⊢ contractibleTriangle X ∈ distinguishedTriangles C

Tactic:
by
  obtain ⟨X⟩ := X
  refine ⟨_, _, 𝟙 X, ⟨?_⟩⟩
  have h := (isZero_quotient_obj_iff _).2 ⟨CochainComplex.mappingCone.homotopyToZeroOfId X⟩
  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) h.isoZero.symm
    (by simp) (h.eq_of_tgt _ _) (by dsimp; ext)

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
inst✝ : L.IsLocalization W
X : C
hX : W (𝟙 X)
⊢ (isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)

Tactic:
by
  rw [← cancel_mono (isoOfHom L W (𝟙 X) hX).hom, Iso.inv_hom_id, id_comp,
    isoOfHom_hom, Functor.map_id]

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

Goal state before:
pp: case mpr.nil
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
⊢ P (G.map Quiver.Path.nil)

Tactic:
simpa only [Functor.map_id] using! hP₁ (𝟙 X₁.obj)

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

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y✝ Z : C
z₁ : W.LeftFraction X Y✝
z₂ : W.LeftFraction Y✝ Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s
Y : C
t : z₄.Y' ⟶ Y
ht : W t
fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t
⊢ W (z₂.s ≫ z₃'.s ≫ z₄.s ≫ t)

Tactic:
exact W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))

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
this : Zero (L.obj X ⟶ L.obj Y) := { zero := L.map 0 }
⊢ AddCommGroup (L.obj X ⟶ L.obj Y)

Tactic:
letI : Add (L.obj X ⟶ L.obj Y) := ⟨add' W⟩

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
this✝ : Zero (L.obj X ⟶ L.obj Y) := { zero := L.map 0 }
this : Add (L.obj X ⟶ L.obj Y) := { add := add' W }
⊢ AddCommGroup (L.obj X ⟶ L.obj Y)
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case succ.inl
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k')

pp: case succ.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k' : J
hk' : ¬IsMax k'
hkk' : Order.succ k' ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj : Order.succ k' ≤ Order.succ k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k')

Tactic:
· refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
      dsimp
      rw [transfiniteIterate_succ _ _ _ hk']
      apply hφ

Goal state after:
case succ.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k' : J
hk' : ¬IsMax k'
hkk' : Order.succ k' ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj : Order.succ k' ≤ Order.succ k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k')
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
this✝¹ : P.IsClosedUnderIsomorphisms
this✝ : HasFiniteCoproducts P.FullSubcategory
this : ∀ (J : Type ?u.31) [Finite J], PreservesColimitsOfShape (Discrete J) P.ι
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
exact ⟨fun J _ ↦ P.isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι _⟩

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 Q : ObjectProperty C
inst✝² : P.IsTriangulated
inst✝¹ : Q.IsTriangulated
inst✝ : Q.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : (P ⊓ Q) T.obj₁
h₃ : (P ⊓ Q) T.obj₃
⊢ (P ⊓ Q).isoClosure T.obj₂

Tactic:
by
    obtain ⟨Y, hY, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1
    exact ⟨Y, ⟨hY, Q.prop_of_iso e (Q.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩

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

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
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁸ : Pretriangulated C
inst✝⁷ : HasShift D ℤ
inst✝⁶ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : W.IsCompatibleWithTriangulation
n : ℤ
⊢ (shiftFunctor W.Localization n).Additive

Tactic:
rw [Localization.functor_additive_iff W.Q W]
  exact Functor.additive_of_iso (W.Q.commShiftIso n)

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₃
n : ℤ
⊢ ((mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n =
    (mappingConeCompTriangle f g).mor₃.f n

Tactic:
simp [mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.hom,
    lift_f _ _ _ _ _ (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (((opFunctor V c).map φ₁.op).f n).unop =
    ((((dNext n) fun i j ↦ (h.hom j i).op) + (prevD n) fun i j ↦ (h.hom j i).op) + ((opFunctor V c).map φ₂.op).f n).unop

Tactic:
dsimp
    rw [h.comm n]
    nth_rw 2 [add_comm]
    rfl

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (((unopFunctor V c).map φ₁.op).f n).op =
    ((((dNext n) fun i j ↦ (h.hom j i).unop) + (prevD n) fun i j ↦ (h.hom j i).unop) +
        ((unopFunctor V c).map φ₂.op).f n).op

Tactic:
dsimp
    rw [h.comm n]
    nth_rw 2 [add_comm]
    rfl

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

Goal state before:
pp: case pos
ι : 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 : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

Tactic:
· have hk' : e.f k = k' := by rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
    rw [K.extend_d_eq e hj' hk', Iso.inv_hom_id_assoc,
      ← cancel_mono (K.extendXIso e hk').inv, zero_comp, assoc]

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0
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
⊢ ((K.restriction e).sc' i j k).HasHomology

Tactic:
by subst hi hk; assumption

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

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✝ : ∀ (j : ι), K.HasHomology j
j' : ι'
⊢ (K.extend e).HasHomology j'

Tactic:
by_cases h : ∃ j, e.f j = j'

Goal state after:
case pos
ι : 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✝ : ∀ (j : ι), K.HasHomology j
j' : ι'
h : ∃ j, e.f j = j'
⊢ (K.extend e).HasHomology j'

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
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : ∀ (j : ι), K.HasHomology j
j' : ι'
h : ¬∃ j, e.f j = j'
⊢ (K.extend e).HasHomology j'
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case mpr
ι : 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 : HomologicalComplex C c
a✝ : K.IsStrictlySupported e₂
⊢ K.IsStrictlySupportedOutside e₁

Tactic:
exact ⟨fun i₁ => K.isZero_X_of_isStrictlySupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Goal state after:
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
inst✝ : ∀ (i : ℤ), HasHomology K i
n : ℤ
⊢ IsIso (K.πTruncGE n) ↔ K.IsStrictlyGE n

Tactic:
by
  apply HomologicalComplex.isIso_πTruncGE_iff

Goal state after:
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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsLE n
⊢ QuasiIso (K.ιTruncLE n)

Tactic:
rw [quasiIso_ιTruncLE_iff]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsLE n
⊢ K.IsLE n
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₂ ≫ φ.app ⟨2, ⋯⟩ ≫ R₂.map (homOfLE ⋯) = 0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7

Tactic:
reassoc_of% h₁,

Goal state after:
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
⊢ 0 ≫ R₂.map (homOfLE ⋯) = 0 ≫ app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7
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₁.Exact
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0

Tactic:
simpa only [R₂.map'_comp 1 2 3] using hR₂.toIsComplex.zero 1

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
n k : ℕ
h : k + 4 ≤ n
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ k₄ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
hk₄ : k₄ = k + 4
h₀ : Epi (app' φ k₀ ⋯)
h₁ : IsIso (app' φ k₁ ⋯)
h₃ : IsIso (app' φ k₃ ⋯)
h₄ : Mono (app' φ k₄ ⋯)
⊢ IsIso (app' φ k₂ ⋯)

Tactic:
subst_vars
  change Epi (app' φ (k₀ + 0)) at h₀
  rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ h₄ ⊢
  exact isIso_of_epi_of_isIso_of_isIso_of_mono (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) _ h₀ h₁ h₃ h₄

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
    (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).inv.app S.X₁

Tactic:
dsimp
  rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _),
    assoc, assoc, assoc, Iso.inv_hom_id_app,
    ← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]
  apply yoneda.map_injective
  ext ⟨A⟩ (x : A ⟶ _)
  obtain ⟨A', π, _, x', w, hx'⟩ :=
    (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)
  erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]
  dsimp
  -- simp? says
  simp only [Iso.inv_hom_id_app, HomologicalComplex.homologyFunctor_obj, Iso.inv_hom_id_app_assoc,
    comp_id]
  erw [comp_id]
  rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx',
    HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
  /- We decompose the cocycle `x'` into two morphisms `a : A' ⟶ S.X₁.X n₁`
     and `b : A' ⟶ S.X₂.X n₀` satisfying certain relations. -/
  obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h
  rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc,
    assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp,
    d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero,
    add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp,
    d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w
  /- We simplify the RHS. -/
  conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f,
    inl_v_descShortComplex_f, comp_zero, zero_add]
  rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
    (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]
  /- We simplify the LHS. -/
  dsimp [Functor.shiftMap, homologyFunctor_shift]
  rw [HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc,
    S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by lia) (n₁ + 1) (by simp),
    Iso.inv_hom_id_app]
  dsimp [homologyFunctor_shift]
  simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc,
    shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg, comp_id,
    inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero]

Goal state after: