awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
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
a :
  (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))
⊢ Eq (α := (↑H : Type v))
    ((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)) :
      (↑H : Type v))
    ((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))
        (HSMul.hSMul (α := R) (β := (↑F'.1 : 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 :
                (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))

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
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
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)))
            ⋯) :
        (↑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))
⊢ (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))

Tactic:
change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.e, CategoryTheory.Limits.MonoFactorisation.m, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
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
a : (↑(c • x) : (↑H : Type v)) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (↑x : (↑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 = (↑(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))

Tactic:
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
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
⊢ (↑(c • x) : (↑H : Type v)) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (↑x : (↑H : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
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))
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type v)
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)))
              ⋯) :
          (↑G : Type v)) :
      (↑H : Type v))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x : (↑H : 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:
change (F'.e ≫ F'.m) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.e, CategoryTheory.Limits.MonoFactorisation.m, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type v)
hf : (↑x : (↑H : Type v)) = (Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x
⊢ 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))

Tactic:
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, Classical.indefiniteDescription, Subtype.property
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type v)
⊢ (↑x : (↑H : Type v)) = (Hom.hom (ι f) : (a : (↑(image f) : Type v)) → (↑H : Type v)) x

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ (imageIsoRange f).inv ≫ Limits.image.ι f = ↟(Hom.hom f).range.subtype

Tactic:
IsImage.isoExt_inv_m _ _

Premises used: Set.Mem, CategoryTheory.Limits.IsImage.isoExt_inv_m, ModuleCat.image, ModuleCat.image.ι
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
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
rw₁ rw₂ : Eq (α := Limits.image f ⟶ of R (↑H : Type v)) (Limits.image.ι f) (Limits.image.ι f)
⊢ (imageIsoRange f).hom ≫ ↟(Hom.hom f).range.subtype = Limits.image.ι f

Tactic:
rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]

Premises used: ModuleCat.imageIsoRange_inv_image_ι, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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)
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))
⊢ f ≫ ModuleCat.ofHom l = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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)
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:
simpa using h x
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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
⊢ Mono (ModuleCat.ofHom f)

Tactic:
have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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)
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)
⊢ ∃ (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)

Premises used: ModuleCat.ofHom, CategoryTheory.Injective.factors
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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
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)
⊢ ∃ (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 rfl := ModuleCat.hom_ext_iff.mp h

Premises used: ModuleCat.hom_ext_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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)
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 (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:
⟨l.hom, fun _ => rfl⟩

Premises used: Exists.intro, ModuleCat.Hom.hom, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
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)
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 (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:
exact ⟨l.hom, fun _ => rfl⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Injective R M ↔ CategoryTheory.Injective (C := ModuleCat.{v, u} R) (ModuleCat.of R M)

Tactic:
⟨fun _ => injective_object_of_injective_module R M,
   fun _ => injective_module_of_injective_object R M⟩

Premises used: Module.injective_module_of_injective_object, Iff.intro, Module.injective_object_of_injective_module
-- Module: Mathlib.Algebra.Category.ModuleCat.Injective
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v, u} R
inst_4 : Injective (C := ModuleCat.{v, u} R) (of R M)
⊢ Injective (C := ModuleCat R) (of R (ULift.{v', v} M))

Tactic:
Module.injective_object_of_injective_module
    (inj := Module.ulift_injective_of_injective
      (inj := Module.injective_module_of_injective_object _ _))

Premises used: Module.injective_object_of_injective_module
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
⊢ ↟(Hom.hom f).ker.subtype ≫ f = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
Goal:
R : Type u
inst : Ring R
M N P : ModuleCat.{v, u} R
f : M ⟶ N
s : Fork f 0
c : (↑s.1 : Type v)
⊢ Eq (α := (↑N : Type v))
    ((Hom.hom f : (a : (↑M : Type v)) → (↑N : Type v))
        ((Hom.hom s.ι : (a : (↑s.1 : Type v)) → (↑M : Type v)) c : (↑M : Type v)) :
      (↑N : Type v))
    (0 : (↑N : Type v))

Tactic:
simp [← ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
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)
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) ⋯)) :
          (a : (↑s.pt : Type v)) → (↑(kernelCone f).pt : Type v))
        x :
      (↑(kernelCone f).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))

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Category.ModuleCat.Kernels
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 (α := ↥(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) ⋯)) :
          (a : (↑s.pt : Type v)) → (↑(kernelCone f).pt : Type v))
        x :
      (↑(kernelCone f).pt : Type v))

Tactic:
rfl
-- 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))
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.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : 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.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : 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.Injective (α := (↑M : Type v)) (β := (↑N : Type v)) (⇑(Hom.hom f) : (a : (↑M : Type v)) → (↑N : Type v))
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 ⋯)).symm.hom ≫
        (KernelFork.ofι f ⋯).π.app j
⊢ IsLimit (KernelFork.ofι f ⋯)

Tactic:
refine IsLimit.ofIsoLimit (kernelIsLimit g) <|
    Cone.ext ((LinearEquiv.ofInjective _ H₂).trans
        (LinearEquiv.ofEq _ _ (LinearMap.exact_iff.mp H).symm)).toModuleIso.symm ?_

Premises used: ModuleCat.kernelIsLimit, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.Cone.ext