mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ (asIso (S₂.liftCycles φ.τ₂ w)).symm.hom ≫
      Fork.ι (KernelFork.ofι { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.f ⋯) =
    Fork.ι (KernelFork.ofι S₂.iCycles ⋯)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ i ≫ 𝟙 X = (underlyingIso i).inv ≫ (mk i).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ Over.Hom.left
      ((fun k ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) ⋯)
        ((fun k ↦ homMk (image.lift { I := g.obj.left, m := g.arrow, m_mono := ⋯, e := Over.Hom.left k, fac := ⋯ }) ⋯)
          k)) =
    Over.Hom.left k

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ f ≫ 𝟙 X = 𝟙 Y ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ (asIso (pullback.map i f (mk i).arrow f (underlyingIso i).inv (𝟙 Y) (𝟙 X) ⋯ ⋯)).hom ≫ pullback.snd (mk i).arrow f =
    pullback.snd i f

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.iCycles ≫ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.g = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
A : C
i : A ⟶ Y
w✝ : Mono i
⊢ pullback.fst (mk i).arrow f ≫ (Iso.refl (underlying.obj (mk i))).hom =
    (underlyingIso (pullback.snd (mk i).arrow f)).symm.hom ≫
      (underlyingIso (pullback.snd (mk i).arrow f)).hom ≫ pullback.fst (mk i).arrow f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
A : C
i : A ⟶ Y
w✝ : Mono i
⊢ pullback.snd (mk i).arrow f ≫ (Iso.refl X).hom =
    (underlyingIso (pullback.snd (mk i).arrow f)).symm.hom ≫ (mk (pullback.snd (mk i).arrow f)).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
A : C
i : A ⟶ Y
w✝ : Mono i
⊢ (mk i).arrow ≫ (Iso.refl Y).hom = (Iso.refl (underlying.obj (mk i))).hom ≫ (mk i).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : h ≫ f = h ≫ g
⊢ equalizer.lift h w ≫ (MonoOver.mk (equalizer.ι f g)).arrow = h

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
A : C
i : A ⟶ Y
w✝ : Mono i
⊢ f ≫ (Iso.refl Y).hom = (Iso.refl X).hom ≫ f

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.liftCycles φ.τ₂ ⋯ ≫ h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂

Tactic:
h₁.lift_f,

Goal state after:
case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.liftCycles φ.τ₂ ⋯ ≫ S₂.iCycles = 𝟙 S₁.X₂ ≫ φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂ = 𝟙 S₂.cycles ≫ S₂.iCycles

Tactic:
h₁.lift_f,

Goal state after:
case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ kernel.lift f h w ≫ (MonoOver.mk (kernel.ι f)).arrow = h

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (kernelSubobject f).factorThru h ⋯ ≫ (kernelSubobject f).arrow = h

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (factorThruKernelSubobject f h w ≫ (kernelSubobjectIso f).hom) ≫ kernel.ι f = kernel.lift f h w ≫ kernel.ι f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ ((kernelSubobject f).arrow ≫ Arrow.Hom.left sq) ≫ f' = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
A B : C
⊢ kernelSubobject 0 = ⊤

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelSubobject 0 = ⊤

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
A : Subobject X
h : A.arrow ≫ f = 0
⊢ kernel.lift f A.arrow h ≫ kernel.ι f = A.arrow

Tactic:
simp

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

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✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
⊢ S.X₃ ⟶ J

Tactic:
by
  have := hS.mono_fromOpcycles
  exact Injective.factorThru (S.descOpcycles f hf) S.fromOpcycles

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : HasKernel (f ≫ h)
⊢ (kernelSubobject f).arrow ≫ f ≫ h = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ ((kernelSubobject (f ≫ h)).arrow ≫ f) ≫ h = 0 ≫ h

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
g : Subobject X
⊢ (pullback f).obj ((map f).obj g) = g

Tactic:
revert g

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
⊢ ∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ (kernelCompMono f h).inv ≫ kernel.ι (f ≫ h) = kernel.ι f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
⊢ ∀ [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk g)

Tactic:
hf

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
⊢ ∀ [inst : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk g)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
⊢ f ≫ ((forget Y).obj ⊤).hom = 𝟙 ⊤.obj.left ≫ f

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ kernel.lift g f w ≫ kernel.ι g = f

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow =
    factorThruKernelSubobject g f w ≫ (kernelSubobject g).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w ≫ (kernelSubobject g).arrow = 0 ≫ (kernelSubobject g).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w = (imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) ⋯ ≫ (kernelSubobject (g ≫ h)).arrow =
    (imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯) ≫ (kernelSubobject (g ≫ h)).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g ⋯ ≫ (kernelSubobject g).arrow =
    ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w ≫ (kernelSubobject (g ≫ h)).arrow =
    (imageToKernel f g ⋯ ≫ ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯).inv) ≫
      (kernelSubobject (g ≫ h)).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w ≫ (kernelSubobject g).arrow =
    ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g ⋯) ≫ (kernelSubobject g).arrow

Tactic:
simp

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w ≫ (kernelSubobject (i.inv ≫ g)).arrow =
    ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g ⋯ ≫ (kernelSubobjectIsoComp i.inv g).inv) ≫
      (kernelSubobject (i.inv ≫ g)).arrow

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasZeroObject V
inst✝ : Mono g
⊢ 0 ≫ g = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g h : MonoOver A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ Over.Hom.left k₂.hom ≫ ((forget A).obj g).hom = Over.Hom.left k₁.hom ≫ f.arrow

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ f ≫ 0 = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
⊢ ∀ [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)

Tactic:
hf

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
⊢ ∀ [inst : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (kernel.lift g.unop (kernel.ι f.unop) ⋯ ≫ kernel.ι g.unop).op = (kernel.ι f.unop).op

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
⊢ (k ≫ factorThruImage f) ≫ (MonoOver.mk (image.ι f)).arrow = k ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : (imageSubobject f).Factors (k ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : (imageSubobject f).Factors (k ≫ k' ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ k' ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ k' ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y X' : C
h : X' ⟶ X
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A B : C
⊢ (imageSubobjectIso 0 ≪≫ imageZero ≪≫ botCoeIsoZero.symm).hom ≫ ⊥.arrow = (imageSubobject 0).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ (asIso (imageToKernel S.f S.g ⋯)).hom ≫ (kernelSubobject S.g).arrow = (imageSubobject S.f).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ (underlyingIso f).symm).hom ≫ (Subobject.mk f).arrow =
    (imageSubobject f).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝¹ : IsIso h
f : X ⟶ Y
inst✝ : HasImage f
⊢ inv (image.preComp h f) ≫ image.ι (h ≫ f) = image.ι f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ ((kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : C
P : Subobject Y
⊢ IsIso P.arrow ↔ P = ⊤

Tactic:
rw [isIso_iff_mk_eq_top, mk_arrow]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.ι f ≫ Arrow.Hom.right sq = (imageSubobject f).arrow ≫ Arrow.Hom.right sq

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ (initialIsInitial.uniqueUpToIso HasZeroObject.zeroIsInitial).hom ≫ 0 = initial.to B

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ 0 ≫ ⊥.arrow = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ f ⊓ g ≤ f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ f ⊓ g ≤ g

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ (f ⊓ g).ofLE f ⋯ ≫ f.arrow = (f ⊓ g).ofLE g ⋯ ≫ g.arrow

Tactic:
simp

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

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
tfae_2_to_3 :
  (∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
x✝ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F := x✝
⊢ PreservesFiniteLimits F

Tactic:
by
    exact preservesFiniteLimits_of_preservesKernels F

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ ∀ {W' : C} (g' : W' ⟶ S.X₂) (eq' : g' ≫ S.g = 0), kernel.lift (cokernel.π S.f) g' ⋯ ≫ Abelian.image.ι S.f = g'

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ (f ⊓ g).Factors (s.fst ≫ f.arrow)

Tactic:
simpa using ⟨factors_comp_arrow s.fst, by simpa [s.condition] using factors_comp_arrow s.snd⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ ∀ {Z' : C} (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0), Abelian.coimage.π S.g ≫ cokernel.desc (kernel.ι S.g) g' ⋯ = g'

Tactic:
simp

Goal state after: