Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : 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)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝² : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this✝¹ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
this✝ : IsLocalization.Away (e * f ⊗ₜ[R] 1) (Localization.Away (φ e))
this : IsLocalization.Away (e * f ⊗ₜ[R] 1) (Localization.Away ((ofId R' (Localization.Away e)) f))
equiv : Localization.Away (φ e) ≃ₐ[R' ⊗[R] S] Localization.Away ((ofId R' (Localization.Away e)) f) :=
  IsLocalization.algEquiv (Submonoid.powers (e * f ⊗ₜ[R] 1)) (Localization.Away (φ e))
    (Localization.Away ((ofId R' (Localization.Away e)) f))
⊢ algebraMap (Localization.Away f)
      (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e)) =
    equiv.symm.toRingEquiv.toRingHom.comp (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).toRingHom

Tactic:
apply IsLocalization.ringHom_ext (.powers f)

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : 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)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this✝² : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := ⋯
algInst✝ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := ⋯
this✝¹ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
this✝ : IsLocalization.Away (e * f ⊗ₜ[R] 1) (Localization.Away (φ e))
this : IsLocalization.Away (e * f ⊗ₜ[R] 1) (Localization.Away ((ofId R' (Localization.Away e)) f))
equiv : Localization.Away (φ e) ≃ₐ[R' ⊗[R] S] Localization.Away ((ofId R' (Localization.Away e)) f) := ⋯
⊢ (algebraMap (Localization.Away f)
          (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))).comp
      (algebraMap R' (Localization.Away f)) =
    (equiv.symm.toRingEquiv.toRingHom.comp (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).toRingHom).comp
      (algebraMap R' (Localization.Away f))