-- Mathlib/Algebra/Category/ModuleCat/Injective.lean
theorem injective_module_of_injective_object
    [inj : CategoryTheory.Injective <| ModuleCat.of R M] :
    Module.Injective R M where
  out X Y _ _ _ _ f hf g

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Proof state:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
this : Mono (ModuleCat.ofHom f)
l : ModuleCat.of R Y ⟶ ModuleCat.of R M
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l))
⊢ ∃ h, ∀ (x : X), h (f x) = (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l)) x

Tactic:
exact ⟨l.hom, fun _ => rfl⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
obtain ⟨l, h⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)

Result:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
l : ModuleCat.of R Y ⟶ ModuleCat.of R M
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom g
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Proof state:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
this : Mono (ModuleCat.ofHom f)
l : ModuleCat.of R Y ⟶ ModuleCat.of R M
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom g
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
obtain rfl := ModuleCat.hom_ext_iff.mp h

Result:
case intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
this : Mono (ModuleCat.ofHom f)
l : ModuleCat.of R Y ⟶ ModuleCat.of R M
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l))
⊢ ∃ h, ∀ (x : X), h (f x) = (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l)) x