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
⊢ Eq (α := T ⊗[S] H1Cotangent R S →ₗ[T] H1Cotangent R T)
    (↑(tensorH1CotangentOfIsLocalization R T M) : T ⊗[S] H1Cotangent R S →ₗ[T] H1Cotangent R T)
    (LinearMap.liftBaseChange T (H1Cotangent.map R R S T))
have a : ∀ (x : H1Cotangent R S),
  Eq (α := H1Cotangent R T)
    ((((AlgebraTensorModule.curry
                  (↑(tensorH1CotangentOfIsLocalization R T M) : T ⊗[S] H1Cotangent R S →ₗ[T] H1Cotangent R T) :
                T →ₗ[T] H1Cotangent R S →ₗ[S] H1Cotangent R T) :
              (a : T) → H1Cotangent R S →ₗ[S] H1Cotangent R T)
            1 :
          (a : H1Cotangent R S) → H1Cotangent R T)
        x :
      H1Cotangent R T)
    ((((AlgebraTensorModule.curry (LinearMap.liftBaseChange T (H1Cotangent.map R R S T)) :
                T →ₗ[T] H1Cotangent R S →ₗ[S] H1Cotangent R T) :
              (a : T) → H1Cotangent R S →ₗ[S] H1Cotangent R T)
            1 :
          (a : H1Cotangent R S) → H1Cotangent R T)
        x :
      H1Cotangent R T)
Tactic: ext x : 3
-- 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
x : H1Cotangent R S
⊢ Eq (α := H1Cotangent R T)
    ((((AlgebraTensorModule.curry
                  (↑(tensorH1CotangentOfIsLocalization R T M) : T ⊗[S] H1Cotangent R S →ₗ[T] H1Cotangent R T) :
                T →ₗ[T] H1Cotangent R S →ₗ[S] H1Cotangent R T) :
              (a : T) → H1Cotangent R S →ₗ[S] H1Cotangent R T)
            1 :
          (a : H1Cotangent R S) → H1Cotangent R T)
        x :
      H1Cotangent R T)
    ((((AlgebraTensorModule.curry (LinearMap.liftBaseChange T (H1Cotangent.map R R S T)) :
                T →ₗ[T] H1Cotangent R S →ₗ[S] H1Cotangent R T) :
              (a : T) → H1Cotangent R S →ₗ[S] H1Cotangent R T)
            1 :
          (a : H1Cotangent R S) → H1Cotangent R T)
        x :
      H1Cotangent R T)
have a : Eq (α := H1Cotangent R T)
  ((tensorH1CotangentOfIsLocalization R T M : (a : T ⊗[S] H1Cotangent R S) → H1Cotangent R T) (1 ⊗ₜ[S] x) :
    H1Cotangent R T)
  ((H1Cotangent.map R R S T : (a : H1Cotangent R S) → H1Cotangent R T) x : H1Cotangent R T)
Tactic: simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, LinearMap.liftBaseChange_tmul, one_smul]
-- 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
x : H1Cotangent R S
⊢ Eq (α := H1Cotangent R T)
    ((tensorH1CotangentOfIsLocalization R T M : (a : T ⊗[S] H1Cotangent R S) → H1Cotangent R T) (1 ⊗ₜ[S] x) :
      H1Cotangent R T)
    ((H1Cotangent.map R R S T : (a : H1Cotangent R S) → H1Cotangent R T) x : H1Cotangent R T)
have a : Eq (α := H1Cotangent R T)
  ((Extension.H1Cotangent.equivOfFormallySmooth
          (Extension.ofSurjective (P :=
            Localization
              (Submonoid.comap (F := Generators.Ring (Generators.self R S) →+* S)
                (algebraMap (Generators.Ring (Generators.self R S)) S) M))
            (IsLocalization.liftAlgHom (R := Generators.Ring (Generators.self R S)) (f :=
              AlgHom.comp (IsScalarTower.toAlgHom R S T)
                (IsScalarTower.toAlgHom R (Generators.Ring (Generators.self R S)) S))
              sorry)
            sorry)
          (Generators.toExtension (Generators.self R T)) :
        (a : (Extension.ofSurjective (IsLocalization.liftAlgHom sorry) sorry).H1Cotangent) → H1Cotangent R T)
      ((Extension.H1Cotangent.map
            {
              toRingHom :=
                algebraMap (Generators.Ring (Generators.self R S))
                  (Localization
                    (Submonoid.comap (F := Generators.Ring (Generators.self R S) →+* S)
                      (algebraMap (Generators.Ring (Generators.self R S)) S) M)),
              toRingHom_algebraMap := sorry, algebraMap_toRingHom := sorry } :
          (a : (Generators.self R S).toExtension.H1Cotangent) →
            (Extension.ofSurjective (IsLocalization.liftAlgHom sorry) sorry).H1Cotangent)
        x) :
    H1Cotangent R T)
  ((H1Cotangent.map R R S T : (a : H1Cotangent R S) → H1Cotangent R T) x : H1Cotangent R T)
Tactic: simp only [tensorH1CotangentOfIsLocalization, Generators.toExtension_Ring,
    Extension.tensorH1CotangentOfFormallyEtale,
    LinearEquiv.ofBijective_apply, LinearMap.liftBaseChange_tmul, one_smul,
    Extension.equivH1CotangentOfFormallySmooth, LinearEquiv.trans_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
x_1 : H1Cotangent R S
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 : T
⊢ ∃ (a : Localization M'), (fQ : (a : Localization M') → T) a = x
have obtain : ∀ (x s : S) (hs : s ∈ M),
  ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a = IsLocalization.mk' T x (Subtype.mk (p := fun (x : S) ↦ 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
x_1 : H1Cotangent R S
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 : S
hs : s ∈ M
⊢ ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a = IsLocalization.mk' T x (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
have obtain : ∀ (x : P.Ring),
  ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a =
      IsLocalization.mk' T ((algebraMap P.Ring S : (a : P.Ring) → S) x) (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
Tactic: obtain ⟨x, rfl⟩ := P.algebraMap_surjective 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
x_1 : H1Cotangent R S
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)) ⋯
s : S
hs : s ∈ M
x : P.Ring
⊢ ∃ (a : Localization M'),
    (fQ : (a : Localization M') → T) a =
      IsLocalization.mk' T ((algebraMap P.Ring S : (a : P.Ring) → S) x) (Subtype.mk (p := fun (x : S) ↦ x ∈ M) s hs)
have obtain : ∀ (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)
Tactic: obtain ⟨s, rfl⟩ := P.algebraMap_surjective s
Cleared hypotheses: s, 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
x_1 : H1Cotangent R S
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
x_1 : H1Cotangent R S
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
x_1 : H1Cotangent R S
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 (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
x : H1Cotangent R S
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 ⋯
⊢ Eq (α := MvPolynomial T R →ₐ[R] T) (AlgHom.comp (IsScalarTower.toAlgHom R Q.Ring T) (MvPolynomial.aeval Q.σ))
    (IsScalarTower.toAlgHom R (Extension.Ring (Generators.toExtension (Generators.self R T))) T)
have hf : ∀ (i : T),
  Eq.{u_3 + 1} (α := T)
    ((AlgHom.comp (IsScalarTower.toAlgHom R Q.Ring T) (MvPolynomial.aeval Q.σ) : (a : MvPolynomial T R) → T)
        (MvPolynomial.X i) :
      T)
    ((IsScalarTower.toAlgHom R (Extension.Ring (Generators.toExtension (Generators.self R T))) T :
          (a : MvPolynomial T R) → T)
        (MvPolynomial.X i) :
      T)
Tactic: ext i
-- 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
x : H1Cotangent R S
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 ⋯
i : T
⊢ Eq.{u_3 + 1} (α := T)
    ((AlgHom.comp (IsScalarTower.toAlgHom R Q.Ring T) (MvPolynomial.aeval Q.σ) : (a : MvPolynomial T R) → T)
        (MvPolynomial.X i) :
      T)
    ((IsScalarTower.toAlgHom R (Extension.Ring (Generators.toExtension (Generators.self R T))) T :
          (a : MvPolynomial T R) → T)
        (MvPolynomial.X i) :
      T)
have hf : Eq.{u_3 + 1} (α := T)
  ((AlgHom.comp (IsScalarTower.toAlgHom R Q.Ring T) (MvPolynomial.aeval Q.σ) : (a : MvPolynomial T R) → T)
      (MvPolynomial.X i) :
    T)
  ((algebraMap (Generators.Ring (Generators.self R T)) T : (a : (Generators.self R T).Ring) → T) (MvPolynomial.X i) : T)
Tactic: change _ = algebraMap (Generators.self R T).Ring _ (.X i)
-- 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
x : H1Cotangent R S
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 ⋯
⊢ ∀ (x : Extension.Ring (Generators.toExtension (Generators.self R T))),
    Eq (α := T)
      ((algebraMap Q.Ring T : (a : Q.Ring) → T)
          ((AlgHom.toRingHom (MvPolynomial.aeval Q.σ) : (a : (Generators.self R T).toExtension.Ring) → Q.Ring) x :
            Q.Ring) :
        T)
      ((algebraMap T T : (a : T) → T)
          ((algebraMap (Extension.Ring (Generators.toExtension (Generators.self R T))) T :
                (a : (Generators.self R T).toExtension.Ring) → T)
              x :
            T) :
        T)
have this : Eq (α := MvPolynomial T R →ₐ[R] T) (AlgHom.comp (IsScalarTower.toAlgHom R Q.Ring T) (MvPolynomial.aeval Q.σ))
  (IsScalarTower.toAlgHom R (Extension.Ring (Generators.toExtension (Generators.self R T))) T)
Tactic: have : (IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ) =
          IsScalarTower.toAlgHom _ (Generators.self R T).toExtension.Ring _ := by
        ext i
        change _ = algebraMap (Generators.self R T).Ring _ (.X i)
        simp
-- 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
⊢ IsLocalizedModule (M := H1Cotangent R S) (M' := H1Cotangent R T) M (map R R S T)
have rw : IsBaseChange (M := H1Cotangent R S) (N := H1Cotangent R T) T (map R R S T)
Tactic: rw [isLocalizedModule_iff_isBaseChange M T]
-- 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
⊢ IsBaseChange (M := H1Cotangent R S) (N := H1Cotangent R T) T (map R R S T)
have change : Function.Bijective (α := T ⊗[S] H1Cotangent R S) (β := H1Cotangent R T)
  (⇑(LinearMap.liftBaseChange T (map R R S T)) : (a : T ⊗[S] H1Cotangent R S) → H1Cotangent R T)
Tactic: change Function.Bijective ((Algebra.H1Cotangent.map R R S T).liftBaseChange T)
-- 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
⊢ Function.Bijective (α := T ⊗[S] H1Cotangent R S) (β := H1Cotangent R T)
    (⇑(LinearMap.liftBaseChange T (map R R S T)) : (a : T ⊗[S] H1Cotangent R S) → H1Cotangent R T)
have rw : Function.Bijective (α := T ⊗[S] H1Cotangent R S) (β := H1Cotangent R T)
  (⇑(↑(tensorH1CotangentOfIsLocalization R T M) : T ⊗[S] H1Cotangent R S →ₗ[T] H1Cotangent R T) :
    (a : T ⊗[S] H1Cotangent R S) → H1Cotangent R T)
Tactic: rw [← tensorH1CotangentOfIsLocalization_toLinearMap R T M]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsEtaleAt R p
inst_11 : IsEtaleAt A P
this : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
⊢ IsEtaleAt R P
have this₁ : FormallyEtale.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P)
Tactic: have : FormallyEtale (Localization.AtPrime p) (Localization.AtPrime P) :=
    .localization_base p.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) ((Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ)
have h : ∀ (p : PrimeSpectrum A),
  Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) ((Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) ((Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ) p
have h : Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
  Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
Tactic: simp only [Set.mem_inter_iff, Set.mem_compl_iff, Module.notMem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
have h : ∀ (h₁ : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]),
  Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
Tactic: have h₁ := IsLocalizedModule.iso p.asIdeal.primeCompl
    (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
h₁ : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
have h : ∀
  (h₂ :
    LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A]
      H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)),
  Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
Tactic: have h₂ := IsLocalizedModule.iso p.asIdeal.primeCompl
    (H1Cotangent.map R R A (Localization.AtPrime p.asIdeal))