awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          F'.m :
        (a : (↑F'.I : Type v)) → (↑H : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) F'.e :
            (a : (↑G : Type v)) → (↑F'.I : Type v))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type v)) ↦
                  (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(c • x) : (↑H : Type v)))
                ⋯) :
            (↑G : Type v)) :
        (↑F'.I : Type v)) =
    HSMul.hSMul (α := R) (β := (↑H : Type v)) ((RingHom.id R : (a : R) → R) c : R)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) F'.m :
            (a : (↑F'.I : Type v)) → (↑H : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  carrier) F'.e :
                (a : (↑G : Type v)) → (↑F'.I : Type v))
              (↑(Classical.indefiniteDescription
                    (fun (x_1 : (↑G : Type v)) ↦
                      (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                    ⋯) :
                (↑G : Type v)) :
            (↑F'.I : Type v)) :
        (↑H : Type v))
have a : (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
        (F'.e ≫ F'.m) :
      (a : (↑G : Type v)) → (↑H : Type v))
    (↑(Classical.indefiniteDescription
          (fun (x_1 : (↑G : Type v)) ↦
            (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(c • x) : (↑H : Type v)))
          sorry) :
      (↑G : Type v)) =
  HSMul.hSMul (α := R) (β := (↑H : Type v)) ((RingHom.id R : (a : R) → R) c : R)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (F'.e ≫ F'.m) :
          (a : (↑G : Type v)) → (↑H : Type v))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type v)) ↦ (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
              sorry) :
          (↑G : Type v)) :
      (↑H : Type v))
Tactic: change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type v)) → (↑H : Type v))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type v)) ↦
              (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(c • x) : (↑H : Type v)))
            ⋯) :
        (↑G : Type v)) =
    HSMul.hSMul (α := R) (β := (↑H : Type v)) ((RingHom.id R : (a : R) → R) c : R)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) (F'.e ≫ F'.m) :
            (a : (↑G : Type v)) → (↑H : Type v))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type v)) ↦
                  (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                ⋯) :
            (↑G : Type v)) :
        (↑H : Type v))
have a : (↑(c • x) : (↑H : Type v)) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (↑x : (↑H : Type v))
Tactic: simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
have hf : ∀ (x : (↑(image f) : Type v)),
  Eq (α := (↑H : Type v)) ((Hom.hom (lift F' ≫ F'.m) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : Type v))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type v)
⊢ Eq (α := (↑H : Type v)) ((Hom.hom (lift F' ≫ F'.m) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : Type v))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : Type v))
have hf : Eq (α := (↑H : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type v)) → (↑H : Type v))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type v)) ↦ (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
            sorry) :
        (↑G : Type v)) :
    (↑H : Type v))
  ((Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : Type v))
Tactic: change (F'.e ≫ F'.m) _ = _
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type v)
⊢ Eq (α := (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (F'.e ≫ F'.m) :
          (a : (↑G : Type v)) → (↑H : Type v))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type v)) ↦ (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
              ⋯) :
          (↑G : Type v)) :
      (↑H : Type v))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : Type v))
have hf : (↑x : (↑H : Type v)) = (Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x
Tactic: rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ↟(Hom.hom f).range.subtype = Limits.image.ι f
have rw : (imageIsoRange f).hom ≫ (imageIsoRange f).inv ≫ Limits.image.ι f = Limits.image.ι f
Tactic: rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
rw : (imageIsoRange f).hom ≫ (imageIsoRange f).inv ≫ Limits.image.ι f = Limits.image.ι f
⊢ (imageIsoRange f).hom ≫ ↟(Hom.hom f).range.subtype = Limits.image.ι f
have rw₁ : Eq (α := Limits.image f ⟶ of R (↑H : Type v)) (Limits.image.ι f) (Limits.image.ι f)
Tactic: rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Injective (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : Injective R M
X Y : ModuleCat.{v, u} R
g : X ⟶ ModuleCat.of R M
f : X ⟶ Y
m : Mono f
l : (↑Y : Type v) →ₗ[R] M
h :
  ∀ (x : (↑X : Type v)),
    Eq (α := M)
      ((l : (a : (↑Y : Type v)) → M) ((ModuleCat.Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v)) :
        M)
      ((ModuleCat.Hom.hom g : (a : (↑X : Type v)) → M) x : M)
⊢ f ≫ ModuleCat.ofHom l = g
have hf : ∀ (x : (↑X : Type v)),
  Eq (α := (↑(ModuleCat.of R M) : Type v))
    ((ModuleCat.Hom.hom (f ≫ ModuleCat.ofHom l) : (a : (↑X : Type v)) → (↑(ModuleCat.of R M) : Type v)) x :
      (↑(ModuleCat.of R M) : Type v))
    ((ModuleCat.Hom.hom g : (a : (↑X : Type v)) → (↑(ModuleCat.of R M) : Type v)) x : (↑(ModuleCat.of R M) : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Injective (hypothesis)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : CategoryTheory.Injective (C := ModuleCat.{v, u} R) (ModuleCat.of R M)
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
⊢ ∃ (h : Y →ₗ[R] M),
    ∀ (x_4 : X), Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)
have this : Mono (ModuleCat.ofHom f)
Tactic: have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Injective (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : CategoryTheory.Injective (C := ModuleCat.{v, u} R) (ModuleCat.of R M)
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
⊢ ∃ (h : Y →ₗ[R] M),
    ∀ (x_4 : X), Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)
have obtain : ∀ (l : Quiver.Hom (V := ModuleCat.{v, u} R) (ModuleCat.of R Y) (ModuleCat.of R M))
  (h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom g),
  ∃ (h : Y →ₗ[R] M),
    ∀ (x_4 : X), Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)
Tactic: obtain ⟨l, h⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Injective (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inj : CategoryTheory.Injective (C := ModuleCat.{v, u} R) (ModuleCat.of R M)
X Y : Type v
x : AddCommGroup X
x_1 : AddCommGroup Y
x_2 : Module R X
x_3 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y)
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
l : Quiver.Hom (V := ModuleCat.{v, u} R) (ModuleCat.of R Y) (ModuleCat.of R M)
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom g
⊢ ∃ (h : Y →ₗ[R] M),
    ∀ (x_4 : X), Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M) ((g : (a : X) → M) x_4 : M)
have obtain : ∀ (h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l))),
  ∃ (h : Y →ₗ[R] M),
    ∀ (x_4 : X),
      Eq (α := M) ((h : (a : Y) → M) ((f : (a : X) → Y) x_4 : Y) : M)
        ((ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l) : (a : X) → M) x_4 : M)
Tactic: obtain rfl := ModuleCat.hom_ext_iff.mp h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = s.ι
x : (↑s.pt : Type v)
⊢ Eq.{v + 1} (α := (↑M : Type v))
    (↑((Hom.hom m : (a : (↑s.pt : Type v)) → (↑(kernelCone f).pt : Type v)) x) : (↑M : Type v))
    (↑((Hom.hom ((fun (s : Fork f 0) ↦ ↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom s.ι) ⋯)) s) :
            (a : (↑s.pt : Type v)) → (↑(kernelCone f).pt : Type v))
          x) :
      (↑M : Type v))
have simp : Eq (α := ↥(Hom.hom f).ker)
  ((Hom.hom m : (a : (↑s.pt : Type v)) → (↑(kernelCone f).pt : Type v)) x : (↑(kernelCone f).pt : Type v))
  ((Hom.hom (↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom (Fork.ι (kernelCone f)) ∘ₗ Hom.hom m) sorry)) :
        (a : (↑s.pt : Type v)) → (↑(kernelCone f).pt : Type v))
      x :
    (↑(kernelCone f).pt : Type v))
Tactic: simp [← h]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ f ≫ g = 0
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ IsLimit (KernelFork.ofι f ⋯)
have refine : ∀ (j : WalkingParallelPair),
  (kernelCone g).π.app j =
    (LinearEquiv.toModuleIso
            (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker sorry)).symm.hom ≫
      (KernelFork.ofι f sorry).π.app j
Tactic: refine IsLimit.ofIsoLimit (kernelIsLimit g) <|
    Cone.ext ((LinearEquiv.ofInjective _ H₂).trans
        (LinearEquiv.ofEq _ _ (LinearMap.exact_iff.mp H).symm)).toModuleIso.symm ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ (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
have 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 sorry)).symm.hom ≫
              (KernelFork.ofι f sorry).π.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: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ (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
have 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 sorry)).symm.hom ≫
              (KernelFork.ofι f sorry).π.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: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (hypothesis)
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.π
⊢ m = (fun (s : Cofork f 0) ↦ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)) s
have this : Epi (↟(Hom.hom f).range.mkQ)
Tactic: haveI : Epi (ofHom f.hom.range.mkQ) :=
      (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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)
⊢ m = (fun (s : Cofork f 0) ↦ ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)) s
have 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.π) sorry)) s
Tactic: apply (cancel_epi (ofHom f.hom.range.mkQ)).1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ f ≫ g = 0
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ IsColimit (CokernelCofork.ofπ g ⋯)
have refine : ∀ (j : WalkingParallelPair),
  (cokernelCocone f).ι.app j ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range sorry).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g sorry).ι.app j
Tactic: refine IsColimit.ofIsoColimit (ModuleCat.cokernelIsColimit f) <|
    Cocone.ext (((Submodule.quotEquivOfEq _ _ (LinearMap.exact_iff.mp H)).toModuleIso).symm
    ≪≫ ((LinearMap.quotKerEquivOfSurjective _ H₂).toModuleIso)) ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ (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
have zero : ∀ (x : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)),
  Eq (α := (↑(CokernelCofork.ofπ g sorry).pt : Type v))
    ((Hom.hom
            ((cokernelCocone f).ι.app WalkingParallelPair.zero ≫
              (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range sorry).toModuleIso.symm ≪≫
                  ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)) → (↑(CokernelCofork.ofπ g sorry).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g sorry).pt : Type v))
    ((Hom.hom ((CokernelCofork.ofπ g sorry).ι.app WalkingParallelPair.zero) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.zero) : Type v)) → (↑(CokernelCofork.ofπ g sorry).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g sorry).pt : Type v))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Kernels (goal)
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))
⊢ (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
have one : ∀ (x : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)),
  Eq (α := (↑(CokernelCofork.ofπ g sorry).pt : Type v))
    ((Hom.hom
            ((cokernelCocone f).ι.app WalkingParallelPair.one ≫
              (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range sorry).toModuleIso.symm ≪≫
                  ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)) → (↑(CokernelCofork.ofπ g sorry).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g sorry).pt : Type v))
    ((Hom.hom ((CokernelCofork.ofπ g sorry).ι.app WalkingParallelPair.one) :
          (a : (↑((parallelPair f 0).obj WalkingParallelPair.one) : Type v)) → (↑(CokernelCofork.ofπ g sorry).pt : Type v))
        x :
      (↑(CokernelCofork.ofπ g sorry).pt : Type v))
Tactic: ext x