-- Mathlib/RingTheory/Localization/Algebra.lean
/-- The canonical linear map from the kernel of `g` to the kernel of its localization
is localizing. In other words, localization commutes with taking kernels. -/
lemma RingHom.toKerIsLocalization_isLocalizedModule (hT : Submonoid.map g M = T) :
    IsLocalizedModule M (toKerIsLocalization S Q g (hT.symm ▸ Submonoid.le_comap_map M))

Proof state:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (↑(LinearEquiv.restrictScalars R e) ∘ₗ Algebra.idealMap S (ker g))

Tactic:
apply IsLocalizedModule.of_linearEquiv

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
⊢ IsLocalizedModule M (toKerIsLocalization S Q g ⋯)

Tactic:
let e := LinearEquiv.ofEq _ _ (IsLocalization.ker_map (S := S) Q g hT).symm

Result:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (toKerIsLocalization S Q g ⋯)

Proof state:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (toKerIsLocalization S Q g ⋯)

Tactic:
convert_to IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ
  Algebra.idealMap S (RingHom.ker g))

Result:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (↑(LinearEquiv.restrictScalars R e) ∘ₗ Algebra.idealMap S (ker g))