Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case refine_1
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).IsIntegral

pp: case refine_2
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).FiniteType

Tactic:
· have : IsLocalization.Away (f.toRingHom (algebraMap R S r))
        (Localization.Away (algebraMap R T r)) := by
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgHom.commutes]; infer_instance
    have h₁ : (Localization.awayMap (algebraMap R S) r).IsIntegral := isIntegral_localization
    have h₂ : Function.Surjective (IsLocalization.Away.map (Localization.Away (algebraMap R S r))
        (Localization.Away (algebraMap R T r)) f.toRingHom (algebraMap R S r)) := by
      intro x
      obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R T r)) x
      suffices ∃ a k l, algebraMap R T r ^ (l + n) * f a =
          algebraMap R T r ^ (l + k) * x by
        simpa [(IsLocalization.mk'_surjective (.powers (algebraMap R S r))).exists,
          IsLocalization.Away.map, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq,
          ← map_pow, Submonoid.mem_powers_iff, IsLocalization.Away.map, IsLocalization.map_mk',
          IsLocalization.mk'_eq_iff_eq, ← map_mul, ← mul_assoc, ← pow_add,
          IsLocalization.eq_iff_exists (.powers (algebraMap R T r))]
      have : PrimeSpectrum.basicOpen (algebraMap R S r) ≤ PrimeSpectrum.basicOpen g := by
        simpa [← SetLike.coe_subset_coe] using hrg
      simp only [PrimeSpectrum.basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff,
        Ideal.mem_span_singleton] at this
      obtain ⟨m', s, hs⟩ := this
      obtain ⟨b, m, e : f b = f g ^ m * x⟩ := Localization.awayMap_surjective_iff.mp hg x
      have : f (s ^ m * b) = f (g * s) ^ m * x := by simp [e, mul_pow, mul_assoc, mul_left_comm]
      simp_rw [← hs, map_pow, AlgHom.commutes, ← pow_mul] at this
      refine ⟨s ^ m * b, (n + m' * m), 0, this ▸ ?_⟩
      simp [pow_add, mul_assoc]
    convert! h₁.trans _ _ (RingHom.IsIntegral.of_finite (.of_surjective _ h₂)) using 1
    refine IsLocalization.ringHom_ext (.powers r) (RingHom.ext fun x ↦ ?_)
    simp [Localization.awayMap, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply R T]

Goal state after:
case refine_2
R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
⊢ (awayMapₐ (Algebra.ofId R T) r).FiniteType