-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (hypothesis)
Goal:
A : Type u_2
K : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : IsDedekindDomain A
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
I J : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K
this :
  (Ideal.span {(↑J.den : A)} * I.num ⊔ Ideal.span {(↑I.den : A)} * J.num) *
      (Ideal.span {(↑J.den : A)} * I.num ⊓ Ideal.span {(↑I.den : A)} * J.num) =
    Ideal.span {(↑J.den : A)} * I.num * (Ideal.span {(↑I.den : A)} * J.num)
⊢ Eq.{u_3 + 1} (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
    ((fun (a : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) a
          (spanSingleton A⁰
              ((algebraMap A K : (a : A) → K) ((↑I.den : A) * (↑I.den : A) * (↑J.den : A) * (↑J.den : A))) :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K))
      ((I ⊓ J) * (I ⊔ J)))
    ((fun (a : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) ↦
        HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) a
          (spanSingleton A⁰
              ((algebraMap A K : (a : A) → K) ((↑I.den : A) * (↑I.den : A) * (↑J.den : A) * (↑J.den : A))) :
            FractionalIdeal.{u_2, u_3} (R := A) A⁰ K))
      (I * J))
have this₁ : (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          I) +
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          J)) *
    (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          I) ⊓
      HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
          J)) =
  HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) I) *
    HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) J)
Tactic: simp only [← coeIdeal_inj (K := K), coeIdeal_mul, coeIdeal_sup, coeIdeal_inf,
    ← den_mul_self_eq_num', coeIdeal_span_singleton] at this
Cleared hypotheses: this