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 ⋯
⊢ IsLocalizedModule M' F

Tactic:
have : (LinearMap.ker <| Algebra.linearMap P.Ring S).localized' (Localization M') M'
        (Algebra.linearMap P.Ring (Localization M')) = RingHom.ker fQ := by
      rw [LinearMap.localized'_ker_eq_ker_localizedMap (Localization M') M'
        (Algebra.linearMap P.Ring (Localization M'))
        (f' := (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)]
      ext x
      obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M' x
      simp only [LinearMap.mem_ker, LinearMap.extendScalarsOfIsLocalization_apply', RingHom.mem_ker,
        IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe, IsLocalization.lift_mk'_spec,
        RingHom.coe_coe, AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
        mul_zero, fQ]
      have : IsLocalization.mk' (Localization M') x ⟨s, hs⟩ =
          IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩ := by
        rw [IsLocalization.mk'_eq_iff_eq_mul, mul_comm, ← Algebra.smul_def, ← Submonoid.smul_def,
          IsLocalizedModule.mk'_cancel']
        rfl
      simp [this, ← IsScalarTower.algebraMap_apply]

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
⊢ IsLocalizedModule M' F