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
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)
refine :
  (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)
⊢ ∃ (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:
refine ⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩
-- 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
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)
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)) ⋯ :
        (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)
⊢ (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)

Tactic:
simp only [fQ, IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe]

Premises used: IsLocalization.coe_liftAlgHom, AlgHom.toRingHom_eq_coe
-- 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
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)
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
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)
⊢ ((↑(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
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 ⋯
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)
⊢ 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:
ext i
-- 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
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
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)
⊢ 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:
change _ = algebraMap (Generators.self R T).Ring _ (.X i)

Premises used: Algebra.Generators.Ring, Algebra.algebraMap, MvPolynomial.X, Algebra.Generators.self, DFunLike.coe
-- 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
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)
    ((algebraMap (Generators.Ring (Generators.self R T)) T : (a : (Generators.self R T).Ring) → T) (MvPolynomial.X i) :
      T)

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
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)

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
-- 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
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 ⋯
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)
⊢ ∀ (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)

Tactic:
DFunLike.congr_fun this

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, AddMonoidAlgebra, Finset.sum
-- 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
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 ⋯
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)
⊢ ∀ (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)

Tactic:
exact DFunLike.congr_fun this

Premises used: DFunLike.congr_fun
-- 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
rw : IsBaseChange (M := H1Cotangent R S) (N := H1Cotangent R T) T (map R R S T)
⊢ IsLocalizedModule (M := H1Cotangent R S) (M' := H1Cotangent R T) M (map R R S T)

Tactic:
rw [isLocalizedModule_iff_isBaseChange M T]

Premises used: isLocalizedModule_iff_isBaseChange
-- 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
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)
⊢ IsBaseChange (M := H1Cotangent R S) (N := H1Cotangent R T) T (map R R S T)

Tactic:
change Function.Bijective ((Algebra.H1Cotangent.map R R S T).liftBaseChange T)

Premises used: Algebra.H1Cotangent.map, LinearMap.liftBaseChange, Function.Bijective, DFunLike.coe
-- 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
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)
⊢ 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:
rw [← tensorH1CotangentOfIsLocalization_toLinearMap R T M]

Premises used: Algebra.tensorH1CotangentOfIsLocalization_toLinearMap
-- 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
⊢ 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:
(tensorH1CotangentOfIsLocalization R T M).bijective

Premises used: LinearEquiv.bijective, Algebra.tensorH1CotangentOfIsLocalization
-- 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
⊢ 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:
exact (tensorH1CotangentOfIsLocalization R T M).bijective

Premises used: LinearEquiv.bijective, Algebra.tensorH1CotangentOfIsLocalization
-- Module: Mathlib.RingTheory.Etale.Locus
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 ↔ IsEtaleAt R p.asIdeal

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, Algebra.etaleLocus, setOf
-- Module: Mathlib.RingTheory.Etale.Locus
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
⊢ FormallyEtale.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P)

Tactic:
have : FormallyEtale (Localization.AtPrime p) (Localization.AtPrime P) :=
    .localization_base p.primeCompl
-- Module: Mathlib.RingTheory.Etale.Locus
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_1 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this : FormallyEtale.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P)
⊢ IsEtaleAt R P

Tactic:
FormallyEtale.comp R (Localization.AtPrime p) _

Premises used: Algebra.FormallyEtale.comp, Localization.AtPrime
-- Module: Mathlib.RingTheory.Etale.Locus
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_1 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this : FormallyEtale.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P)
⊢ IsEtaleAt R P

Tactic:
exact FormallyEtale.comp R (Localization.AtPrime p) _

Premises used: Algebra.FormallyEtale.comp, Localization.AtPrime
-- Module: Mathlib.RingTheory.Etale.Locus
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) (unramifiedLocus R A ∩ smoothLocus R A)

Tactic:
Set.ext fun _ ↦ FormallyEtale.iff_formallyUnramified_and_formallySmooth

Premises used: Set.ext, Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) ((Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Etale.Locus
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 :
  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))
⊢ 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:
simp only [Set.mem_inter_iff, Set.mem_compl_iff, Module.notMem_support_iff]

Premises used: Set.mem_inter_iff, Module.notMem_support_iff, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Etale.Locus
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 :
  ∀ (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))
⊢ 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))
-- Module: Mathlib.RingTheory.Etale.Locus
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]
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))
⊢ 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))