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

Goal state before:
pp: case refine_4
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃'
v₁₂' : X₂' ⟶ Z₁₂'
w₁₂' : Z₁₂' ⟶ (shiftFunctor C 1).obj X₁'
h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distinguishedTriangles
v₂₃' : X₃' ⟶ Z₂₃'
w₂₃' : Z₂₃' ⟶ (shiftFunctor C 1).obj X₂'
h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distinguishedTriangles
v₁₃' : X₃' ⟶ Z₁₃'
w₁₃' : Z₁₃' ⟶ (shiftFunctor C 1).obj X₁'
h₁₃' : Triangle.mk u₁₃' v₁₃' w₁₃' ∈ distinguishedTriangles
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
iso₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ≅ Triangle.mk u₁₂' v₁₂' w₁₂' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂
iso₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ≅ Triangle.mk u₂₃' v₂₃' w₂₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃
iso₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ≅ Triangle.mk u₁₃' v₁₃' w₁₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯
eq₁₂ :
  v₁₂ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ =
    e₂.hom ≫ v₁₂'
eq₁₂' :
  w₁₂ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ ≫ w₁₂'
eq₁₃ :
  v₁₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ =
    e₃.hom ≫ v₁₃'
eq₁₃' :
  w₁₃ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ ≫ w₁₃'
eq₂₃ :
  v₂₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ =
    e₃.hom ≫ v₂₃'
eq₂₃' :
  w₂₃ ≫ (shiftFunctor C 1).map e₂.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ ≫ w₂₃'
rel₁₂ : v₁₂' ≫ H.m₁ = u₂₃' ≫ v₁₃'
rel₁₃ : w₁₂' = H.m₁ ≫ w₁₃'
rel₂₂ : v₁₃' ≫ H.m₃ = v₂₃'
rel₂₃ : w₁₃' ≫ (shiftFunctor C 1).map u₁₂' = H.m₃ ≫ w₂₃'
⊢ w₁₃ ≫ (shiftFunctor C 1).map u₁₂ = (iso₁₃.hom.hom₃ ≫ H.m₃ ≫ iso₂₃.inv.hom₃) ≫ w₂₃

Tactic:
rw [← cancel_mono (e₂.hom⟦(1 : ℤ)⟧'), assoc, assoc, assoc, assoc, eq₂₃',
      iso₂₃.inv_hom_id_triangle_hom₃_assoc, ← rel₂₃, ← Functor.map_comp, comm₁₂,
      Functor.map_comp, reassoc_of% eq₁₃']

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : Hom W X Y
z₂ : Hom W Y Z
⊢ ∀ (a : W.LeftFraction X Y) (b₁ b₂ : W.LeftFraction Y Z), LeftFractionRel b₁ b₂ → a.comp b₁ = a.comp b₂

Tactic:
rintro a b₁ b₂ ⟨U, t₁, t₂, hst, hft, ht⟩
    obtain ⟨z₁, fac₁⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₁.f)
    obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₂.f)
    obtain ⟨w₁, fac₁'⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs t₁)
    obtain ⟨w₂, fac₂'⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs t₂)
    obtain ⟨u, fac₃⟩ := exists_leftFraction (RightFraction.mk w₁.s w₁.hs w₂.s)
    dsimp at fac₁ fac₂ fac₁' fac₂' fac₃ ⊢
    have eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s := by
      rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
    obtain ⟨Z, p, hp, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a.hs eq
    simp only [assoc] at fac₄
    rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]
    apply Quot.sound
    refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ p, ?_, ?_, ?_⟩
    · dsimp
      simp only [assoc, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hst, reassoc_of% fac₃]
    · dsimp
      simp only [assoc, fac₄]
    · dsimp
      simp only [assoc]
      rw [← reassoc_of% fac₁', ← reassoc_of% fac₃, ← assoc]
      exact W.comp_mem _ _ ht (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ u.hs hp))

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
⊢ (P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J

Tactic:
by
  refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    exact P.strictLimitsClosureIter_le_limitsClosure J κ.ord
  · have (a : α) :
        (P.strictLimitsClosureIter J κ.ord).isoClosure.IsClosedUnderLimitsOfShape (J a) := ⟨by
      conv_rhs => rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]
      rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
        strictLimitsClosureStep]
      exact monotone_isoClosure ((le_trans (by rfl) (le_iSup _ a)).trans le_sup_right)⟩
    refine limitsClosure_le
      ((P.le_strictLimitsClosureIter J κ.ord).trans (le_isoClosure _))

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasTerminal C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
h : IsLimit (BinaryFan.mk (terminal.from Y) e.inv) :=
  BinaryFan.IsLimit.mk (BinaryFan.mk (terminal.from Y) e.inv) (fun {T} x f ↦ f ≫ e.hom) ⋯ ⋯ ⋯
⊢ P Y

Tactic:
exact P.prop_of_isLimit_binaryFan h P.prop_terminal hX

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ m₀ hm₀ f).comp g ⋯ = f ≫ g

Tactic:
subst hm₀
  simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Mono g
Z✝ : C
α β : Z✝ ⟶ x✝³
w : α ≫ f = β ≫ f
⊢ α = β

Tactic:
by
    rw [← cancel_mono h.i.left, ← cancel_mono g, Category.assoc, Category.assoc,
      h.i_w, reassoc_of% w]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ g ≫ Arrow.Hom.right h.r ≫ α = g ≫ Arrow.Hom.right h.r ≫ β

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ (g ≫ Arrow.Hom.right h.r) ≫ α = g ≫ Arrow.Hom.right h.r ≫ β

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ (g ≫ Arrow.Hom.right h.r) ≫ α = (g ≫ Arrow.Hom.right h.r) ≫ β
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
M : Type u_4
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
inst✝³ : HasShift D M
X Y : C
a : M
f : ShiftedHom X Y a
F G : C ⥤ D
τ : F ⟶ G
inst✝² : F.CommShift M
inst✝¹ : G.CommShift M
inst✝ : NatTrans.CommShift τ M
⊢ (f.map F).comp (mk₀ 0 ⋯ (τ.app Y)) ⋯ = (mk₀ 0 ⋯ (τ.app X)).comp (f.map G) ⋯

Tactic:
by
  rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]

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
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ P.trW g ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
rw [P.trW_iff]
  constructor
  · rintro ⟨Z, g, h, H, mem⟩
    exact ⟨_, _, _, inv_rot_of_distTriang _ H, P.le_shift (-1) _ mem⟩
  · rintro ⟨Z, g, h, H, mem⟩
    exact ⟨_, _, _, rot_of_distTriang _ H, P.le_shift 1 _ mem⟩

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
P Q : ObjectProperty C
h : P ≤ Q
⊢ P.trW ≤ Q.trW

Tactic:
by
  intro X Y f hf
  rw [trW_iff] at hf ⊢
  obtain ⟨Z, a, b, hT, hZ⟩ := hf
  exact ⟨Z, a, b, hT, h _ hZ⟩

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₃
⊢ (f ≫ g) ≫ 𝟙 X₃ = f ≫ g

Tactic:
by rw [comp_id]

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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
⊢ (u₁₂ ≫ u₂₃) ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃

Tactic:
by rw [comp_id]

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ False

Tactic:
rw [e.rel_iff] at hk

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hk : c.Rel j k
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : 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 ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0

Tactic:
dsimp [homRestrict]

Goal state after:
ι : 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 ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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
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 j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : c.Rel j k
⊢ IsLimit (KernelFork.ofι (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ⋯)

Tactic:
let e : parallelPair ((K.truncGE' e).d j k) 0 ≅
        parallelPair (K.fromOpcycles j' (e.f k)) 0 :=
      parallelPair.ext (K.truncGE'XIsoOpcycles e hj' hj)
        (K.truncGE'XIso e rfl (e.not_boundaryGE_next hjk))
        (by simp [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj]) (by simp)

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
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 j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e✝.f j = j'
hj : e✝.BoundaryGE j
hk' : c'.next j' = e✝.f k
hjk : c.Rel j k
e : parallelPair ((K.truncGE' e✝).d j k) 0 ≅ parallelPair (K.fromOpcycles j' (e✝.f k)) 0 :=
  parallelPair.ext (K.truncGE'XIsoOpcycles e✝ hj' hj) (K.truncGE'XIso e✝ ⋯ ⋯) ⋯ ⋯
⊢ IsLimit (KernelFork.ofι (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e✝ hj' hj).inv) ⋯)
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 : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ ((K.extend e).sc j').homologyπ ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.homologyIso.hom ≫
        (K.sc j).homologyData.left.homologyIso.inv =
    (K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ

Tactic:
ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc,

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫ (K.sc j).homologyData.left.homologyIso.inv =
    (K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inl
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : a ≤ b
⊢ ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) (b - a)).obj ((singleFunctor C 0).obj Y)) ≃
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
exact (Functor.FullyFaithful.ofFullyFaithful
        (shiftFunctor _ a)).homEquiv.trans
        ((shiftFunctorAdd' _ _ _ _ (Int.sub_add_cancel b a)).symm.app _).homToEquiv

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫
      Q.map f.τ₃ ≫
        inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂)) ≫
          Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫
      Q.map f.τ₃ ≫
        inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂)) ≫
          Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫
      Q.map f.τ₃ ≫
        inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂)) ≫
          Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    (Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
      inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂)) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    (Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
      inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂)) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    ((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
        inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
      Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    ((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
        inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
      Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    (((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
          inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X)))).comp
      ((ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map biprod.fst)).comp α.hom ⋯) ⋯ =
    α.hom

Tactic:
ShiftedHom.mk₀_comp_mk₀_assoc,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1
          ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X)) ≫ (singleFunctor C 0).map biprod.fst)).comp
      α.hom ⋯ =
    α.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X)))).comp
      ((ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map biprod.snd)).comp β.hom ⋯) ⋯ =
    β.hom

Tactic:
ShiftedHom.mk₀_comp_mk₀_assoc,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1
          ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X)) ≫ (singleFunctor C 0).map biprod.snd)).comp
      β.hom ⋯ =
    β.hom