-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
inst_5 : q.LiesOver p
inst_6 : FiniteType R S
inst_7 : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : (↑s₂ : S) ∉ q
hs₂ :
  Function.Bijective (α := Localization.Away s₂) (β :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    (⇑(Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂) :
      (a : Localization.Away s₂) →
        Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
s₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  Eq (α :=
    Localization.Away (M := S)
      ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((Localization.awayMap (AlgHom.toRingHom (Subalgebra.val (integralClosure R S))) s₂ :
          (a : Localization.Away s₂) →
            Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        (IsLocalization.mk' (Localization.Away s₂) s₃
          (Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S)) (Submonoid.powers s₂) x) ((fun (x : ℕ) ↦ s₂ ^ x) n)
            ⋯)) :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
    ((algebraMap S
            (Localization.Away (M := S)
              ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S)) :
          (a : S) → Localization.Away (((integralClosure R S).val.toRingHom : (a : ↥(integralClosure R S)) → S) s₂))
        s₁ :
      Localization.Away (M := S)
        ((AlgHom.toRingHom (Subalgebra.val (integralClosure R S)) : (a : ↥(integralClosure R S)) → S) s₂ : S))
m : ℕ
hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)
hm0 : 0 < m
hs₃q : (↑s₃ : S) ∉ q
q' : Ideal ↥(integralClosure R S)
h : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
h_1 : q'.LiesOver p
this_1 : Algebra (↥(integralClosure R S)) (Localization.Away (↑s₂ : S)) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away (↑s₂ : S) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
q's : Ideal (Localization.Away s₂) :=
  Ideal.map (F := ↥(integralClosure R S) →+* Localization.Away s₂)
    (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H :
  ¬Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x)
        ((↑s₂ : S) ^ m * (↑s₃ : S)) ⋯ ∈
      q'
hq's : Disjoint (↑(Submonoid.powers s₂) : Set ↥(integralClosure R S)) (↑q' : Set ↥(integralClosure R S))
this_2 : q's.IsPrime
this_3 : q's.LiesOver q'
this : q's.LiesOver p
⊢ Membership.mem (γ := Ideal S)
    (Ideal.comap (F := S →+* Localization.Away s₂)
      (AlgHom.toRingHom
        ((↑e.symm : Localization.Away (↑s₂ : S) →ₐ[↥(integralClosure R S)] Localization.Away s₂).comp
          (IsScalarTower.toAlgHom (↥(integralClosure R S)) S (Localization.Away (↑s₂ : S)))))
      q's)
    s₁

Tactic:
have := hs₁ (q's.comap (e.symm.toAlgHom.comp (IsScalarTower.toAlgHom _ _ _)).toRingHom)
    inferInstance (by
      contrapose hq'q
      rw [← hq'q, Ideal.under, Ideal.comap_comap, AlgHom.toRingHom_eq_coe,
        AlgHom.comp_algebraMap, q's.over_def q'])
    (inferInstanceAs ((q's.comap ((e.symm.toAlgHom.comp
      (IsScalarTower.toAlgHom _ _ _)).restrictScalars R)).LiesOver _))