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)) ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this_1 : FormallySmooth R P.Ring
this_2 : FormallySmooth P.Ring (Localization M')
this_3 : FormallySmooth R Q.Ring
this_4 : Module.Flat S T
this_5 : Algebra P.Ring Q.Ring := inferInstance
this_6 : Algebra P.Ring T :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S T) (algebraMap P.Ring S))
this_7 : Algebra (Localization M') T := fQ.toAlgebra
this_8 : IsScalarTower P.Ring S T
this_9 : IsScalarTower P.Ring (Localization M') T
this_10 : IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
F : LinearMap (R := P.Ring) (RingHom.id P.Ring) ↥P.ker ↥(RingHom.ker fQ) := f.mapKer ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
x : ↥P.ker
⊢ Eq (α := Localization M') (↑((F : (a : ↥P.ker) → ↥(RingHom.ker fQ)) x) : Localization M')
    (↑(((↑(LinearEquiv.restrictScalars P.Ring
                    (LinearEquiv.ofEq
                      (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                        (LinearMap.ker (Algebra.linearMap P.Ring S)))
                      (RingHom.ker fQ) this)) :
                ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                      (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
                  ↥(RingHom.ker fQ)) ∘ₗ
              Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker :
            (a : ↥P.ker) → ↥(RingHom.ker fQ))
          x) :
      Localization M')

Tactic:
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_10 : IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
F : LinearMap (R := P.Ring) (RingHom.id P.Ring) ↥P.ker ↥(RingHom.ker fQ) := f.mapKer ⋯
this :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
⊢ F =
    (↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker

Tactic:
have : F = ((LinearEquiv.ofEq _ _ this).restrictScalars P.Ring).toLinearMap ∘ₗ
      P.ker.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) := by
      ext; rfl
-- 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_10 : IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
F : LinearMap (R := P.Ring) (RingHom.id P.Ring) ↥P.ker ↥(RingHom.ker fQ) := f.mapKer ⋯
this_11 :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
this :
  F =
    (↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
refine_2 :
  IsLocalizedModule M'
    ((↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)
⊢ IsLocalizedModule M' F

Tactic:
rw [this]
-- 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_10 : IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
F : LinearMap (R := P.Ring) (RingHom.id P.Ring) ↥P.ker ↥(RingHom.ker fQ) := f.mapKer ⋯
this_11 :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
this :
  F =
    (↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
⊢ IsLocalizedModule M'
    ((↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)

Tactic:
IsLocalizedModule.of_linearEquiv _ _ _

Premises used: Set.Mem, IsLocalizedModule.of_linearEquiv
-- 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_10 : IsLocalizedModule M' (AlgHom.toLinearMap (IsScalarTower.toAlgHom P.Ring S T))
F : LinearMap (R := P.Ring) (RingHom.id P.Ring) ↥P.ker ↥(RingHom.ker fQ) := f.mapKer ⋯
this_11 :
  Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
      (LinearMap.ker (Algebra.linearMap P.Ring S)) =
    RingHom.ker fQ
this :
  F =
    (↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker
⊢ IsLocalizedModule M'
    ((↑(LinearEquiv.restrictScalars P.Ring
            (LinearEquiv.ofEq
              (Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
                (LinearMap.ker (Algebra.linearMap P.Ring S)))
              (RingHom.ker fQ) this_11)) :
        ↥(Submodule.localized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M'))
              (Algebra.linearMap P.Ring S).ker) →ₗ[P.Ring]
          ↥(RingHom.ker fQ)) ∘ₗ
      Submodule.toLocalized' (Localization M') M' (Algebra.linearMap P.Ring (Localization M')) P.ker)

Tactic:
exact IsLocalizedModule.of_linearEquiv _ _ _

Premises used: IsLocalizedModule.of_linearEquiv
-- 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
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)
⊢ 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))

Tactic:
ext x : 3
-- 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
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)
⊢ 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:
simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, LinearMap.liftBaseChange_tmul, one_smul]

Premises used: LinearMap.coe_restrictScalars, TensorProduct.AlgebraTensorModule.curry_apply, one_smul, LinearMap.liftBaseChange_tmul, TensorProduct.curry_apply, LinearEquiv.coe_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
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))
                ⋯)
              ⋯)
            (Generators.toExtension (Generators.self R T)) :
          (a : (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯).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 := ⋯, algebraMap_toRingHom := ⋯ } :
            (a : (Generators.self R S).toExtension.H1Cotangent) →
              (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯).H1Cotangent)
          x) :
      H1Cotangent R T)
    ((H1Cotangent.map R R S T : (a : H1Cotangent R S) → H1Cotangent R T) x : H1Cotangent R T)
⊢ 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 [tensorH1CotangentOfIsLocalization, Generators.toExtension_Ring,
    Extension.tensorH1CotangentOfFormallyEtale,
    LinearEquiv.ofBijective_apply, LinearMap.liftBaseChange_tmul, one_smul,
    Extension.equivH1CotangentOfFormallySmooth, LinearEquiv.trans_apply]

Premises used: Algebra.Extension.tensorH1CotangentOfFormallyEtale, Algebra.tensorH1CotangentOfIsLocalization, LinearEquiv.trans_apply, LinearEquiv.ofBijective_apply, one_smul, LinearMap.liftBaseChange_tmul, Algebra.Generators.toExtension_Ring, Algebra.Extension.equivH1CotangentOfFormallySmooth
-- 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
x_1 : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit.{u_3} (M := T)
    ((AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S) : (a : P.Ring) → T)
        (↑(Subtype.mk (p := fun (x : P.Ring) ↦ x ∈ M') y hy) : P.Ring) :
      T)

Tactic:
simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩

Premises used: Algebra.algebraMap, Algebra.Extension.Ring, Subtype.mk, IsLocalization.map_units, 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_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
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)
⊢ ∃ (a : Localization M'), (fQ : (a : Localization M') → T) a = x

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- 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 : S
hs : s ∈ M
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)
⊢ ∃ (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, rfl⟩ := P.algebraMap_surjective x

Premises used: Algebra.Extension.algebraMap_surjective, 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
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
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)
⊢ ∃ (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 ⟨s, rfl⟩ := P.algebraMap_surjective s

Premises used: Algebra.Extension.algebraMap_surjective, 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
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)

Tactic:
⟨IsLocalization.mk' _ x ⟨s, show s ∈ M' from hs⟩, ?_⟩

Premises used: Subtype.mk, IsLocalization.mk', Exists.intro