-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
have 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))
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]