-- Module: Mathlib.RingTheory.ZariskisMainTheorem
Goal:
n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] (p : Ideal S) [inst_7 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S) (hf : f.Finite), ZariskisMainProperty R p
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S :=
  f.comp
    (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →ₐ[R] MvPolynomial (Fin (n + 1)) R)
this_1 : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this_3 : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this_4 : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : (x : S) → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
R' : Subalgebra R S :=
  adjoin R
    (↑(Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}) :
      Set S)
hrR' : r ∈ R'
this_5 : WeaklyQuasiFiniteAt R (S := ↥R') (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' :=
  MvPolynomial.aeval fun (i : Fin n) ↦
    Subtype.mk (p := fun (x : S) ↦ x ∈ R') ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X i.succ)) ⋯
this_6 : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
this_7 : IsScalarTower (MvPolynomial (Fin n) R) (↥R') S
this :
  (∀ (a : Fin n),
      IsIntegral (MvPolynomial (Fin n) R) (A := S)
        ((f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X a.succ) : S)) ∧
    ∀ a ∈ s, IsIntegral (MvPolynomial (Fin n) R) (r ^ s.sup m * a)
simp :
  ∀ (x : S)
    (a :
      x ∈
        Finset.image (α := Fin n)
              (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                (MvPolynomial.X ∘ Fin.succ))
              Finset.univ ∪
            r ^ s.sup m • s ∪
          {r}),
    ∃ (h : True),
      Membership.mem (γ :=
        Subalgebra R
          ↥(adjoin R
              (↑(Finset.image (α := Fin n)
                        (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                          (MvPolynomial.X ∘ Fin.succ))
                        Finset.univ ∪
                      r ^ s.sup m • s ∪
                    {r}) :
                Set S)))
        (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R)
          (integralClosure (MvPolynomial (Fin n) R)
            ↥(adjoin R
                (↑(Finset.image (α := Fin n)
                          (Function.comp (β := MvPolynomial (Fin (n + 1)) R)
                            (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S) (MvPolynomial.X ∘ Fin.succ))
                          Finset.univ ∪
                        r ^ s.sup m • s ∪
                      {r}) :
                  Set S))))
        (Subtype.mk (p := fun (a : S) ↦
          Membership.mem (γ := Subalgebra R S)
            (adjoin R
              (↑(Finset.image (α := Fin n)
                        (Function.comp (β := MvPolynomial (Fin (n + 1)) R) (⇑f : (a : MvPolynomial (Fin (n + 1)) R) → S)
                          (MvPolynomial.X ∘ Fin.succ))
                        Finset.univ ∪
                      r ^ s.sup m • s ∪
                    {r}) :
                Set S))
            a)
          x ⋯)
⊢ R'.val.range ≤
    Subalgebra.map R'.val
      (Subalgebra.restrictScalars R (S := MvPolynomial (Fin n) R) (integralClosure (MvPolynomial (Fin n) R) ↥R'))

Tactic:
simp +contextual only [Subalgebra.range_val, Algebra.adjoin_le_iff, Subalgebra.coe_map,
            Subalgebra.coe_val, Set.subset_def, SetLike.mem_coe, Algebra.mem_adjoin_of_mem,
            Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right, R']

Premises used: Set.subset_def, Set.mem_image, Subtype.exists, exists_eq_right, Subalgebra.range_val, exists_and_right, Subalgebra.coe_val, Subalgebra.coe_map, Algebra.mem_adjoin_of_mem, Algebra.adjoin_le_iff, SetLike.mem_coe