awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
⊢ IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)

Tactic:
have : IsLocalization.Away (f ⊗ₜ 1 : R' ⊗[R] S) (Localization.Away f ⊗[R] S) := by
    have : .powers (f ⊗ₜ[R] 1) = Algebra.algebraMapSubmonoid (R' ⊗[R] S) (.powers f) := by simp
    rw [IsLocalization.Away, this]
    refine IsLocalization.tensorProduct_tensorProduct _ _ _ _ ?_
    ext; simp [RingHom.algebraMap_toAlgebra, φ]
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this_1 : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
this : IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
⊢ IsLocalization.Away (e * f ⊗ₜ[R] 1)
    (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
      ((φ : (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S) e : TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))

Tactic:
have : IsLocalization.Away (e * (f ⊗ₜ 1)) (Localization.Away (φ e)) :=
    .mul (Localization.Away f ⊗[R] S) (Localization.Away (algebraMap _ _ e)) _ _
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
inst_4 : CommRing R'
inst_5 : Algebra R R'
inst_6 : CommRing R''
inst_7 : Algebra R R''
inst_8 : Algebra R'' S
inst_9 : Algebra.IsIntegral R R''
inst_10 : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst_11 : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] R'') → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := R' ⊗[R] R'' →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) : R' ⊗[R] R'' →ₐ[R'] R' ⊗[R] S))
              P'
g : R''
hgq : ((algebraMap R'' S : (a : R'') → S) g : S) ∉ q
hg :
  Function.Surjective.{u_5 + 1, u_3 + 1} (α := Localization.Away g) (β :=
    Localization.Away (M := S) ((algebraMap R'' S : (a : R'') → S) g : S))
    (⇑(Localization.awayMap (algebraMap R'' S) g) :
      (a : Localization.Away g) → Localization.Away ((algebraMap R'' S : (a : R'') → S) g))
this_1 : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
    Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))
    (Localization.awayMapₐ (ofId R' (Localization.Away e)) f)
φ : R' ⊗[R] S →ₐ[R'] TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S :=
  TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst : Algebra (R' ⊗[R] S) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S) := φ.toAlgebra
this_2 : IsLocalization.Away (R := R' ⊗[R] S) (f ⊗ₜ[R] 1) (TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
this :
  IsLocalization.Away (e * f ⊗ₜ[R] 1)
    (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
      ((φ : (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S) e : TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S))
⊢ IsLocalization.Away (e * f ⊗ₜ[R] 1)
    (Localization.Away (M := Localization.Away e)
      ((ofId R' (Localization.Away e) : (a : R') → Localization.Away e) f : Localization.Away e))

Tactic:
have : IsLocalization.Away (e * (f ⊗ₜ 1)) (Localization.Away (Algebra.ofId R'
      (Localization.Away e) f)) :=
    .mul' (Localization.Away e)
      (Localization.Away (algebraMap (R' ⊗[R] S) (Localization.Away e) (f ⊗ₜ[R] 1))) _ _
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
          TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
w_5 : P'.IsPrime
w_6 : P'.LiesOver P
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
heP' : e ∉ P'
hpP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
H' :
  ∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                  TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
              P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : (↑g : S) ∉ q
hg :
  Function.Bijective (α := Localization.Away g) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) g : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) g) :
      (a : Localization.Away g) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) g))
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away (M := Localization.Away f ⊗[R] S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        Localization.Away f ⊗[R] S))
Pf : Ideal (Localization.Away f) := Ideal.map (F := R' →+* Localization.Away f) (algebraMap R' (Localization.Away f)) P
rwa rwa₁ rwa₂ rwa₃ : f ∉ P
⊢ Disjoint (↑(Submonoid.powers f) : Set R') (↑P : Set R')

Tactic:
rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime]

Premises used: Ideal.disjoint_powers_iff_notMem_of_isPrime
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
          TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
w_5 : P'.IsPrime
w_6 : P'.LiesOver P
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
heP' : e ∉ P'
hpP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
H' :
  ∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                  TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
              P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : (↑g : S) ∉ q
hg :
  Function.Bijective (α := Localization.Away g) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) g : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) g) :
      (a : Localization.Away g) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) g))
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away (M := Localization.Away f ⊗[R] S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        Localization.Away f ⊗[R] S))
Pf : Ideal (Localization.Away f) := Ideal.map (F := R' →+* Localization.Away f) (algebraMap R' (Localization.Away f)) P
⊢ Pf.IsPrime

Tactic:
have : Pf.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_› (by
    rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime])
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
          TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
w_5 : P'.IsPrime
w_6 : P'.LiesOver P
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
heP' : e ∉ P'
hpP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
H' :
  ∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                  TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
              P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : (↑g : S) ∉ q
hg :
  Function.Bijective (α := Localization.Away g) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) g : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) g) :
      (a : Localization.Away g) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) g))
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away (M := Localization.Away f ⊗[R] S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        Localization.Away f ⊗[R] S))
Pf : Ideal (Localization.Away f) := Ideal.map (F := R' →+* Localization.Away f) (algebraMap R' (Localization.Away f)) P
this : Pf.IsPrime
rwa rwa₁ rwa₂ rwa₃ : f ∉ P
⊢ Disjoint (↑(Submonoid.powers f) : Set R') (↑P : Set R')

Tactic:
rwa [Ideal.disjoint_powers_iff_notMem _ (Ideal.IsPrime.isRadical ‹_›)]

Premises used: Ideal.disjoint_powers_iff_notMem, Ideal.IsPrime.isRadical
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
          TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
w_5 : P'.IsPrime
w_6 : P'.LiesOver P
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
heP' : e ∉ P'
hpP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
H' :
  ∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                  TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
              P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : (↑g : S) ∉ q
hg :
  Function.Bijective (α := Localization.Away g) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) g : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) g) :
      (a : Localization.Away g) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) g))
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away (M := Localization.Away f ⊗[R] S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        Localization.Away f ⊗[R] S))
Pf : Ideal (Localization.Away f) := Ideal.map (F := R' →+* Localization.Away f) (algebraMap R' (Localization.Away f)) P
this : Pf.IsPrime
⊢ Pf.LiesOver P

Tactic:
have : Pf.LiesOver P := ⟨(IsLocalization.under_map_of_isPrime_disjoint (.powers f) _ ‹_› (by
    rwa [Ideal.disjoint_powers_iff_notMem _ (Ideal.IsPrime.isRadical ‹_›)])).symm⟩
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e :
  ((TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
          TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S) :
        (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S)
      e₀ =
    e
P' : Ideal (R' ⊗[R] S)
w_5 : P'.IsPrime
w_6 : P'.LiesOver P
hP'q : Ideal.comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom TensorProduct.includeRight) P' = q
heP' : e ∉ P'
hpP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
H' :
  ∀ (P'' : Ideal (TensorProduct.{u, u, v} R R' ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' →
          P'' =
            Ideal.comap (F := TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →+* R' ⊗[R] S)
              (AlgHom.toRingHom
                (TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S)) :
                  TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S))
              P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : (↑g : S) ∉ q
hg :
  Function.Bijective (α := Localization.Away g) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) g : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) g) :
      (a : Localization.Away g) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) g))
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away (M := Localization.Away f ⊗[R] S)
      (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
              R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S) :
            (a : R' ⊗[R] S) → Localization.Away f ⊗[R] S)
          e :
        Localization.Away f ⊗[R] S))
Pf : Ideal (Localization.Away f) := Ideal.map (F := R' →+* Localization.Away f) (algebraMap R' (Localization.Away f)) P
this_1 : Pf.IsPrime
this_2 : Pf.LiesOver P
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
this_3 : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this : IsScalarTower R' (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := ⋯
⊢ Eq (α := Submonoid (R' ⊗[R] S)) (Submonoid.powers (f ⊗ₜ[R] 1)) (algebraMapSubmonoid (R' ⊗[R] S) (Submonoid.powers f))

Tactic:
simp