-- Module: Mathlib.RingTheory.Etale.Kaehler
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
M : Submonoid S
inst_7 : IsLocalization M T
P : Extension R S := Generators.toExtension (Generators.self R S)
M' : Submonoid P.Ring := Submonoid.comap (F := P.Ring →+* S) (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T :=
  IsLocalization.liftAlgHom (R := P.Ring) (M := M') (f :=
    AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this_1 : FormallySmooth R P.Ring
this_2 : FormallySmooth P.Ring (Localization M')
this_3 : FormallySmooth R Q.Ring
this_4 : Module.Flat S T
this_5 : Algebra P.Ring Q.Ring := inferInstance
this_6 : Algebra P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_7 : Algebra (Localization M') T := fQ.toAlgebra
this_8 : IsScalarTower P.Ring S T
this_9 : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
F : LinearMap (R := P.Ring) (RingHom.id P.Ring) ↥P.ker ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
h :
  Eq.{u_3 + 1} (α := T)
      ((((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
                    (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T)) :
                  (a : P.Ring →ₗ[P.Ring] S) → Localization M' →ₗ[P.Ring] T)
                (Algebra.linearMap P.Ring S) :
              LinearMap (R := P.Ring) (RingHom.id P.Ring) (Localization M') T) :
            (a : Localization M') → T)
          (IsLocalization.mk' (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs)) :
        T)
      (0 : T) ↔
    Eq.{u_3 + 1} (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap P.Ring S : (a : P.Ring) → S) x : S) : T) (0 : T)
⊢ Membership.mem (γ := Ideal (Localization M'))
      (LinearMap.ker (M₂ := T)
        (LinearMap.extendScalarsOfIsLocalization M' (Localization M')
          ((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
                (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T)) :
              (a : P.Ring →ₗ[P.Ring] S) → Localization M' →ₗ[P.Ring] T)
            (Algebra.linearMap P.Ring S))))
      (IsLocalization.mk' (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs)) ↔
    Membership.mem (γ := Ideal (Localization M')) (RingHom.ker fQ)
      (IsLocalization.mk' (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs))

Tactic:
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]

Premises used: IsLocalization.lift_mk'_spec, IsScalarTower.coe_toAlgHom', RingHom.coe_coe, IsLocalization.coe_liftAlgHom, RingHom.mem_ker, MulZeroClass.mul_zero, LinearMap.mem_ker, AlgHom.coe_comp, AlgHom.toRingHom_eq_coe, Function.comp_apply, LinearMap.extendScalarsOfIsLocalization_apply'