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
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Epi S.g ↔ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g
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:
constructor

Goal state after:
case mp
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 φ.τ₂

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

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
⊢ (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) =
    k

Tactic:
ext

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 : 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
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
⊢ ((Subobject.pullback f).obj y).Factors h ↔ y.Factors (h ≫ f)

Tactic:
by
  refine ⟨fun hf ↦ ?_, fun hF ↦ pullback_factors f y h hF⟩
  rw [factors_iff]
  use Subobject.factorThru _ _ hf ≫ Subobject.pullbackπ f y
  simp [(Subobject.isPullback f y).w]

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

Goal state before:
pp: 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:
constructor

Goal state after:
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

case mpr
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
⊢ A ≤ B → (map e.hom).obj A ≤ (map e.hom).obj B
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 = factorThruKernelSubobject g f w

Tactic:
ext

Goal state after:
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
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 = 0

Tactic:
ext

Goal state after:
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
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) ⋯ = imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯

Tactic:
ext

Goal state after:
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
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 ⋯ = (imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g w

Tactic:
ext

Goal state after:
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
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 = imageToKernel f g ⋯ ≫ ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯).inv

Tactic:
ext

Goal state after:
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
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 = (imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g ⋯

Tactic:
ext

Goal state after:
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
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 =
    (imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g ⋯ ≫ (kernelSubobjectIsoComp i.inv g).inv

Tactic:
ext

Goal state after:
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
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
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ image.ι f ≫ g = 0

Tactic:
ext

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
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = factorThruImage f ≫ 0
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
w : f ≫ g = 0
⊢ (imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom

Tactic:
ext

Goal state after:
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
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0
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
⊢ coprod.inl ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom = f.arrow

Tactic:
coprod.inl_desc

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.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
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w

Tactic:
ext

Goal state after:
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
w : f ≫ g = 0
⊢ (imageToKernel' f g w ≫ (kernelSubobjectIso g).inv) ≫ (kernelSubobject g).arrow =
    ((imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫ (kernelSubobject 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
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
constructor

Goal state after:
case mp
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 ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) → Epi (imageToKernel' S.f S.g ⋯)

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 ⋯
⊢ Epi (imageToKernel' S.f S.g ⋯) → Epi (kernel.lift S.g S.f ⋯)
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:
constructor

Goal state after:
case mp
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 ⋯)

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) → Epi (imageToKernel S.f S.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✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom

Tactic:
ext

Goal state after:
case h₁
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 h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inl ≫ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    coprod.inl ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom

case h₂
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 h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inr ≫ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    coprod.inr ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom
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 = k ≫ factorThruImageSubobject f

Tactic:
ext

Goal state after:
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
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 = k ≫ k' ≫ factorThruImageSubobject f

Tactic:
ext

Goal state after:
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
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:
constructor

Goal state after:
case mp
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

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ imageSubobject S.f = kernelSubobject 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
h : imageSubobject S.f = kernelSubobject S.g
⊢ imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f))

Tactic:
ext

Goal state after:
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
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
X : C
⊢ ∀ (a : Subobject X), a ≤ Quotient.mk'' ⊤

Tactic:
refine Quotient.ind' fun f => ?_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f : MonoOver X
⊢ Quotient.mk'' f ≤ Quotient.mk'' ⊤
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 ⋯ =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g))

Tactic:
ext

Goal state after:
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
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✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
⊢ ∀ (a : Subobject X), Quotient.mk'' ⊥ ≤ a

Tactic:
refine Quotient.ind' fun f => ?_

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
f : MonoOver X
⊢ Quotient.mk'' ⊥ ≤ Quotient.mk'' f
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
⊢ image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv = (imageSubobjectIso f).inv ≫ imageSubobjectMap sq

Tactic:
ext

Goal state after:
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
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ (imageSubobject (Arrow.mk g).hom).arrow =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ (imageSubobject (Arrow.mk g).hom).arrow
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_3
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).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯ = s.snd

Tactic:
ext

Goal state after:
case refine_3
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).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯) ≫ g.arrow = s.snd ≫ 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
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
g'✝ : S.X₂ ⟶ Z'✝
eq'✝ : S.f ≫ g'✝ = 0
m✝ : Abelian.coimage S.g ⟶ Z'✝
hm : Abelian.coimage.π S.g ≫ m✝ = g'✝
⊢ m✝ = cokernel.desc (kernel.ι S.g) g'✝ ⋯

Tactic:
ext

Goal state after:
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
m✝ : Abelian.coimage S.g ⟶ Z'✝
hm : Abelian.coimage.π S.g ≫ m✝ = g'✝
⊢ coequalizer.π (kernel.ι S.g) 0 ≫ m✝ = coequalizer.π (kernel.ι S.g) 0 ≫ cokernel.desc (kernel.ι S.g) g'✝ ⋯
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯

Tactic:
ext

Goal state after:
case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ ≫ (f ⊓ g).arrow = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).arrow
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ coimageImageComparison (α.app X) = (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coequalizer.π (kernel.ι (α.app X)) 0 ≫ coimageImageComparison (α.app X)) ≫ equalizer.ι (cokernel.π (α.app X)) 0 =
    (coequalizer.π (kernel.ι (α.app X)) 0 ≫
        (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom) ≫
      equalizer.ι (cokernel.π (α.app X)) 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯)) ≫ f.arrow = smallCoproductDesc s

Tactic:
ext

Goal state after:
case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
b✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯)) ≫ f.arrow =
    Sigma.ι (fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫ smallCoproductDesc s
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
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ ⟨mk (W.arrow ≫ Y.arrow), ⋯⟩ ≤ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩ ↔ W ≤ Z

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ ⟨mk (W.arrow ≫ Y.arrow), ⋯⟩ ≤ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩ → W ≤ Z

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ W ≤ Z → ⟨mk (W.arrow ≫ Y.arrow), ⋯⟩ ≤ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop = (𝟙 (op (A ⨯ B))).unop

Tactic:
ext

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.fst

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.snd