-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (goal)
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 :
  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)
          (I + J)) *
      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)
          (I ⊓ J)) =
    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)
          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)
⊢ 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 a : (I ⊓ J) * (I + J) *
    HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (β := 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)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : 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))
      (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) =
  I * J *
    HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
      (HMul.hMul (β := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_2, u_3} (R := A) A⁰ K) (β := 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)
          (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑I.den : A)) : 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))
      (spanSingleton A⁰ ((algebraMap A K : (a : A) → K) (↑J.den : A)) : FractionalIdeal.{u_2, u_3} (R := A) A⁰ K)
Tactic: simp only [FractionalIdeal.sup_eq_add, _root_.map_mul, ← spanSingleton_mul_spanSingleton]