Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁹ : FormallySmooth R P.Ring
this✝⁸ : FormallySmooth P.Ring (Localization M')
this✝⁷ : FormallySmooth R Q.Ring
this✝⁶ : Module.Flat S T
this✝⁵ : Algebra P.Ring Q.Ring := inferInstance
this✝⁴ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝³ : Algebra (Localization M') T := fQ.toAlgebra
this✝² : IsScalarTower P.Ring S T
this✝¹ : IsScalarTower P.Ring (Localization M') T
this✝ : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
⊢ IsLocalizedModule M' F

Tactic:
have : F = ((LinearEquiv.ofEq _ _ this).restrictScalars P.Ring).toLinearMap ∘ₗ
      P.ker.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) := by
      ext; rfl

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝¹⁰ : FormallySmooth R P.Ring
this✝⁹ : FormallySmooth P.Ring (Localization M')
this✝⁸ : FormallySmooth R Q.Ring
this✝⁷ : Module.Flat S T
this✝⁶ : Algebra P.Ring Q.Ring := inferInstance
this✝⁵ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝⁴ : Algebra (Localization M') T := fQ.toAlgebra
this✝³ : IsScalarTower P.Ring S T
this✝² : IsScalarTower P.Ring (Localization M') T
this✝¹ : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
this✝ :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (Algebra.linearMap P.Ring S).ker =
    RingHom.ker fQ
this :
  F =
    ↑(LinearEquiv.restrictScalars P.Ring
          (LinearEquiv.ofEq
            (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker)
            (RingHom.ker fQ) this✝)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
⊢ IsLocalizedModule M' F