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

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
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq) ≫ (PreservesKernel.iso G g).hom

Tactic:
PreservesKernel.iso_hom,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq) ≫ kernelComparison g G
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesKernel.iso G f).hom ≫ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    G.map (kernel.map f g p q hpq) ≫ kernelComparison g G

Tactic:
PreservesKernel.iso_hom,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernelComparison f G ≫ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    G.map (kernel.map f g p q hpq) ≫ kernelComparison g G
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

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
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (cokernel.π f) ⋯))
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
| 0 - 0

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

Tactic:
next => skip

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ factorThruImage f = 0

Tactic:
by simp [← cancel_mono (Limits.image.ι f)]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).inv = kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯

Tactic:
by
  ext
  rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
    imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
    kernel.lift_ι, Limits.image.fac]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ e = 0

Tactic:
have : (-g) ≫ d = 0 := calc
      (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inr_desc]
      _ = biprod.inr ≫ u := by rw [Category.assoc, hd]
      _ = 0 := biprod.inr_desc _ _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this : (-g) ≫ d = 0
⊢ e = 0
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h : IsIso γ.left.φH.op
⊢ IsIso γ.left.φH

Tactic:
apply isIso_of_op

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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
let γ₁ := leftHomologyMapData φ₁ h₁ h₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ 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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Tactic:
let γ₁ := leftHomologyMapData φ₁ h₁ h₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ 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
φ : 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

Tactic:
hb

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
⊢ x = x
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Tactic:
rw [leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
    S.homologyData h₁ h₂]
  dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyMapIso', leftHomologyIso,
    RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', rightHomologyIso]
  simp only [assoc, ← leftHomologyMap'_comp_assoc, id_comp, ← rightHomologyMap'_comp]

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
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 ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z'✝ : C
x : h.K ⟶ Z'✝
hx : f' ≫ x = 0
b : h.H ⟶ Z'✝
hb : h.π ≫ b = x
⊢ h.π ≫ b = x

Tactic:
hb

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 ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
Z'✝ : C
x : h.K ⟶ Z'✝
hx : f' ≫ x = 0
b : h.H ⟶ Z'✝
hb : h.π ≫ b = x
⊢ x = x
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₁ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₁

pp: case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₂ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₂

pp: case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₃ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₃

Tactic:
· exact h₁.uniq (π₁.mapCone s) _ (fun j => π₁.congr_map (hm j))

Goal state after:
case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₂ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₃ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (S.map F).g = (h.map F).p ≫ F.map h.g'

Tactic:
map_g,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ F.map S.g = (h.map F).p ≫ F.map h.g'
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (c.ι.app j).τ₁ ≫ h₁.desc (π₁.mapCocone s) = (s.ι.app j).τ₁
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) = (s.ι.app j).τ₂
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ c.pt.f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ (s.ι.app j).τ₁ ≫ s.pt.f = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)

Tactic:
eq₁₂',

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (c.ι.app j).τ₁ ≫ h₁.desc (π₁.mapCocone s) = (s.ι.app j).τ₁
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) = (s.ι.app j).τ₂
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ c.pt.f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ (F.obj j).f ≫ (s.ι.app j).τ₂ = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op

Tactic:
rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂

Tactic:
h.comm₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives C
⊢ ∀ (X : D), Nonempty (ProjectivePresentation X)

Tactic:
intro X

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives C
X : D
⊢ Nonempty (ProjectivePresentation X)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)

Tactic:
intro X

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂

Tactic:
h.comm₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Tactic:
h.comm₂

Goal state after:
case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.toCycles = 𝟙 S.cycles

Tactic:
rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.f = S.iCycles
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
⊢ IsIso (Over.Hom.left f.hom) ↔ Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom

Tactic:
isIso_hom_left_iff_subobjectMk_eq

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
⊢ Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom ↔ Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
x : Subobject X
⊢ (pullback (𝟙 X)).obj x = x

Tactic:
by
  induction x using Quotient.inductionOn' with | _ f
  exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
⊢ (map e.hom).obj A ≤ (map e.hom).obj B → A ≤ B

Tactic:
intro h
      apply_fun (map e.inv).obj at h
      · simpa only [← map_comp, e.hom_inv_id, map_id] using h
      · apply Functor.monotone

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ IsColimit (L.mapCocone (Cofork.ofπ (cokernel.π f) ⋯))
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ IsColimit (L.mapCocone (Cofork.ofπ (cokernel.π f) ⋯))

Tactic:
apply (CokernelCofork.isColimitMapCoconeEquiv _ L).2

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ IsColimit (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂

Tactic:
intro f₁

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂

Tactic:
intro f₁

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ ∀ (j : CostructuredArrow L Y),
    (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₁).app Y =
      (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₂).app Y

Tactic:
intro X

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₂).app Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ ∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j

Tactic:
intro X

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X