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✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
⊢ ∀ (P : C) (g : P ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
⊢ ∀ (P : C) (g : P ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0
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
f g : MonoOver X
h : f.obj.left ≅ g.obj.left
w : h.hom ≫ g.arrow = f.arrow
⊢ f.arrow = f.arrow

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ i₁ = i₁

Tactic:
]

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✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ (g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom =
    (h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom

Tactic:
]

Goal state after:
case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ (g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom =
    (h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom
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
⊢ Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom ↔ Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom

Tactic:
]

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ 0 = 0

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯) ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂

Tactic:
]

Goal state after:
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
⊢ IsIso (S₂.liftCycles φ.τ₂ ⋯) ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂
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
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ Over.Hom.left e.hom ≫ h.arrow ≫ f = g.arrow ≫ f

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ Over.Hom.left e.hom ≫ h.arrow ≫ f = g.arrow ≫ f
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 φ.τ₂ ⋯)
⊢ Mono (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles)

Tactic:
]

Goal state after:
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 φ.τ₂ ⋯)
⊢ Mono (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles)
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 : image.obj f ⟶ g
⊢ factorThruImage f.hom ≫ (image.obj f).obj.hom = f.hom

Tactic:
]

Goal state after:
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 : image.obj f ⟶ g
⊢ factorThruImage f.hom ≫ (image.obj f).obj.hom = f.hom
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
⊢ mk (pullback.snd i f) = mk (pullback.snd (mk i).arrow f)

Tactic:
]

Goal state after:
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
⊢ mk (pullback.snd i f) = mk (pullback.snd (mk i).arrow f)
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
⊢ ∃ φ, IsPullback φ (mk (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f

Tactic:
]

Goal state after:
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
⊢ ∃ φ, IsPullback φ (mk (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst✝ : HasPullbacks C
y : Subobject Y
h : W ⟶ X
hf : ((Subobject.pullback f).obj y).Factors h
⊢ (representative.obj y).Factors (h ≫ f)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst✝ : HasPullbacks C
y : Subobject Y
h : W ⟶ X
hf : ((Subobject.pullback f).obj y).Factors h
⊢ (representative.obj y).Factors (h ≫ f)
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
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ g = (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ g

Tactic:
]

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 : (equalizerSubobject f g).Factors h
⊢ (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ g =
    (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ g

Tactic:
]

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 φ.τ₂
⊢ φ.τ₂ = φ.τ₂

Tactic:
]

Goal state after:
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 φ.τ₂
⊢ S₂.iCycles = S₂.iCycles

Tactic:
]

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
⊢ pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g =
    pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g

Tactic:
]

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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

pp: case hf₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₂.op.f = 0

pp: case hg₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₂.op.g = 0

pp: case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.op.f = 0

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

case hf₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₂.op.f = 0

case hg₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₂.op.g = 0

case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.op.f = 0
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g = (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g

Tactic:
]

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
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case hf₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case hg₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ 0 = 0

Tactic:
]

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 : (kernelSubobject f).Factors h
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ 0 = 0

Tactic:
]

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₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.unop.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.unop.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂
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 : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ f = f

Tactic:
]

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✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso ((underlyingIso (kernel.ι f)).hom ≫ (kernelCompMono f h).inv ≫ (underlyingIso (kernel.ι (f ≫ h))).inv)

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:
]

Goal state after:
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
⊢ IsIso ((underlyingIso (kernel.ι f)).hom ≫ (kernelCompMono f h).inv ≫ (underlyingIso (kernel.ι (f ≫ h))).inv)

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
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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f = S.f

Tactic:
]

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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.g = S.g

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.snd ((forget A).obj g).hom X✝.arrow ≫ X✝.arrow = pullback.snd ((forget A).obj g).hom X✝.arrow ≫ X✝.arrow

Tactic:
]

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

Goal state before:
pp: case refine_1
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
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫
      ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom

Tactic:
]

Goal state after:
case g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫
      ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom
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
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.snd g.obj.hom X✝.arrow ≫ X✝.arrow = pullback.snd g.obj.hom X✝.arrow ≫ X✝.arrow

Tactic:
]

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
this : Epi (image.ι f)
⊢ Epi (((imageSubobjectIso f).hom ≫ image.ι f) ≫ inv (kernelSubobject 0).arrow)

Tactic:
]

Goal state after:
ι : 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
this : Epi (image.ι f)
⊢ Epi (((imageSubobjectIso f).hom ≫ image.ι f) ≫ inv (kernelSubobject 0).arrow)
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✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (((forget A).prod (forget A)).obj (f, g)).1.hom = f.arrow

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (((forget A).prod (forget A)).obj (f, g)).1.hom = f.arrow
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case g.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯ ≫ g =
    pullback.snd (a.arrow ≫ h) k

Tactic:
]

Goal state after:
case g.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯ ≫ g =
    pullback.snd (a.arrow ≫ h) k
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✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (((forget A).prod (forget A)).obj (f, g)).2.hom = g.arrow

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (((forget A).prod (forget A)).obj (f, g)).2.hom = g.arrow
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
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
⊢ 0 = 0

Tactic:
]

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
⊢ Epi (imageToKernel' S.f S.g ⋯) ↔ Epi (imageToKernel S.f S.g ⋯)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel' S.f S.g ⋯) ↔ Epi (imageToKernel S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel S.f S.g ⋯) ↔ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel S.f S.g ⋯) ↔ IsIso (imageToKernel S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

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

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) ↔ imageSubobject S.f = kernelSubobject S.g
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✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasEqualizers C
⊢ 0 = 0

Tactic:
]

Goal state after: