-- 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)
inr :
  ∀
    (this :
      ∀ (m : ℕ) (hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)) (hm0 : 0 < m),
        ∃ s ∉ q,
          ∃ (hs : IsIntegral R s),
            (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
              ∀ (q' : Ideal ↥(integralClosure R S)),
                q'.IsPrime →
                  q' ≠ Ideal.under (↥(integralClosure R S)) q →
                    q'.LiesOver p →
                      Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s
                          hs ∈
                        q')
    (hm0 : ¬0 < m),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
wlog :
  ∀ (m : ℕ) (hm : (↑s₂ : S) ^ m * (↑s₃ : S) = (↑s₂ : S) ^ m * (s₁ * (↑s₂ : S) ^ n)) (hm0 : 0 < m),
    ∃ s ∉ q,
      ∃ (hs : IsIntegral R s),
        (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
          ∀ (q' : Ideal ↥(integralClosure R S)),
            q'.IsPrime →
              q' ≠ Ideal.under (↥(integralClosure R S)) q →
                q'.LiesOver p →
                  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime →
            q' ≠ Ideal.under (↥(integralClosure R S)) q →
              q'.LiesOver p →
                Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hs ∈ q'

Tactic:
wlog hm0 : 0 < m generalizing m