-- 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 :
  (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)
⊢ 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) (↑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
Cleared hypotheses: this