awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ⋯
x s : P.Ring
hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)
rw :
  ((↑(AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) : P.Ring →+* T) :
        (a : P.Ring) → T)
      x =
    HMul.hMul (α := T)
      (((↑(AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) : P.Ring →+* T) :
            (a : P.Ring) → T)
          (↑(Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s ⋯) : P.Ring) :
        T)
      (IsLocalization.mk'.{u_2, u_3} (R := S) (M := M) T ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ M) ((algebraMap P.Ring S : (a : P.Ring) → S) s) hs : ↥M))
⊢ (IsLocalization.lift (R := P.Ring) (M := M') (g :=
          (↑(AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) : P.Ring →+* T)) ⋯ :
        (a : Localization M') → T)
      (IsLocalization.mk' (M := M') (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s ⋯)) =
    IsLocalization.mk'.{u_2, u_3} (R := S) (M := M) T ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
      (Subtype.mk (p := fun (x : S) ↦ x ∈ M) ((algebraMap P.Ring S : (a : P.Ring) → S) s) hs : ↥M)

Tactic:
rw [IsLocalization.lift_mk'_spec]

Premises used: IsLocalization.lift_mk'_spec
-- 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)) ⋯
x s : P.Ring
hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)
⊢ ((↑(AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) : P.Ring →+* T) :
        (a : P.Ring) → T)
      x =
    HMul.hMul (α := T)
      (((↑(AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) : P.Ring →+* T) :
            (a : P.Ring) → T)
          (↑(Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s ⋯) : P.Ring) :
        T)
      (IsLocalization.mk'.{u_2, u_3} (R := S) (M := M) T ((algebraMap P.Ring S : (a : P.Ring) → S) x : S)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ M) ((algebraMap P.Ring S : (a : P.Ring) → S) s) hs : ↥M))

Tactic:
simp
-- 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 := ⋯ }
⊢ FormallySmooth R P.Ring

Tactic:
haveI : FormallySmooth R P.Ring := inferInstanceAs (FormallySmooth R (MvPolynomial _ _))
-- 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 : FormallySmooth R P.Ring
⊢ FormallySmooth P.Ring (Localization M')

Tactic:
haveI : FormallySmooth P.Ring (Localization M') := .of_isLocalization M'
-- 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 : FormallySmooth P.Ring (Localization M')
⊢ FormallySmooth R Q.Ring

Tactic:
haveI : FormallySmooth R Q.Ring := .comp R P.Ring (Localization M')
-- 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 : FormallySmooth R Q.Ring
⊢ Module.Flat S T

Tactic:
haveI : Module.Flat S T := IsLocalization.flat T M
-- 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 : Algebra (Localization M') T := fQ.toAlgebra
⊢ IsScalarTower P.Ring S T

Tactic:
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
-- 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 : IsScalarTower P.Ring S T
⊢ IsScalarTower P.Ring (Localization M') T

Tactic:
haveI : IsScalarTower P.Ring (Localization M') T :=
    .of_algebraMap_eq fun r ↦ (f.algebraMap_toRingHom r).symm
-- 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 : IsScalarTower P.Ring (Localization M') T
rw : IsLocalization (algebraMapSubmonoid S M') T
⊢ IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))

Tactic:
rw [isLocalizedModule_iff_isLocalization]

Premises used: isLocalizedModule_iff_isLocalization
-- 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 : IsScalarTower P.Ring (Localization M') T
h : algebraMapSubmonoid S M' = M
⊢ IsLocalization (algebraMapSubmonoid S M') T

Tactic:
convert! ‹IsLocalization M T› using 1

Premises used: IsLocalization
-- 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 : IsScalarTower P.Ring (Localization M') T
⊢ algebraMapSubmonoid S M' = M

Tactic:
Submonoid.map_comap_eq_of_surjective P.algebraMap_surjective _

Premises used: Algebra.Extension.algebraMap_surjective, Algebra.algebraMapSubmonoid, Submonoid.map_comap_eq_of_surjective
-- 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 : IsScalarTower P.Ring (Localization M') T
⊢ algebraMapSubmonoid S M' = M

Tactic:
exact Submonoid.map_comap_eq_of_surjective P.algebraMap_surjective _

Premises used: Algebra.Extension.algebraMap_surjective, Submonoid.map_comap_eq_of_surjective
-- 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 : IsScalarTower P.Ring (Localization M') T
⊢ IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))

Tactic:
haveI : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap := by
    rw [isLocalizedModule_iff_isLocalization]
    convert! ‹IsLocalization M T› using 1
    exact Submonoid.map_comap_eq_of_surjective P.algebraMap_surjective _
-- 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))
refine_1 : f.toRingHom.FormallyEtale
refine_2 :
  Function.Bijective (α :=
    Q.Ring ⊗[Extension.Ring (Generators.toExtension (Generators.self R S))]
      ↥(Extension.ker (Generators.toExtension (Generators.self R S))))
    (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer ⋯)) :
      (a : Q.Ring ⊗[(Generators.self R S).toExtension.Ring] ↥(Generators.self R S).toExtension.ker) → ↥Q.ker)
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T

Tactic:
refine Extension.tensorH1CotangentOfFormallyEtale f rfl ?_ ?_ ≪≫ₗ
      Extension.equivH1CotangentOfFormallySmooth _

Premises used: Algebra.Extension.tensorH1CotangentOfFormallyEtale, Algebra.Extension.equivH1CotangentOfFormallySmooth, rfl
-- 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.toRingHom.FormallyEtale

Tactic:
RingHom.formallyEtale_algebraMap.mpr
      (FormallyEtale.of_isLocalization (M := M') (Rₘ := Localization M'))

Premises used: Iff.mpr, Algebra.FormallyEtale.of_isLocalization, RingHom.formallyEtale_algebraMap
-- 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.toRingHom.FormallyEtale

Tactic:
exact RingHom.formallyEtale_algebraMap.mpr
      (FormallyEtale.of_isLocalization (M := M') (Rₘ := Localization M'))

Premises used: Iff.mpr, Algebra.FormallyEtale.of_isLocalization, RingHom.formallyEtale_algebraMap
-- 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 ⋯
⊢ Function.Bijective (α :=
    Q.Ring ⊗[Extension.Ring (Generators.toExtension (Generators.self R S))]
      ↥(Extension.ker (Generators.toExtension (Generators.self R S))))
    (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer ⋯)) :
      (a : Q.Ring ⊗[(Generators.self R S).toExtension.Ring] ↥(Generators.self R S).toExtension.ker) → ↥Q.ker)

Tactic:
(isLocalizedModule_iff_isBaseChange M' (Localization M') F).mp ?_

Premises used: isLocalizedModule_iff_isBaseChange, Set.Mem, OreLocalization, Localization, IsLocalization.lift, IsTensorProduct, Quotient, IsBaseChange, Ideal.comap, Iff.mp, IsLocalization.liftAlgHom, RingHom.ker