-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
haveI haveI₁ haveI₂ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
pos :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : x = 0),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
neg neg₁ neg₂ neg₃ neg₄ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : ¬x = 0),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
neg₅ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : ¬x = 0),
    let L := FractionRing B;
    IsIntegral A
      (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
        (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
neg₆ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : ¬x = 0),
    let K := FractionRing A;
    let L := FractionRing B;
    let E := AlgebraicClosure L;
    IsIntegral A
      (HMul.hMul (α := E) (((algebraMap B E : (a : B) → E) x)⁻¹ : E)
        (HMul.hMul (α := E) ((algebraMap B E : (a : B) → E) x : E)
            ((aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E).erase
                ((algebraMap B E : (a : B) → E) x)).prod ^
          finrank (↥K⟮((algebraMap B L : (a : B) → L) x : L)⟯) L))
neg₇ neg₈ :
  ∀ (this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)) (hx : ¬x = 0),
    let K := FractionRing A;
    let L := FractionRing B;
    let E := AlgebraicClosure L;
    Membership.mem (α := E) (aroots (minpoly K (B := L) ((algebraMap B L : (a : B) → L) x : L)) E)
      ((algebraMap B E : (a : B) → E) x : E)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
classical
  haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  by_cases hx : x = 0
  · exact ⟨1, by simp [hx]⟩
  let K := FractionRing A
  let L := FractionRing B
  let E := AlgebraicClosure L
  suffices IsIntegral A ((algebraMap B L x)⁻¹ * (algebraMap A L (intNorm A B x))) by
    obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this
    refine ⟨y, ?_⟩
    apply FaithfulSMul.algebraMap_injective B L
    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
  rw [← isIntegral_algHom_iff (toAlgHom A L E)
    (FaithfulSMul.algebraMap_injective L E), coe_toAlgHom', map_mul, map_inv₀,
    algebraMap_apply A K L, algebraMap_intNorm (L := L), ← algebraMap_apply, ← algebraMap_apply,
    norm_eq_prod_roots _ (IsAlgClosed.splits _), ← Multiset.prod_erase
    (a := algebraMap B E x)]
  · have := IsTorsionFree.trans_faithfulSMul B L E
    rw [mul_pow, ← mul_pow_sub_one (Nat.pos_iff_ne_zero.1 Module.finrank_pos) (algebraMap B E x),
      mul_assoc, inv_mul_cancel_left₀]
    · refine IsIntegral.mul (IsIntegral.pow ?_ _)
        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
          (IsIntegral.isIntegral x), ?_⟩)) _)
      · exact (isIntegral_algebraMap_iff (isTorsionFree_iff_algebraMap_injective.1 this)).mpr
          (IsIntegral.isIntegral x)
      · replace ha := Multiset.erase_subset _ _ ha
        suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
        rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]
        simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha
        exact ha.2
    · exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
  · simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
    refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
    simp [algebraMap_apply B L E, aeval_algebraMap_apply]

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic, IsScalarTower.coe_toAlgHom', IsIntegral.mul, inv_mul_cancel_left₀, mul_assoc, Polynomial.IsRoot.def, map_inv₀, IsIntegral.pow, IsIntegral.multiset_prod, ne_eq, minpoly, map_mul, Polynomial.mem_roots', And.intro, Exists.intro, IsAlgClosed.splits, Algebra.norm_eq_prod_roots, Polynomial.eval_map_algebraMap, Polynomial.map_eq_zero, mul_pow, IsScalarTower.algebraMap_apply, Polynomial.aeval_algebraMap_apply