-- Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal R
x : S
hx : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x
A : Subalgebra R R[X] :=
  Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}
this : Algebra.{u_1, u_2} R[X] S[X] := algebra R S
zero :
  IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) 0) X)
add :
  ∀ (x y : S),
    Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x →
      Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) y →
        ∀
          (hx :
            IsIntegral.{u_1, u_2}
              (↥(Algebra.adjoin R
                  {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
              (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X))
          (hy :
            IsIntegral.{u_1, u_2}
              (↥(Algebra.adjoin R
                  {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
              (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) X)),
          IsIntegral.{u_1, u_2}
            (↥(Algebra.adjoin R
                {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (x + y) : S[X]) X)
mem :
  ∀ (x : S) (h : Membership.mem (γ := Set S) ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R)) x),
    IsIntegral.{u_1, u_2}
      (↥(Algebra.adjoin R
          {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
      (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)
smul :
  ∀ (a x : S),
    Membership.mem (γ := Submodule S S) (Submodule.span S ((⇑(algebraMap R S) : (a : R) → S) '' (↑I : Set R))) x →
      ∀
        (hx :
          IsIntegral.{u_1, u_2}
            (↥(Algebra.adjoin R
                {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)),
        IsIntegral.{u_1, u_2}
          (↥(Algebra.adjoin R
              {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (a • x) : S[X]) X)
⊢ IsIntegral.{u_1, u_2}
    (↥(Algebra.adjoin R {x : R[X] | ∃ r ∈ I, HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X = x}))
    (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) X)

Tactic:
induction hx using Submodule.span_induction with
  | zero => simp [isIntegral_zero]
  | add x y _ _ hx hy => simpa [add_mul] using hx.add hy
  | mem x h =>
    obtain ⟨x, hx, rfl⟩ := h
    simpa using isIntegral_algebraMap (R := A) (A := S[X])
      (x := ⟨C x * X, Algebra.subset_adjoin ⟨x, hx, rfl⟩⟩)
  | smul a x _ hx =>
    simp only [smul_eq_mul, map_mul, mul_assoc]
    refine .mul ?_ hx
    exact ((Algebra.IsIntegral.isIntegral (R := R) a).map (IsScalarTower.toAlgHom R S _)).tower_top

Premises used: add_mul, mul_assoc, map_mul, smul_eq_mul, isIntegral_zero, rfl