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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
right :
  ∀ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent)
    (ha :
      Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
        ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
          TensorProduct.{u_2, u_3, u} S T P.Cotangent)
        (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
          TensorProduct.{u_2, u_3, u} S T P.Cotangent)),
    ∃ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent),
      (LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a = x
⊢ ∃ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent),
    (LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a = x

Tactic:
obtain ⟨a, ha⟩ := (this ((Extension.tensorCotangent f halg H₂).symm x.1)).mp (by
      apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
      rw [LinearEquiv.map_zero, ← x.2]
      have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
          Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
        ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
        simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
      exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1)))

Premises used: LinearEquiv.symm, Iff.mp, Algebra.Extension.tensorCotangent, Subtype.val, 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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
⊢ ∃ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent),
    (LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a = x

Tactic:
⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩

Premises used: LinearEquiv.eq_symm_apply, Exists.intro, Iff.mp, Eq.trans, Subtype.ext
-- 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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
right :
  Eq.{u + 1} (α := Q.Cotangent)
    ((↑((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a) :
        Q.Cotangent) :
      Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a) :
      Q.Cotangent)
⊢ ∃ (a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent),
    (LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a = x

Tactic:
refine ⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩
-- 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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
right :
  Eq.{u + 1} (α := Q.Cotangent)
    ((h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent) a :
      Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι :
          (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent)
        a :
      Q.Cotangent)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((↑((LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.H1Cotangent) a) :
        Q.Cotangent) :
      Q.Cotangent)
    ((tensorCotangent f halg H₂ : (a : T ⊗[S] P.Cotangent) → Q.Cotangent)
        ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a) :
      Q.Cotangent)

Tactic:
change (h1Cotangentι ∘ₗ (H1Cotangent.map f).liftBaseChange T) _ =
      ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) _

Premises used: LinearMap.baseChange, Algebra.Extension.H1Cotangent.map, LinearMap.comp, LinearMap.liftBaseChange, Algebra.Extension.h1Cotangentι, Algebra.Extension.Cotangent.map, 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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
right :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent →ₗ[T] Q.Cotangent)
    (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))
    (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι)
⊢ Eq.{u + 1} (α := Q.Cotangent)
    ((h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f) : (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent) a :
      Q.Cotangent)
    ((LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι :
          (a : T ⊗[S] P.H1Cotangent) → Q.Cotangent)
        a :
      Q.Cotangent)

Tactic:
congr 1
-- 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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
right :
  ∀ (x : P.H1Cotangent),
    Eq.{u + 1} (α := Q.ker.Cotangent)
      (Cotangent.val
        ((((AlgebraTensorModule.curry (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f)) :
                  LinearMap.{u_3, u_3, u_3, u} (RingHom.id T) T (P.H1Cotangent →ₗ[S] Q.Cotangent)) :
                (a : T) → P.H1Cotangent →ₗ[S] Q.Cotangent)
              1 :
            (a : P.H1Cotangent) → Q.Cotangent)
          x))
      (Cotangent.val
        ((((AlgebraTensorModule.curry
                    (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι) :
                  LinearMap.{u_3, u_3, u_3, u} (RingHom.id T) T (P.H1Cotangent →ₗ[S] Q.Cotangent)) :
                (a : T) → P.H1Cotangent →ₗ[S] Q.Cotangent)
              1 :
            (a : P.H1Cotangent) → Q.Cotangent)
          x))
⊢ Eq (α := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent →ₗ[T] Q.Cotangent)
    (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))
    (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι)

Tactic:
ext
-- 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
P : Extension.{u, u_1, u_2} R S
Q : Extension.{u, u_1, u_3} R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst_7 : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ :
  Function.Bijective (α := Q.Ring ⊗[P.Ring] ↥P.ker) (β := ↥Q.ker)
    (⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) : (a : Q.Ring ⊗[P.Ring] ↥P.ker) → ↥Q.ker)
x : Q.H1Cotangent
this :
  Function.Exact (M := TensorProduct.{u_2, u_3, u} S T P.H1Cotangent) (N := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (P := T ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange T h1Cotangentι) : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent)
    (⇑(LinearMap.baseChange T P.cotangentComplex) : (a : T ⊗[S] P.Cotangent) → T ⊗[S] P.CotangentSpace)
a : TensorProduct.{u_2, u_3, u} S T P.H1Cotangent
ha :
  Eq (α := TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    ((LinearMap.baseChange T h1Cotangentι : (a : T ⊗[S] P.H1Cotangent) → T ⊗[S] P.Cotangent) a :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
    (((tensorCotangent f halg H₂).symm : (a : Q.Cotangent) → T ⊗[S] P.Cotangent) (↑x : Q.Cotangent) :
      TensorProduct.{u_2, u_3, u} S T P.Cotangent)
x_1 : P.H1Cotangent
⊢ Eq.{u + 1} (α := Q.ker.Cotangent)
    (Cotangent.val
      ((((AlgebraTensorModule.curry (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f)) :
                LinearMap.{u_3, u_3, u_3, u} (RingHom.id T) T (P.H1Cotangent →ₗ[S] Q.Cotangent)) :
              (a : T) → P.H1Cotangent →ₗ[S] Q.Cotangent)
            1 :
          (a : P.H1Cotangent) → Q.Cotangent)
        x_1))
    (Cotangent.val
      ((((AlgebraTensorModule.curry
                  (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι) :
                LinearMap.{u_3, u_3, u_3, u} (RingHom.id T) T (P.H1Cotangent →ₗ[S] Q.Cotangent)) :
              (a : T) → P.H1Cotangent →ₗ[S] Q.Cotangent)
            1 :
          (a : P.H1Cotangent) → Q.Cotangent)
        x_1))

Tactic:
dsimp
-- 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
x : ↥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
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
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
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
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
-- Module: Mathlib.RingTheory.Etale.Kaehler
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
M : Submonoid S
inst_7 : IsLocalization M T
P : Extension R S := Generators.toExtension (Generators.self R S)
M' : Submonoid P.Ring := Submonoid.comap (F := P.Ring →+* S) (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T :=
  IsLocalization.liftAlgHom (R := P.Ring) (M := M') (f :=
    AlgHom.comp (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R P.Ring S)) ⋯
x s : P.Ring
hs : Membership.mem (α := S) M ((algebraMap P.Ring S : (a : P.Ring) → S) s : S)
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
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