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)) ⋯
x s : P.Ring
hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)
⊢ ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a =
      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)
have refine : (fQ : (a : Localization M') → T)
    (IsLocalization.mk' (M := M') (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s sorry)) =
  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: refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
-- 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)) ⋯
x s : P.Ring
hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)
⊢ (fQ : (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)
have simp : (IsLocalization.lift (R := P.Ring) (M := M') (g :=
        (↑(AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) : P.Ring →+* T)) sorry :
      (a : Localization M') → T)
    (IsLocalization.mk' (M := M') (Localization M') x (Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') s sorry)) =
  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 only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]
-- 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)) ⋯
x s : P.Ring
hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)
⊢ (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)
have 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 sorry) : 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: rw [IsLocalization.lift_mk'_spec]
-- 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 := ⋯ }
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this : FormallySmooth R P.Ring
Tactic: haveI : FormallySmooth R P.Ring := inferInstanceAs (FormallySmooth R (MvPolynomial _ _))
-- 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 : FormallySmooth R P.Ring
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this₁ : FormallySmooth P.Ring (Localization M')
Tactic: haveI : FormallySmooth P.Ring (Localization M') := .of_isLocalization M'
-- 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 : FormallySmooth P.Ring (Localization M')
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this₁ : FormallySmooth R Q.Ring
Tactic: haveI : FormallySmooth R Q.Ring := .comp R P.Ring (Localization M')
-- 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 : FormallySmooth R Q.Ring
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this₁ : Module.Flat S T
Tactic: haveI : Module.Flat S T := IsLocalization.flat T M
-- 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 : Algebra (Localization M') T := fQ.toAlgebra
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this₁ : IsScalarTower P.Ring S T
Tactic: haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' 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 : IsScalarTower P.Ring S T
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this₁ : IsScalarTower P.Ring (Localization M') T
Tactic: haveI : IsScalarTower P.Ring (Localization M') T :=
    .of_algebraMap_eq fun r ↦ (f.algebraMap_toRingHom r).symm
-- 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 : IsScalarTower P.Ring (Localization M') T
⊢ IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
have rw : IsLocalization (algebraMapSubmonoid S M') T
Tactic: rw [isLocalizedModule_iff_isLocalization]
-- 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 : IsScalarTower P.Ring (Localization M') T
⊢ IsLocalization (algebraMapSubmonoid S M') T
have h : algebraMapSubmonoid S M' = M
Tactic: convert! ‹IsLocalization M T› using 1
-- 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 : IsScalarTower P.Ring (Localization M') T
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have this₁ : 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 _
-- 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))
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have refine_1 : f.toRingHom.FormallyEtale
Tactic: refine Extension.tensorH1CotangentOfFormallyEtale f rfl ?_ ?_ ≪≫ₗ
      Extension.equivH1CotangentOfFormallySmooth _
-- 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))
refine_1 : f.toRingHom.FormallyEtale
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
have 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 sorry)) :
    (a : Q.Ring ⊗[(Generators.self R S).toExtension.Ring] ↥(Generators.self R S).toExtension.ker) → ↥Q.ker)
Tactic: refine Extension.tensorH1CotangentOfFormallyEtale f rfl ?_ ?_ ≪≫ₗ
      Extension.equivH1CotangentOfFormallySmooth _
-- 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 ⋯
⊢ 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)
have refine_2 : IsLocalizedModule M' F
Tactic: refine (isLocalizedModule_iff_isBaseChange M' (Localization M') F).mp ?_
-- 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 ⋯
⊢ Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
have rw : 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
Tactic: rw [LinearMap.localized'_ker_eq_ker_localizedMap (Localization M') M'
        (Algebra.linearMap P.Ring (Localization M'))
        (f' := (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)]