-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
this_1 :
  IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))
r : R
hpr : { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R))
hrg :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum R)) ⊆
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))ᶜ
this :
  IsLocalization.Away.{u_1, u_1} (R := T) ((f.toRingHom : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
h₁ :
  RingHom.IsIntegral.{u, v} (R := Away r) (A := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
    (awayMap (algebraMap R S) r)
h₂ :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r : S)) (β :=
    Away (M := T) ((algebraMap R T : (a : R) → T) r : T))
    (⇑(IsLocalization.Away.map (Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
          (Away (M := T) ((algebraMap R T : (a : R) → T) r : T)) f.toRingHom ((algebraMap R S : (a : R) → S) r)) :
      (a : Away ((algebraMap R S : (a : R) → S) r)) → Away ((algebraMap R T : (a : R) → T) r))
e_2 : Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T) = Away (M := T) ((algebraMap R T : (a : R) → T) r : T)
e_4 :
  HEq.{u_1 + 1} (α := Ring (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))) CommRing.toRing (β :=
    Ring (Away (M := T) ((algebraMap R T : (a : R) → T) r : T))) CommRing.toRing
h :
  ∀ (x : R),
    Eq.{u_1 + 1} (α := Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
      (((RingHom.comp (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r)) (algebraMap R (Away r)) :
              RingHom.{u, u_1} R (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))) :
            (a : R) → Away ((Algebra.ofId R T : (a : R) → T) r))
          x :
        Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
      (((RingHom.comp (β := Away r)
                (RingHom.comp (β := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
                  (IsLocalization.Away.map (Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
                    (Away (M := T) ((algebraMap R T : (a : R) → T) r : T)) f.toRingHom
                    ((algebraMap R S : (a : R) → S) r))
                  (awayMap (algebraMap R S) r))
                (algebraMap R (Away r)) :
              RingHom.{u, u_1} R (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))) :
            (a : R) → Away ((Algebra.ofId R T : (a : R) → T) r))
          x :
        Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T))
⊢ Eq (α := RingHom.{u, u_1} (Away r) (Away (M := T) ((Algebra.ofId R T : (a : R) → T) r : T)))
    (AlgHom.toRingHom (awayMapₐ (Algebra.ofId R T) r))
    (RingHom.comp (β := Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
      (IsLocalization.Away.map (Away (M := S) ((algebraMap R S : (a : R) → S) r : S))
        (Away (M := T) ((algebraMap R T : (a : R) → T) r : T)) f.toRingHom ((algebraMap R S : (a : R) → S) r))
      (awayMap (algebraMap R S) r))

Tactic:
refine IsLocalization.ringHom_ext (.powers r) (RingHom.ext fun x ↦ ?_)

Premises used: RingHom.ext, Submonoid.powers, IsLocalization.ringHom_ext