-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsFractionRing A K
inst_12 : IsIntegrallyClosed A
inst_13 : FiniteDimensional K L
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsSeparable K L
inst_16 : IsDomain A
inst_17 : IsFractionRing B L
inst_18 : Nontrivial B
inst_19 : NoZeroDivisors B
I : FractionalIdeal.{u_3, u} (R := B) B⁰ L
hI : ¬I = 0
have have₁ have₂ :
  ∀ (s : Finset L) (b : Basis (↥s) K L) (hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)),
    IsFractional B⁰ (↑I : Submodule B L)ᵛ
have₃ :
  ∀ (s : Finset L) (b : Basis (↥s) K L) (hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)) (x : B)
    (hx : x ≠ 0) (hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)),
    IsFractional B⁰ (↑I : Submodule B L)ᵛ
have₄ :
  ∀ (s : Finset L) (b : Basis (↥s) K L) (hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)) (x : B)
    (hx : x ≠ 0) (hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)) (y : B)
    (hy :
      Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
        ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L)),
    IsFractional B⁰ (↑I : Submodule B L)ᵛ
refine_1 :
  ∀ (s : Finset L) (b : Basis (↥s) K L) (hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)) (x : B)
    (hx : x ≠ 0) (hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)) (y : B)
    (hy :
      Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
        ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L)),
    y ≠ 0
⊢ IsFractional B⁰ (↑I : Submodule B L)ᵛ
have refine_2 : ∀ (s : Finset L) (b : Basis (↥s) K L) (hb : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)) (x : B)
  (hx : x ≠ 0) (hx' : Membership.mem (α := L) I ((algebraMap B L : (a : B) → L) x : L)) (y : B)
  (hy :
    Eq.{u + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L)
      ((algebraMap K L : (a : K) → L) (discr.{u_2, u, u} (ι := ↥s) K (B := L) (⇑b : (a : ↥s) → L)) : L))
  (z : L) (hz : z ∈ (↑I : Submodule B L)ᵛ), IsInteger B ((y * x) • z)
Tactic: classical
    have ⟨s, b, hb⟩ := FiniteDimensional.exists_is_basis_integral A K L
    obtain ⟨x, hx, hx'⟩ := exists_ne_zero_mem_isInteger hI
    have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp
      (IsIntegral.algebraMap (B := L) (discr_isIntegral K hb))
    refine ⟨y * x, mem_nonZeroDivisors_iff_ne_zero.mpr (mul_ne_zero ?_ hx), fun z hz ↦ ?_⟩
    · rw [← (IsIntegralClosure.algebraMap_injective B A L).ne_iff, hy, map_zero,
        ← (algebraMap K L).map_zero, (algebraMap K L).injective.ne_iff]
      exact discr_not_zero_of_basis K b
    · convert! isIntegral_discr_mul_of_mem_traceDual I hb hx' hz using 1
      · ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
      · rw [Algebra.smul_def, map_mul, hy, ← Algebra.smul_def]