-- 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 : 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)) ⋯
⊢ ZariskisMainProperty R (S := ↥R') (Ideal.under (↥R') p)

Tactic:
have := IH (R := R) (S := R') (p.under R') φ <| by
      refine RingHom.finite_iff_isIntegral_and_finiteType.mpr ⟨?_, ?_⟩
      · letI := φ.toAlgebra
        have : IsScalarTower (MvPolynomial (Fin n) R) R' S := .of_algebraMap_eq' <| by
          ext <;> simp [φ, (f'.toRingHom.comp C).algebraMap_toAlgebra, φ.algebraMap_toAlgebra, f',
            MvPolynomial.finSuccEquiv, MvPolynomial.optionEquivLeft]
        refine algebraMap_isIntegral_iff.mpr (integralClosure_eq_top_iff.mp ?_)
        apply Subalgebra.restrictScalars_injective R
        rw [← (Subalgebra.map_injective (f := R'.val) Subtype.val_injective).eq_iff]
        simp only [Subalgebra.restrictScalars_top, Algebra.map_top]
        refine le_antisymm (Set.image_subset_range _ _) ?_
        suffices (∀ (a : Fin n), IsIntegral (MvPolynomial (Fin n) R) (f (MvPolynomial.X a.succ))) ∧
            ∀ a ∈ s, IsIntegral (MvPolynomial (Fin n) R) (r ^ s.sup m * a) by
          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']
          simpa [R', mem_integralClosure_iff,
            ← isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective R' S),
            forall_and, hr, or_imp, Finset.mem_smul_finset]
        refine ⟨fun i ↦ ?_, fun a has ↦ ?_⟩
        · convert! isIntegral_algebraMap (x := MvPolynomial.X i)
          simp [RingHom.algebraMap_toAlgebra, f', MvPolynomial.finSuccEquiv,
            MvPolynomial.optionEquivLeft]
        · rw [← Nat.sub_add_cancel (s.le_sup has), pow_add, mul_assoc]
          exact (hr.pow _).mul (hm _)
      · refine .of_comp_finiteType (f := algebraMap R _) ?_
        rw [AlgHom.toRingHom_eq_coe, φ.comp_algebraMap, RingHom.finiteType_algebraMap]
        exact ⟨(Subalgebra.fg_top _).mpr ⟨_, rfl⟩⟩