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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated 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₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂ =
    ((shiftFunctor C 1).map w₁₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁ ≫ u₁₂
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
← opShiftFunctorEquivalence_unitIso_inv_naturality,

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated 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₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂ =
    ((shiftFunctor C 1).map w₁₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map u₁₂).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: 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
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsZero ((t.truncLE n₀).obj X)

Tactic:
exact (Triangle.isZero₁_iff_isIso₂ _ (t.triangleLEGE_distinguished n₀ n₁ h X)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hY : IsZero Y
⊢ epiWithInjectiveKernel f ↔ Injective X

Tactic:
simp only [epiWithInjectiveKernel, hY.epi f, true_and]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
hY : IsZero Y
⊢ Injective (kernel f) ↔ Injective X
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝² : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝¹ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
hf : L₂.map f.hom = L₂.map 0
⊢ L₁.map f = 0

Tactic:
rw [MorphismProperty.map_eq_iff_postcomp L₂ B.trW] at hf

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝² : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝¹ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
hf : ∃ Z s, ∃ (_ : B.trW s), f.hom ≫ s = 0 ≫ s
⊢ L₁.map f = 0
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
a b : ℤ
X : C
φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X
hφ :
  (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app X
⊢ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
exact t.from_truncGE_obj_ext (by cat_disch)

Goal state after:
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
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : LeftHomotopyRel x✝¹ x✝
⊢ RightHomotopyClass.mk x✝¹ = RightHomotopyClass.mk x✝

Tactic:
rw [RightHomotopyClass.mk_eq_mk_iff]
    exact h.rightHomotopyRel

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
X Y : FibrantObject C
f : X ⟶ Y
⊢ WeakEquivalence (toHoCat.map f) ↔ WeakEquivalence f

Tactic:
by
  simp only [weakEquivalence_iff]
  apply MorphismProperty.quotient_iff

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inl
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
q : ℤ
hq✝ : q ≤ n
hq : q < n
⊢ QuasiIsoAt (ι f n) q

pp: case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
⊢ QuasiIsoAt (ι f n) n

Tactic:
· have := quasiIsoAt_π f n q hq
    rw [← quasiIsoAt_iff_comp_right _ (π f n), mappingCocone.lift_fst]
    exact hf q hq

Goal state after:
case inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝² : EnoughInjectives C
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
⊢ QuasiIsoAt (ι f n) n
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
⊢ IsConnected
    ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y)

Tactic:
let w := (TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv)
  have : Nonempty (w.CostructuredArrowDownwards y) :=
    ⟨(fromRightResolution Φ L y).obj (Classical.arbitrary _)⟩
  suffices ∀ (X : w.CostructuredArrowDownwards y),
      ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y) by
    refine zigzag_isConnected (fun X X' => ?_)
    obtain ⟨Y, hX⟩ := this X
    obtain ⟨Y', hX'⟩ := this X'
    exact hX.trans ((zigzag_obj_of_zigzag _ (isPreconnected_zigzag Y Y')).trans hX'.symm)
  intro X
  obtain ⟨c, g, x, fac, rfl⟩ := TwoSquare.CostructuredArrowDownwards.mk_surjective X
  dsimp [w] at x fac
  rw [id_comp] at fac
  let ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary _
  refine ⟨RightResolution.mk ρ.w.left ρ.hw.1, ?_⟩
  have := zigzag_obj_of_zigzag
    (fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac)
      (isPreconnected_zigzag (RightResolution.mk (𝟙 _) (W₂.id_mem _))
        (RightResolution.mk ρ.w.right ρ.hw.2))
  refine Zigzag.trans ?_ (Zigzag.trans this ?_)
  · exact Zigzag.of_hom (eqToHom (by simp))
  · apply Zigzag.of_inv
    refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_
    ext
    simp [← cancel_epi (isoOfHom L W₂ ρ.w.left ρ.hw.1).hom, ← L.map_comp_assoc, fac]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + ↑q
⊢ epiWithInjectiveKernel ((π f n₀).f i)

Tactic:
rw [← midπ_π_f f n₀ q]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q : ℕ
hq : i ≤ n₀ + ↑q
⊢ epiWithInjectiveKernel ((midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
hK : K.IsGE n
⊢ L.IsGE n

Tactic:
← DerivedCategory.isGE_Q_obj_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
hK : (DerivedCategory.Q.obj K).IsGE n
⊢ (DerivedCategory.Q.obj L).IsGE n
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
⊢ (CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus =
    (homotopyEquivalences (InjectiveObject C) (ComplexShape.up ℤ)).inverseImage
      (CochainComplex.Plus.ι (InjectiveObject C))

Tactic:
ext K L f
  simp [CochainComplex.Plus.quasiIso, Functor.mapCochainComplexPlus,
    ← HomologicalComplex.isIso_quotient_map_iff_homotopyEquivalences,
    CochainComplex.IsKInjective.quasiIso_iff,
    ← isIso_iff_of_reflects_iso _ ((InjectiveObject.ι C).mapHomotopyCategory (.up ℤ))]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j j' : ι
h : j = j'
⊢ ¬c.Rel j j'

Tactic:
by
  subst h
  exact c.not_rel_self j

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

Goal state before:
pp: case pos
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:
subst hi
      by_cases hj : j = i₁
      · subst hj
        nth_rw 2 [dif_neg (by tauto)]
        rw [comp_zero]
      · rw [dif_neg (by tauto), zero_comp]

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

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ (C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)

Tactic:
rw [(C.X i).map_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
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
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
have fac : cc.π ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f' := by
    rw [← cancel_mono h.i, h.f'_i, ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i,
      assoc, IsComplex.cokerToKer'_fac]

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
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
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
fac : Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf = h.f'
⊢ Epi (hS.cokerToKer' k hk cc kf hcc hkf)
Module: Mathlib.Algebra.Homology.GrothendieckAbelian

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
inst✝¹ : c.HasNoLoop
inst✝ : Small.{w, t} ι
⊢ HasSeparator (HomologicalComplex C c)

Tactic:
have : HasCoproductsOfShape ι C :=
      hasColimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{w} ι)).symm

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
inst✝¹ : c.HasNoLoop
inst✝ : Small.{w, t} ι
this : HasCoproductsOfShape ι C
⊢ HasSeparator (HomologicalComplex C c)
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = -↑(n + 1)
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology K n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology K' n
⊢ homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m =
    ((h.homologyIsoNeg n m hmn).hom ≫ homologyMap fK n ≫ (h'.homologyIsoNeg n m hmn).inv) ≫
      homologyι h'.cochainComplex m

Tactic:
dsimp [homologyIsoNeg]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
m : ℤ
hmn : m = -↑(n + 1)
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology K n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology K' n
⊢ homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m =
    (((restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              ⋯).inv ≫
          homologyMap h.restrictionLEIso.hom n) ≫
        homologyMap fK n ≫
          homologyMap h'.restrictionLEIso.inv n ≫
            (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯).hom) ≫
      homologyι h'.cochainComplex m
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ Cofork.π (CokernelCofork.ofπ (pOpcycles P.complex 0) ⋯) ≫
      (P.complex.isoHomologyι₀.symm ≪≫
          isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom =
    Cofork.π P.cokernelCofork

Tactic:
← cancel_mono (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _).inv,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ (Cofork.π (CokernelCofork.ofπ (pOpcycles P.complex 0) ⋯) ≫
        (P.complex.isoHomologyι₀.symm ≪≫
            isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom) ≫
      (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt).inv =
    Cofork.π P.cokernelCofork ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt).inv
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫
      ιTensorObj X₁ (tensorObj X₂ X₃) i₁ (i₂ + i₃) j ⋯ ≫ tensorHom f₁ (tensorHom f₂ f₃) j =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      Y₁ i₁ ◁ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯

Tactic:
ι_tensorHom,

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫
      (f₁ i₁ ⊗ₘ tensorHom f₂ f₃ (i₂ + i₃)) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      Y₁ i₁ ◁ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (𝟙 (X₁ i₁) ≫ f₁ i₁ ⊗ₘ ιTensorObj X₂ X₃ i₂ i₃ (i₂ + i₃) ⋯ ≫ tensorHom f₂ f₃ (i₂ + i₃)) ≫
      ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      (𝟙 (Y₁ i₁) ⊗ₘ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯

Tactic:
ι_tensorHom,

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (𝟙 (X₁ i₁) ≫ f₁ i₁ ⊗ₘ (f₂ i₂ ⊗ₘ f₃ i₃) ≫ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫
      ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯ =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫
      (𝟙 (Y₁ i₁) ⊗ₘ ιTensorObj Y₂ Y₃ i₂ i₃ (i₂ + i₃) ⋯) ≫ ιTensorObj Y₁ (tensorObj Y₂ Y₃) i₁ (i₂ + i₃) j ⋯
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ≫
      ιTensorObj (tensorObj X₁ X₂) X₃ (i₁ + i₂) i₃ j ⋯ ≫ tensorHom (tensorHom f₁ f₂) f₃ j =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ Y₃ i₃ ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯

Tactic:
ι_tensorHom,

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ X₃ i₃ ≫
      (tensorHom f₁ f₂ (i₁ + i₂) ⊗ₘ f₃ i₃) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ▷ Y₃ i₃ ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ (ιTensorObj X₁ X₂ i₁ i₂ (i₁ + i₂) ⋯ ≫ tensorHom f₁ f₂ (i₁ + i₂) ⊗ₘ f₃ i₃) ≫
      ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      (ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ 𝟙 (Y₃ i₃)) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯

Tactic:
ι_tensorHom,

Goal state after:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ((f₁ i₁ ⊗ₘ f₂ i₂) ≫ ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ f₃ i₃) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯ =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫
      (ιTensorObj Y₁ Y₂ i₁ i₂ (i₁ + i₂) ⋯ ⊗ₘ 𝟙 (Y₃ i₃)) ≫ ιTensorObj (tensorObj Y₁ Y₂) Y₃ (i₁ + i₂) i₃ j ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
⊢ hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) ≫
      Fork.ι (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) =
    X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯ ≫ Fork.ι (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯)

Tactic:
simpa using! hi.fac _ .zero

Goal state after: