mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasKernel (cokernel.π f)
inst✝³ : PreservesColimit (parallelPair f 0) F
inst✝² : PreservesLimit (parallelPair (cokernel.π f) 0) F
inst✝¹ : HasCokernel (F.map f)
inst✝ : HasKernel (cokernel.π (F.map f))
⊢ F.map (Abelian.factorThruImage f) ≫ (iso F f).hom = Abelian.factorThruImage (F.map f)

Tactic:
by
  ext; simp [iso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasCokernel (kernel.ι f)
inst✝³ : PreservesLimit (parallelPair f 0) F
inst✝² : PreservesColimit (parallelPair (kernel.ι f) 0) F
inst✝¹ : HasKernel (F.map f)
inst✝ : HasCokernel (kernel.ι (F.map f))
⊢ (iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) = Abelian.factorThruCoimage (F.map f)

Tactic:
by
  ext; simp [iso]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Biproducts

Goal state before:
pp: J : Type w
f : J → AddCommGrpCat
s : Fan f
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) 0) = 0

Tactic:
simp only [Functor.const_obj_obj, map_zero]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    (coprod.inr ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
coprod.inr_desc

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ (coprod.inr ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
coprod.inr_desc

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
| -a - b

Tactic:
neg_sub

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
| -b - a
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ IsColimit (CokernelCofork.ofπ f ⋯)

Tactic:
have aux (s : CokernelCofork (kernel.ι f)) :
            Cofork.π (CokernelCofork.ofπ _ (kernel.condition f)) ≫
              inv (imageMonoFactorisation f).m ≫ inv (Abelian.coimageImageComparison f) ≫
                colimit.desc (parallelPair (kernel.ι f) 0) s = Cofork.π s := ?_

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
⊢ IsColimit (CokernelCofork.ofπ f ⋯)

case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
⊢ Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
    Cofork.π s
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: 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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ (e₁.inv ≫ S₁.f) ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom

Tactic:
assoc,

Goal state after:
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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₁.inv ≫ S₁.f ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: 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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₁.inv ≫ S₁.f ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom

Tactic:
assoc,

Goal state after:
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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₁.inv ≫ S₁.f ≫ e₂.hom = S₂.f ≫ e₂.inv ≫ e₂.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: 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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ (e₂.inv ≫ S₁.g) ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom

Tactic:
assoc,

Goal state after:
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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₂.inv ≫ S₁.g ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: 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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₂.inv ≫ S₁.g ≫ e₃.hom = (S₂.g ≫ e₃.inv) ≫ e₃.hom

Tactic:
assoc,

Goal state after:
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
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ e₃.inv ≫ e₃.hom
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
⊢ e = 0

Tactic:
have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa [u]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
⊢ e = 0

Tactic:
have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa [u]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
⊢ e = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ (x ≫ S.f) ≫ S.g = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ x ≫ S.f ≫ S.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0

Tactic:
by rw [hx, assoc, S.zero, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ (h.ι ≫ φ) ≫ h.ι = 𝟙 h.H ≫ h.ι

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ h.ι ≫ φ ≫ h.ι = 𝟙 h.H ≫ h.ι
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (eK.hom ≫ h.i) ≫ S.g = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ eK.hom ≫ h.i ≫ S.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ ((Cocone.precompose (parallelPair.ext (Iso.refl S.X₁) eK.symm ⋯ ⋯).inv).obj (CokernelCofork.ofπ h.π ⋯)).pt ≅
    (CokernelCofork.ofπ (eK.hom ≫ h.π ≫ eH.inv) ⋯).pt

Tactic:
by exact eH.symm

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.i ≫ φ.τ₂ ≫ S₂.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ φK ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ φK ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ φK ≫ h₂.i = φ.τ₁ ≫ h₂.f' ≫ h₂.i
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ (h₁.i ≫ h₂.p) ≫ h₂.g' = h₁.π ≫ 0

Tactic:
assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.i ≫ h₂.p ≫ h₂.g' = h₁.π ≫ 0
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ ((Cone.postcompose (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯).hom).obj (KernelFork.ofι h.ι ⋯)).pt ≅
    (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).pt

Tactic:
by exact eH.symm

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ

Tactic:
simp only [← cancel_epi h.cyclesIso.hom, ← cancel_mono h.leftHomologyIso.hom, assoc,
    Iso.inv_hom_id, comp_id, Iso.hom_inv_id_assoc,
    LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ (h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯) ≫ h₂.ι = 0 ≫ h₂.ι

Tactic:
assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ ≫ h₂.ι = 0 ≫ h₂.ι
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ (x ≫ inv φ.τ₂) ≫ S₁.g = 0

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ x ≫ inv φ.τ₂ ≫ S₁.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ (x ≫ inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ x ≫ (inv φ.τ₂ ≫ S₁.g) ≫ φ.τ₃ = 0 ≫ φ.τ₃

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
⊢ x ≫ inv φ.τ₂ ≫ S₁.g ≫ φ.τ₃ = 0 ≫ φ.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ (b ≫ h.i) ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ b ≫ h.i ≫ φ.τ₂ = (h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i) ≫ φ.τ₂

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ b ≫ h.i ≫ φ.τ₂ = h.liftK (x ≫ inv φ.τ₂) ⋯ ≫ h.i ≫ φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ b ≫ h.i ≫ φ.τ₂ = (x ≫ inv φ.τ₂) ≫ φ.τ₂

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
W'✝ : C
x : W'✝ ⟶ S₂.X₂
hx : x ≫ S₂.g = 0
b : W'✝ ⟶ h.K
hb : b ≫ i = x
⊢ b ≫ h.i ≫ φ.τ₂ = x ≫ inv φ.τ₂ ≫ φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
⊢ ((φ.τ₁ ≫ f') ≫ h.i) ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
⊢ (φ.τ₁ ≫ f') ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
⊢ (φ.τ₁ ≫ f') ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
⊢ φ.τ₁ ≫ f' ≫ h.i ≫ φ.τ₂ = (h.f' ≫ h.i) ≫ φ.τ₂