-- Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
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) (↑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)
⊢ 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)

Tactic:
rw [mul_left_comm, ← mul_add, ← mul_add, ← mul_inf₀ (FractionalIdeal.zero_le _),
    ← mul_inf₀ (FractionalIdeal.zero_le _)] at this

Premises used: mul_inf₀, mul_left_comm, mul_add