awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
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 ⋯
⊢ 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))) =
    RingHom.ker fQ
have h : ∀ (x : Localization M'),
  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))))
      x ↔
    Membership.mem (γ := Ideal (Localization M')) (RingHom.ker fQ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
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 : Localization M'
⊢ 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))))
      x ↔
    Membership.mem (γ := Ideal (Localization M')) (RingHom.ker fQ) x
have h : ∀ (x s : P.Ring) (hs : s ∈ M'),
  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: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M' x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
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'
⊢ 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
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'
⊢ Eq (α := Localization M') (IsLocalization.mk' (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs))
    (IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x
      (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs))
have rw : Eq (α := Localization M') ((algebraMap P.Ring (Localization M') : (a : P.Ring) → Localization M') x : Localization M')
  ((Algebra.linearMap P.Ring (Localization M') : (a : P.Ring) → Localization M') x : Localization M')
Tactic: rw [IsLocalization.mk'_eq_iff_eq_mul, mul_comm, ← Algebra.smul_def, ← Submonoid.smul_def,
          IsLocalizedModule.mk'_cancel']
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
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'
⊢ 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)
have this₁ : Eq (α := Localization M') (IsLocalization.mk' (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs))
  (IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x
    (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s hs))
Tactic: 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
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
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 ⋯
⊢ IsLocalizedModule M' F
have this₁ : Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
    (LinearMap.ker (Algebra.linearMap P.Ring S)) =
  RingHom.ker fQ
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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
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_10 : 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 ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
⊢ F =
    (↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
have h : ∀ (x : ↥P.ker),
  Eq (α := Localization M') (↑((F : (a : ↥P.ker) → ↥(RingHom.ker fQ)) x) : Localization M')
    (↑(((↑(LinearEquiv.restrictScalars P.Ring
                    (LinearEquiv.ofEq
                      (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                        (LinearMap.ker (Algebra.linearMap P.Ring S)))
                      (RingHom.ker fQ) this)) :
                ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                      (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
                  ↥(RingHom.ker fQ)) ∘ₗ
              Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker :
            (a : ↥P.ker) → ↥(RingHom.ker fQ))
          x) :
      Localization M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (hypothesis)
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_10 : 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 ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
⊢ IsLocalizedModule M' F
have this₁ : F =
  (↑(LinearEquiv.restrictScalars P.Ring
          (LinearEquiv.ofEq
            (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (LinearMap.ker (Algebra.linearMap P.Ring S)))
            (RingHom.ker fQ) this)) :
      ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
            (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
        ↥(RingHom.ker fQ)) ∘ₗ
    Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
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
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
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_10 : 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 ⋯
this_11 :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
this :
  F =
    (↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
⊢ IsLocalizedModule M' F
have refine_2 : IsLocalizedModule M'
  ((↑(LinearEquiv.restrictScalars P.Ring
          (LinearEquiv.ofEq
            (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (LinearMap.ker (Algebra.linearMap P.Ring S)))
            (RingHom.ker fQ) this_11)) :
      ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
            (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
        ↥(RingHom.ker fQ)) ∘ₗ
    Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)
Tactic: rw [this]