-- 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}))
q : PrimeSpectrum S
hq : Membership.mem (γ := Set (PrimeSpectrum S)) (PrimeSpectrum.zeroLocus {g}) q
e : PrimeSpectrum.comap (algebraMap R S) q = { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }
this_2 : q.asIdeal.LiesOver p
this :
  1 ⊗ₜ[R] g ∉
    PrimeSpectrum.asIdeal
      ((PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := inst_7 } :
          (a : (↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := inst_7 }}) : Type v)) →
            PrimeSpectrum ({ asIdeal := p, isPrime := inst_7 }.asIdeal.Fiber S))
        (Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
          Membership.mem (γ := Set (PrimeSpectrum S))
            (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
              {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
            x)
          q e))
⊢ 1 ⊗ₜ[R] g ∉
    RingHom.ker (F :=
      { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →+*
        (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                  Membership.mem (γ := Set (PrimeSpectrum S))
                    (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                      {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                    x)
                  q e) :
              PrimeSpectrum S).asIdeal.ResidueField)
      (AlgHom.toRingHom
        (Algebra.TensorProduct.lift
            (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := inst_7 }.asIdeal
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                      Membership.mem (γ := Set (PrimeSpectrum S))
                        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                          {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                        x)
                      q e) :
                  PrimeSpectrum S).asIdeal
              (Algebra.ofId R S) ⋯)
            (IsScalarTower.toAlgHom R S
              (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                        Membership.mem (γ := Set (PrimeSpectrum S))
                          (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                            {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                          x)
                        q e) :
                    PrimeSpectrum S).asIdeal.ResidueField)
            ⋯ :
          { asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }.asIdeal.ResidueField ⊗[R] S →ₐ[R]
            (↑(Subtype.mk (p := fun (x : PrimeSpectrum S) ↦
                      Membership.mem (γ := Set (PrimeSpectrum S))
                        (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
                          {{ asIdeal := p, isPrime := inst_7 : PrimeSpectrum R }})
                        x)
                      q e) :
                  PrimeSpectrum S).asIdeal.ResidueField))

Tactic:
rw [PrimeSpectrum.preimageEquivFiber_apply_asIdeal] at this

Premises used: PrimeSpectrum.preimageEquivFiber_apply_asIdeal