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

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
inst✝³ : Preadditive D
A : Type u_3
inst✝² : Category.{v_3, u_3} A
inst✝¹ : Abelian A
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : HomotopyCategory.Plus C),
    HomotopyCategory.plus D ((HomotopyCategory.Plus.ι C ⋙ F.mapHomotopyCategory (ComplexShape.up ℤ)).obj X)

Tactic:
by
      rintro ⟨X, hX⟩
      obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective X
      dsimp
      simp only [HomotopyCategory.plus_quotient_obj_iff] at hX ⊢
      obtain ⟨n, _⟩ := hX
      exact ⟨n, inferInstanceAs (CochainComplex.IsStrictlyGE
        ((F.mapHomologicalComplex _).obj K) n)⟩

Goal state after:
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
a b : ℤ
h : a + 1 = b
⊢ t.truncLE a = t.truncLT b

Tactic:
← h

Goal state after:
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
a b : ℤ
h : a + 1 = b
⊢ t.truncLE a = t.truncLT (a + 1)
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
a b : ℤ
h : a + 1 = b
⊢ t.truncGT a = t.truncGE b

Tactic:
← h

Goal state after:
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
a b : ℤ
h : a + 1 = b
⊢ t.truncGT a = t.truncGE (a + 1)
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : HomotopyCategory C (ComplexShape.up ℤ)
φ : K ⟶ L
hK : HomotopyCategory.subcategoryAcyclic C K
hL : HomotopyCategory.plus C L
⊢ ∃ Z a b, HomotopyCategory.plus C Z ∧ HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = φ

Tactic:
obtain ⟨K : CochainComplex _ _, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
    obtain ⟨L : CochainComplex _ _, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
    simp only [HomotopyCategory.plus_quotient_obj_iff] at hL
    obtain ⟨n, hn⟩ := hL
    obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective φ
    rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hK
    refine ⟨(HomotopyCategory.quotient _ _).obj (K.truncGE n),
      (HomotopyCategory.quotient _ _).map (K.πTruncGE n),
      (HomotopyCategory.quotient _ _).map (CochainComplex.truncGEMap φ n ≫ inv (L.πTruncGE n)),
      ?_, ?_, by simp [← Functor.map_comp]⟩
    · simp only [HomotopyCategory.plus_quotient_obj_iff]
      exact ⟨n, inferInstance⟩
    · rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic]
      exact hK.truncGE _

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
⊢ (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse = (B.inverseImage A.ι).op.trW

Tactic:
ext ⟨X₁⟩ ⟨X₂⟩ a
  simp [trW_op, trW_inverseImage_ι_iff, ← op_inf]

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 Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
h : g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) + (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    σ₁.r ≫ { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.f +
      { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.g ≫ σ₁.s

Tactic:
← h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
h : g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) + (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    σ₁.r ≫ { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.f +
      (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)
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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ t.IsLE ((t.truncLT n₁).obj X) n₀

Tactic:
← h

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ t.IsLE ((t.truncLT (n₀ + 1)).obj X) n₀
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
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₃ : t.IsGE T.obj₃ n
⊢ IsIso ((t.truncLT n).map T.mor₁)

Tactic:
rw [isIso_truncLT_map_iff]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₃ : t.IsGE T.obj₃ n
⊢ ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h ∈ distinguishedTriangles), t.IsGE Z n
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
n : ℤ
⊢ f ≫ α f n = 0

Tactic:
simp [α]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝² : T.IsEquivalence
inst✝¹ : B.IsEquivalence
inst✝ : IsIso w.natTrans
⊢ w.GuitartExact

Tactic:
by
  rw [← guitartExact_op_iff]
  infer_instance

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 : ℤ
hi : i ≤ n + ↑0
⊢ IsIso (homologyMap f i)

Tactic:
apply IsZero.isIso

Goal state after:
case hX
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 : ℤ
hi : i ≤ n + ↑0
⊢ IsZero (homology K i)

case hY
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 : ℤ
hi : i ≤ n + ↑0
⊢ IsZero (homology L 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 L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
⊢ QuasiIsoAt (ι f n₀) i

Tactic:
obtain ⟨q, hq⟩ : ∃ (q : ℕ), i + 1 ≤ n₀ + q := ⟨(i + 1 - n₀).natAbs, by lia⟩

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 + 1 ≤ n₀ + ↑q
⊢ QuasiIsoAt (ι f n₀) i
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: case hP₀
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
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := ⋯
⊢ P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))

Tactic:
convert! hP₀
    simp

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

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

Tactic:
by
  have : K.obj.IsGE n := (K.isGE_ι_obj_iff n).2 (by assumption)
  obtain ⟨L, _, ⟨e⟩⟩ := DerivedCategory.exists_iso_Q_obj_of_isGE K.obj n
  obtain ⟨M, _, i, hi⟩ :=
    CochainComplex.Plus.exists_quasiIso_injective ⟨L, ⟨n, inferInstance⟩⟩ n
  have : QuasiIso i.hom := by assumption
  exact ⟨M, inferInstance,
    ⟨DerivedCategory.Plus.ι.preimageIso ((asIso (DerivedCategory.Q.map i.hom)).symm ≪≫ e.symm)⟩⟩

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

Goal state before:
pp: case refine_2
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) ≤ CochainComplex.Plus.quasiIso C

Tactic:
intro K L f hf
    exact homotopyEquivalences_le_quasiIso _ _ _ hf

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

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      (((Plus.prepathObject { obj := K₂, property := ⋯ }).map (CochainComplex.Plus.localizerMorphism C).functor).map
          (CochainComplex.plus C).ι).p₀ =
    (ObjectProperty.homMk f₀).hom

pp: case refine_2.refine_2
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      (((Plus.prepathObject { obj := K₂, property := ⋯ }).map (CochainComplex.Plus.localizerMorphism C).functor).map
          (CochainComplex.plus C).ι).p₁ =
    (ObjectProperty.homMk f₁).hom

Tactic:
all_goals
        dsimp [Functor.mapCochainComplexPlus]
        cat_disch

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

Goal state before:
pp: 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₁
K : HomologicalComplex C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ = φ'

Tactic:
by
  ext k
  by_cases h : k = i₀ ∨ k = i₁
  · obtain rfl | rfl := h <;> assumption
  · simp only [not_or] at h
    apply (isZero_double_X f hi₀₁ k h.1 h.2).eq_of_src

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
⊢ toSingleMk 0 h = 0

Tactic:
simp [toSingleMk]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
⊢ (toSingleMk f h).v p q h = f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv

Tactic:
simp [toSingleMk]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (φ.app x✝¹.X).f ≫ (G.map f.f).f

pp: case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f

Tactic:
← h

Goal state after:
case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (φ.app x✝.X).f

case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
x✝¹ x✝ : Karoubi C
f : x✝¹ ⟶ x✝
h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f
h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x✝¹.p).f
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ.app P.X).f ≫ (G.map P.p).f

pp: case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ'.app P.X).f

pp: case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f

Tactic:
← h

Goal state after:
case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (φ.app P.X).f

case a.a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (φ'.app P.X).f

case a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    e.inv.app (X j) ≫
      (F.map (φ j)).app Y ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯

Tactic:
← NatTrans.naturality_assoc e.inv

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    (𝟭 D).map (φ j) ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
⊢ X.δ g h n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = 0

Tactic:
X.zero₁_assoc g h _ rfl n₀ n₁ hn₁,

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f : i ⟶ j
g : j ⟶ k
h : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
eq : (X.H n₁).map (twoδ₂Toδ₁ g h (g ≫ h) ⋯) ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = X.δ f g n₁ n₂ ⋯
⊢ 0 ≫ X.δ f (g ≫ h) n₁ n₂ ⋯ = 0
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
⊢ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = 𝟙 (X.opcycles f g n)

Tactic:
← cancel_epi (X.pOpcycles f g n),

Goal state after:
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 : ι
f : i ⟶ j
g : j ⟶ k
n : ℤ
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f g (𝟙 (mk₂ f g)) n = X.pOpcycles f g n ≫ 𝟙 (X.opcycles f g n)
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' (α ≫ α') n

Tactic:
← cancel_epi (X.pOpcycles f g n),

Goal state after:
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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n =
    X.pOpcycles f g n ≫ X.opcyclesMap f g f'' g'' (α ≫ α') n
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ X.opcyclesMap f g f' g' α n ≫ X.fromOpcycles f' g' fg' h' n = X.fromOpcycles f g fg h n ≫ (X.H n).map β

Tactic:
← cancel_epi (X.pOpcycles f g n),

Goal state after:
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 : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n ≫ X.fromOpcycles f' g' fg' h' n =
    X.pOpcycles f g n ≫ X.fromOpcycles f g fg h n ≫ (X.H n).map β