-- Mathlib/RingTheory/LocalRing/Module.lean
theorem free_of_lTensor_residueField_injective (hg : Surjective g) (h : Exact f g)
    [Module.Finite R M] [Module.Finite R N] [Module.Free R N]
    (hf : Function.Injective (f.lTensor k)) :
    Module.Free R P

Proof state:
case H
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.lTensor P (Submodule.subtype 𝔪))

Tactic:
apply lTensor_injective_of_exact_of_exact_of_rTensor_injective
  h hg (LinearMap.exact_subtype_mkQ 𝔪) (Submodule.mkQ_surjective _)
  ((LinearMap.lTensor_inj_iff_rTensor_inj _ _).mp hf)
  (Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective)

Result:
no goals

Proof state:
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ Free R P

Tactic:
have := Module.finitePresentation_of_free_of_surjective g hg
  (by rw [h.linearMap_ker_eq, LinearMap.range_eq_map]; exact (Module.Finite.fg_top).map f)

Result:
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Free R P

Proof state:
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ (LinearMap.ker g).FG

Tactic:
rw [h.linearMap_ker_eq, LinearMap.range_eq_map]

Result:
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ (Submodule.map f ⊤).FG

Proof state:
case H
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.rTensor P (Submodule.subtype 𝔪))

Tactic:
rw [← LinearMap.lTensor_inj_iff_rTensor_inj]

Result:
case H
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.lTensor P (Submodule.subtype 𝔪))

Proof state:
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Free R P

Tactic:
apply free_of_maximalIdeal_rTensor_injective

Result:
case H
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
this : FinitePresentation R P
⊢ Function.Injective ⇑(LinearMap.rTensor P (Submodule.subtype 𝔪))

Proof state:
R : Type u_3
inst✝¹⁰ : CommRing R
M : Type u_4
N : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
P : Type u_2
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ (Submodule.map f ⊤).FG

Tactic:
exact (Module.Finite.fg_top).map f

Result:
no goals