awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S T : VonNeumannAlgebra H
h : ∀ (x : H →L[ℂ] H), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (↑S : Set (H →L[ℂ] H)).centralizer.centralizer = (↑S : Set (H →L[ℂ] H))

Tactic:
S.centralizer_centralizer'

Premises used: VonNeumannAlgebra.centralizer_centralizer'
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (Subsemigroup.carrier
          (Submonoid.toSubsemigroup
            (Subsemiring.toSubmonoid
              (Subalgebra.toSubsemiring
                (StarSubalgebra.toSubalgebra
                  (StarSubalgebra.centralizer ℂ (↑S : Set (H →L[ℂ] H)))))))).centralizer.centralizer =
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup
        (Subsemiring.toSubmonoid
          (Subalgebra.toSubsemiring
            (StarSubalgebra.toSubalgebra (StarSubalgebra.centralizer ℂ (↑S : Set (H →L[ℂ] H)))))))

Tactic:
simp
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (↑S.commutant : Set (H →L[ℂ] H)) = (↑S : Set (H →L[ℂ] H)).centralizer

Tactic:
simp [commutant]

Premises used: VonNeumannAlgebra.commutant
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
rw : z ∈ (↑S : Set (H →L[ℂ] H)).centralizer ↔ ∀ g ∈ S, g * z = z * g
⊢ z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

Tactic:
rw [← SetLike.mem_coe, coe_commutant]

Premises used: SetLike.mem_coe, VonNeumannAlgebra.coe_commutant
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S : Set (H →L[ℂ] H)).centralizer ↔ ∀ g ∈ S, g * z = z * g

Tactic:
rfl
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (↑S.commutant.commutant : Set (H →L[ℂ] H)) = (↑S : Set (H →L[ℂ] H))

Tactic:
simp
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
simp : e ∈ S
| ∀ y ∈ S.commutant,
    (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
      (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)

Tactic:
simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]

Premises used: commute_iff_eq, Commute.symm_iff, ContinuousLinearMap.IsIdempotentElem.commute_iff, VonNeumannAlgebra.mem_commutant_iff
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
h : IsIdempotentElem e
S : VonNeumannAlgebra H
conv_rhs :
  e ∈ S ↔
    ∀ y ∈ S.commutant,
      (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
        (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)
conv_rhs₁ : e ∈ S ↔ e ∈ S
⊢ e ∈ S ↔
    ∀ y ∈ S.commutant,
      (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H) ∧
        (↑e : H →ₗ[ℂ] H).ker ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)

Tactic:
conv_rhs => simp [← h.commute_iff, Commute.symm_iff (a := e), commute_iff_eq, ← mem_commutant_iff]

Premises used: commute_iff_eq, Commute.symm_iff, ContinuousLinearMap.IsIdempotentElem.commute_iff, VonNeumannAlgebra.mem_commutant_iff
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
simp_rw :
  (∀ (x : H →L[ℂ] H) (x_1 : x ∈ S.commutant), e * (x * e) = x * e) →
    ∀ (x : H →L[ℂ] H) (x_1 : x ∈ S.commutant), e * (x * e) = e * x
⊢ e ∈ S ↔ ∀ y ∈ S.commutant, (↑e : H →ₗ[ℂ] H).range ∈ Module.End.invtSubmodule (↑y : H →ₗ[ℂ] H)

Tactic:
simp_rw [he.isIdempotentElem.mem_iff, he.isIdempotentElem.range_mem_invtSubmodule_iff,
    he.isIdempotentElem.ker_mem_invtSubmodule_iff, forall_and, and_iff_left_iff_imp, ← mul_def]

Premises used: IsStarProjection.isIdempotentElem, VonNeumannAlgebra.IsIdempotentElem.mem_iff, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, ContinuousLinearMap.mul_def, and_iff_left_iff_imp, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, forall_and
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
h : ∀ (x : H →L[ℂ] H) (x_1 : x ∈ S.commutant), e * (x * e) = x * e
x : H →L[ℂ] H
hx : x ∈ S.commutant
⊢ e * (x * e) = e * x

Tactic:
simpa [he.isSelfAdjoint.star_eq] using congr(star $(h _ (star_mem hx)))

Premises used: IsStarProjection.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α := X ⟶ Abelian.image f) (kernel.lift (cokernel.π f) f ⋯ : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
        (coimageImageComparison f) :
      X ⟶ Abelian.image f)
⊢ (imageMonoFactorisation f).e =
    CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
h :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (kernel.lift (cokernel.π f) f ⋯ : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
      (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
        (coimageImageComparison f))
      (equalizer.ι (cokernel.π f) 0)
⊢ Eq (α := X ⟶ Abelian.image f) (kernel.lift (cokernel.π f) f ⋯ : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
        (coimageImageComparison f) :
      X ⟶ Abelian.image f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (kernel.lift (cokernel.π f) f ⋯ : X ⟶ kernel (Y := cokernel f) (cokernel.π f))
      (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
        (coimageImageComparison f))
      (equalizer.ι (cokernel.π f) 0)

Tactic:
simp only [Abelian.coimageImageComparison, Category.assoc,
    cokernel.π_desc_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.cokernel.π_desc_assoc, CategoryTheory.Abelian.coimageImageComparison
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
simp :
  Eq (α := (imageMonoFactorisation f).I ⟶ Y)
    (CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
      (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m))
    (kernel.ι (cokernel.π f))
⊢ Eq (α := (imageMonoFactorisation f).I ⟶ Y)
    (CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f)) (cokernel.desc (kernel.ι f) F.e ⋯) ≫
      F.m)
    (kernel.ι (cokernel.π f))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
rw :
  Eq (α := Abelian.coimage f ⟶ Y) (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m)
    (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))
⊢ Eq (α := (imageMonoFactorisation f).I ⟶ Y)
    (CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
      (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m))
    (kernel.ι (cokernel.π f))

Tactic:
rw [IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
h :
  CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m) =
    CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))
⊢ Eq (α := Abelian.coimage f ⟶ Y) (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m)
    (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
F : MonoFactorisation f
⊢ CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m) =
    CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (CategoryStruct.comp (Y := (imageMonoFactorisation f).I) (coimageImageComparison f) (kernel.ι (cokernel.π f)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Mono f
inst_6 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
rw :
  IsIso (Y := (imageMonoFactorisation f).I)
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f))
⊢ IsIso (imageMonoFactorisation f).e

Tactic:
rw [imageMonoFactorisation_e']

Premises used: CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e'
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Mono f
inst_6 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
⊢ IsIso (Y := (imageMonoFactorisation f).I)
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f))

Tactic:
IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Mono f
inst_6 : IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
⊢ IsIso (Y := (imageMonoFactorisation f).I)
    (CategoryStruct.comp (Y := cokernel (X := kernel f) (kernel.ι f)) (cokernel.π (kernel.ι f))
      (coimageImageComparison f))

Tactic:
exact IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Epi f
dsimp : IsIso (X := Abelian.image f) (kernel.ι (cokernel.π f))
⊢ IsIso (imageMonoFactorisation f).m

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_5 : Epi f
⊢ IsIso (X := Abelian.image f) (kernel.ι (cokernel.π f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
⊢ HasImages.{v, u} C

Tactic:
{ has_image := fun {_} {_} f => { exists_image := ⟨imageFactorisation f⟩ } }

Premises used: CategoryTheory.Limits.HasImage.mk', CategoryTheory.Limits.HasImages.mk, Nonempty.intro, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
⊢ Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
⊢ HasImages.{v, u} C

Tactic:
haveI : Limits.HasImages C := hasImages
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this : HasImages.{v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this : HasEqualizers.{v, u} C
⊢ HasZeroObject.{v, u} C

Tactic:
haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
refine_2 :
  (aux :
      ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
        (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι f ⋯) =
          Fork.ι s) →
    IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
refine_1 :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)

Tactic:
have aux (s : KernelFork (cokernel.π f)) :
            (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι _ (cokernel.condition f)) = Fork.ι s := ?_
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
refine_2 :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f))
    (m_1 : s.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)),
    m_1 ≫ Fork.ι (KernelFork.ofι f ⋯) = Fork.ι s →
      m_1 =
        (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
            limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
          s
⊢ IsLimit (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)

Tactic:
refine isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux ?_

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.limit.lift, CategoryTheory.inv, CategoryTheory.Limits.isLimitAux, OfNat.ofNat, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ Fork.ι (KernelFork.ofι f ⋯) = Fork.ι A
⊢ g ≫ f = Fork.ι A

Tactic:
rw [KernelFork.ι_ofι] at hg

Premises used: CategoryTheory.Limits.KernelFork.ι_ofι
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : KernelFork (Y := cokernel f) (cokernel.π f)),
    (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (Y := cokernel f) (cokernel.π f)
g : A.pt ⟶ Cone.pt (F := parallelPair (Y := cokernel f) (cokernel.π f) 0) (KernelFork.ofι f ⋯)
hg : g ≫ f = Fork.ι A
refine_2 :
  g ≫ f =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
refine_2₁ :
  Fork.ι A =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
refine_2₂ :
  (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫
      Fork.ι (KernelFork.ofι f ⋯) =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
refine_2₃ refine_2₄ :
  (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
          limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
        A ≫
      f
⊢ g =
    (fun (A : KernelFork (Y := cokernel f) (cokernel.π f)) ↦
        limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e)
      A

Tactic:
rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]

Premises used: CategoryTheory.Limits.KernelFork.ι_ofι, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : KernelFork (Y := cokernel f) (cokernel.π f)
refine_1 :
  limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e ≫ f = Fork.ι s
⊢ (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
      Fork.ι (KernelFork.ofι f ⋯) =
    Fork.ι s

Tactic:
simp only [KernelFork.ι_ofι, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.KernelFork.ι_ofι
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Mono f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : KernelFork (Y := cokernel f) (cokernel.π f)
⊢ CategoryStruct.comp (Y := limit (parallelPair (Y := cokernel f) (cokernel.π f) 0))
      (limit.lift (parallelPair (Y := cokernel f) (cokernel.π f) 0) s)
      (limit.π (parallelPair (Y := cokernel f) (cokernel.π f) 0) WalkingParallelPair.zero) =
    s.π.app WalkingParallelPair.zero

Tactic:
limit.lift_π s WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.WalkingParallelPair.zero