awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v))
zero :
  ∀
    (x :
      (↑(Functor.obj (Functor.obj (Functor.const WalkingParallelPair) (kernelCone g).pt) WalkingParallelPair.zero) :
        Type v)),
    Eq (α := (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
      ((Hom.hom ((kernelCone g).π.app WalkingParallelPair.zero) :
            (a :
                (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero) :
                  Type v)) →
              (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
          x :
        (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
      ((Hom.hom
              ((LinearEquiv.toModuleIso
                      (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                        LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯)).symm.hom ≫
                (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero) :
            (a :
                (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero) :
                  Type v)) →
              (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
          x :
        (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
⊢ (kernelCone g).π.app WalkingParallelPair.zero =
    (LinearEquiv.toModuleIso
            (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯)).symm.hom ≫
      (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v))
one :
  ∀
    (x :
      (↑(Functor.obj (Functor.obj (Functor.const WalkingParallelPair) (kernelCone g).pt) WalkingParallelPair.one) :
        Type v)),
    Eq (α := (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
      ((Hom.hom ((kernelCone g).π.app WalkingParallelPair.one) :
            (a :
                (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one) : Type v)) →
              (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
          x :
        (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
      ((Hom.hom
              ((LinearEquiv.toModuleIso
                      (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                        LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯)).symm.hom ≫
                (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one) :
            (a :
                (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one) : Type v)) →
              (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
          x :
        (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
⊢ (kernelCone g).π.app WalkingParallelPair.one =
    (LinearEquiv.toModuleIso
            (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯)).symm.hom ≫
      (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v))
x :
  (↑(Functor.obj (Functor.obj (Functor.const WalkingParallelPair) (kernelCone g).pt) WalkingParallelPair.zero) : Type v)
⊢ Eq (α := (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
    ((Hom.hom ((kernelCone g).π.app WalkingParallelPair.zero) :
          (a : (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero) : Type v)) →
            (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
        x :
      (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
    ((Hom.hom
            ((LinearEquiv.toModuleIso
                    (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                      LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯)).symm.hom ≫
              (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero) :
          (a : (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero) : Type v)) →
            (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))
        x :
      (↑((parallelPair g 0).obj WalkingParallelPair.zero) : Type v))

Tactic:
simp [kernelCone]

Premises used: ModuleCat.kernelCone
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v))
x :
  (↑(Functor.obj (Functor.obj (Functor.const WalkingParallelPair) (kernelCone g).pt) WalkingParallelPair.one) : Type v)
⊢ Eq (α := (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
    ((Hom.hom ((kernelCone g).π.app WalkingParallelPair.one) :
          (a : (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one) : Type v)) →
            (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
        x :
      (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
    ((Hom.hom
            ((LinearEquiv.toModuleIso
                    (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                      LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯)).symm.hom ≫
              (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one) :
          (a : (↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one) : Type v)) →
            (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))
        x :
      (↑((parallelPair g 0).obj WalkingParallelPair.one) : Type v))

Tactic:
simp [kernelCone]

Premises used: ModuleCat.kernelCone
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
⊢ Epi (↟(Hom.hom f).range.mkQ)

Tactic:
haveI : Epi (ofHom f.hom.range.mkQ) :=
      (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
this : Epi (↟(Hom.hom f).range.mkQ)
apply :
  ↟(Hom.hom f).range.mkQ ≫ m =
    ↟(Hom.hom f).range.mkQ ≫ (fun (s : Cofork f 0) ↦ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)) s
⊢ m = (fun (s : Cofork f 0) ↦ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)) s

Tactic:
apply (cancel_epi (ofHom f.hom.range.mkQ)).1

Premises used: LinearMap.range, Iff.mp, Submodule.mkQ, ModuleCat.ofHom, ModuleCat.Hom.hom, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
this : Epi (↟(Hom.hom f).range.mkQ)
⊢ ↟(Hom.hom f).range.mkQ ≫ m =
    ↟(Hom.hom f).range.mkQ ≫ (fun (s : Cofork f 0) ↦ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)) s

Tactic:
h

Premises used: Quotient.liftOn', AddCon.liftOn, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
this : Epi (↟(Hom.hom f).range.mkQ)
⊢ ↟(Hom.hom f).range.mkQ ≫ m =
    ↟(Hom.hom f).range.mkQ ≫ (fun (s : Cofork f 0) ↦ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)) s

Tactic:
exact h
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
hf :
  ∀ (x : (↑M : Type v)),
    Eq (α := (↑P : Type v)) ((Hom.hom (f ≫ g) : (a : (↑M : Type v)) → (↑P : Type v)) x : (↑P : Type v))
      ((Hom.hom 0 : (a : (↑M : Type v)) → (↑P : Type v)) x : (↑P : Type v))
⊢ f ≫ g = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
x : (↑M : Type v)
⊢ Eq (α := (↑P : Type v)) ((Hom.hom (f ≫ g) : (a : (↑M : Type v)) → (↑P : Type v)) x : (↑P : Type v))
    ((Hom.hom 0 : (a : (↑M : Type v)) → (↑P : Type v)) x : (↑P : Type v))

Tactic:
H.apply_apply_eq_zero _

Premises used: Function.Exact.apply_apply_eq_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
x : (↑M : Type v)
⊢ Eq (α := (↑P : Type v)) ((Hom.hom (f ≫ g) : (a : (↑M : Type v)) → (↑P : Type v)) x : (↑P : Type v))
    ((Hom.hom 0 : (a : (↑M : Type v)) → (↑P : Type v)) x : (↑P : Type v))

Tactic:
exact H.apply_apply_eq_zero _

Premises used: Function.Exact.apply_apply_eq_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
refine :
  ∀ (j : WalkingParallelPair),
    (cokernelCocone f).ι.app j ≫
        (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
            ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
      (CokernelCofork.ofπ g ⋯).ι.app j
⊢ IsColimit (CokernelCofork.ofπ g ⋯)

Tactic:
refine IsColimit.ofIsoColimit (ModuleCat.cokernelIsColimit f) <|
    Cocone.ext (((Submodule.quotEquivOfEq _ _ (LinearMap.exact_iff.mp H)).toModuleIso).symm
    ≪≫ ((LinearMap.quotKerEquivOfSurjective _ H₂).toModuleIso)) ?_

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, ModuleCat.cokernelIsColimit, CategoryTheory.Iso.trans
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
zero :
  ∀ (x : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)),
    Eq (α := (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
      ((Hom.hom
              ((cokernelCocone f).ι.app WalkingParallelPair.zero ≫
                (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
                    ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom) :
            (a : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)) →
              (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
          x :
        (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
      ((Hom.hom ((CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero) :
            (a : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)) →
              (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
          x :
        (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
one :
  ∀ (x : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)),
    Eq (α := (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
      ((Hom.hom
              ((cokernelCocone f).ι.app WalkingParallelPair.one ≫
                (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
                    ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom) :
            (a : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)) →
              (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
          x :
        (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
      ((Hom.hom ((CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one) :
            (a : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)) →
              (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
          x :
        (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
x : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)
⊢ Eq (α := (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
    ((Hom.hom
            ((cokernelCocone f).ι.app WalkingParallelPair.zero ≫
              (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
                  ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)) → (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
    ((Hom.hom ((CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)) → (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g ⋯).pt : Type v))

Tactic:
simpa using (Function.Exact.apply_apply_eq_zero H x).symm

Premises used: Function.Exact.apply_apply_eq_zero, Eq.symm
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f_1 f : M ⟶ N
g : N ⟶ P
H :
  Function.Exact (M := (↑M : Type v)) (N := (↑N : Type v)) (P := (↑P : Type v))
    (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
H₂ : Function.Surjective (α := (↑N : Type v)) (β := (↑P : Type v)) (⇑(Hom.hom g) : (a : (↑N : Type v)) → (↑P : Type v))
x : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)
⊢ Eq (α := (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
    ((Hom.hom
            ((cokernelCocone f).ι.app WalkingParallelPair.one ≫
              (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
                  ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)) → (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
    ((Hom.hom ((CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)) → (↑(CokernelCofork.ofπ g ⋯).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g ⋯).pt : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
⊢ HasKernels (ModuleCat.{u_1, u} R)

Tactic:
⟨fun f => HasLimit.mk ⟨_, kernelIsLimit f⟩⟩

Premises used: CategoryTheory.Limits.HasKernels.mk, CategoryTheory.Limits.HasLimit.mk, ModuleCat.kernelIsLimit, ModuleCat.kernelCone, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
⊢ HasCokernels (ModuleCat.{u_1, u} R)

Tactic:
⟨fun f => HasColimit.mk ⟨_, cokernelIsColimit f⟩⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.HasCokernels.mk, CategoryTheory.Limits.ColimitCocone.mk, ModuleCat.cokernelIsColimit, ModuleCat.cokernelCocone
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ (kernelIsoKer f).inv ≫ kernel.ι f = ↟(Hom.hom f).ker.subtype

Tactic:
limit.isoLimitCone_inv_π _ _

Premises used: CategoryTheory.Limits.limit.isoLimitCone_inv_π
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ (kernelIsoKer f).hom ≫ ↟(Hom.hom f).ker.subtype = kernel.ι f

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ cokernel.π f ≫ (cokernelIsoRangeQuotient f).hom = ↟(Hom.hom f).range.mkQ

Tactic:
colimit.isoColimitCocone_ι_hom _ _

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ ↟(Hom.hom f).range.mkQ ≫ (cokernelIsoRangeQuotient f).inv = cokernel.π f

Tactic:
colimit.isoColimitCocone_ι_inv ⟨_, cokernelIsColimit f⟩ WalkingParallelPair.one

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.ColimitCocone.mk, ModuleCat.cokernelIsColimit
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N : ModuleCat R
f : M ⟶ N
x y : (↑N : Type u)
m : (↑M : Type u)
w :
  x =
    HAdd.hAdd (β := (↑N : Type u)) y
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑M : Type u)) → (↑N : Type u))
          m :
        (↑N : Type u))
subst :
  Eq (α := (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        (HAdd.hAdd (β := (↑N : Type u)) y
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
                  f :
                (a : (↑M : Type u)) → (↑N : Type u))
              m :
            (↑N : Type u))) :
      (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        y :
      (↑(cokernel f) : Type u))
⊢ Eq (α := (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        x :
      (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        y :
      (↑(cokernel f) : Type u))

Tactic:
subst w
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N : ModuleCat R
f : M ⟶ N
y : (↑N : Type u)
m : (↑M : Type u)
⊢ Eq (α := (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        (HAdd.hAdd (β := (↑N : Type u)) y
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
                  f :
                (a : (↑M : Type u)) → (↑N : Type u))
              m :
            (↑N : Type u))) :
      (↑(cokernel f) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            cokernel f) (cokernel.π f) :
          (a : (↑N : Type u)) → (↑(cokernel f) : Type u))
        y :
      (↑(cokernel f) : Type u))

Tactic:
simpa only [map_add, add_eq_left] using cokernel.condition_apply f m

Premises used: map_add, add_eq_left, CategoryTheory.Limits.cokernel.condition_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution
Goal:
R : Type u
inst : Ring R
X : Type u
M N : ModuleCat R
f : Functor.obj (free R) X ⟶ N
p : M ⟶ N
hp : Epi p
⊢ Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) p) :
      (a : (↑M : Type u)) → (↑N : Type u))

Tactic:
rw [epi_iff_surjective] at hp

Premises used: ModuleCat.epi_iff_surjective