-- 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₀)
obtain :
  ∀ (f : R') (hfP : f ∉ P)
    (hf :
      AlgHom.Finite (R := R') (A := Localization.Away f) (B :=
        Localization.Away (M :=
          Localization.Away (M := R' ⊗[R] S)
            (((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₀ :
              R' ⊗[R] S))
          ((ofId R'
                  (Localization.Away (M := R' ⊗[R] S)
                    (((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₀ :
                      R' ⊗[R] S)) :
                (a : R') →
                  Localization.Away
                    ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S) :
                        (a : R' ⊗[R] R'') → R' ⊗[R] S)
                      e₀))
              f :
            Localization.Away (M := R' ⊗[R] S)
              (((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₀ :
                R' ⊗[R] S)))
        (Localization.awayMapₐ
          (ofId R'
            (Localization.Away (M := R' ⊗[R] S)
              (((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₀ :
                R' ⊗[R] S)))
          f)),
    ∃ f ∉ P,
      Module.Finite (Localization.Away f)
        (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
          (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
                  R' ⊗[R] S →ₐ[R'] 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))
⊢ ∃ f ∉ P,
    Module.Finite (Localization.Away f)
      (Localization.Away (M := TensorProduct.{u_2, u_4, u_3} R (Localization.Away f) S)
        (((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S) :
                R' ⊗[R] S →ₐ[R'] 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:
obtain ⟨f, hfP, hf⟩ := Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ
    (Localization.awayMapₐ (Algebra.TensorProduct.map (.id R' R')
      (IsScalarTower.toAlgHom R R'' S)) e₀) (algebraMap (R' ⊗[R] R'') _ (1 ⊗ₜ g)) (by
    apply Localization.awayMap_awayMap_surjective
    refine Localization.awayMap_surjective_iff.mpr fun a ↦ ?_
    induction a with
    | zero => use 0; simp
    | tmul a b =>
      obtain ⟨b', m, e : _ = _⟩ := Localization.awayMap_surjective_iff.mp hg b
      refine ⟨e₀ ^ m * a ⊗ₜ b', m, ?_⟩
      simp [e, mul_pow, mul_assoc]
    | add a b ha hb =>
      obtain ⟨xa, ma, ea⟩ := ha
      obtain ⟨xb, mb, eb⟩ := hb
      refine ⟨(e₀ * 1 ⊗ₜ[R] g) ^ mb * xa + (e₀ * 1 ⊗ₜ[R] g) ^ ma * xb, ma + mb, ?_⟩
      dsimp at ea eb ⊢
      simp only [map_add, map_mul, map_pow, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        ea, eb, pow_add]
      ring) P (by
    contrapose hgq
    obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal _ (Ideal.span_singleton_eq_top.not.mpr hgq)
    have := H (m.comap (Algebra.TensorProduct.includeRight.toRingHom.comp (algebraMap _ _)))
      inferInstance (m.comap_liesOver P (Algebra.TensorProduct.includeRight.comp
        (IsScalarTower.toAlgHom _ _ _)))
        (Ideal.notMem_of_isUnit (m.comap Algebra.TensorProduct.includeRight)
        (IsLocalization.Away.algebraMap_isUnit _))
    rw [← hP'q]
    exact this.le ((Ideal.span_singleton_le_iff_mem _).mp hm :))

Premises used: Algebra.algebraMap, Algebra.TensorProduct.map, Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ, IsScalarTower.toAlgHom, AlgHom.id, TensorProduct, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, Localization.awayMapₐ