Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I + J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I ⊓ J))) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (I ⊓ J) * (I + J) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
          spanSingleton A⁰ ((algebraMap A K) ↑J.den) *
        spanSingleton A⁰ ((algebraMap A K) ↑J.den)) =
    I * J *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
          spanSingleton A⁰ ((algebraMap A K) ↑J.den) *
        spanSingleton A⁰ ((algebraMap A K) ↑J.den))

Tactic:
convert! this using 1

Goal state after:
case e'_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I + J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I ⊓ J))) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ (I ⊓ J) * (I + J) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
          spanSingleton A⁰ ((algebraMap A K) ↑J.den) *
        spanSingleton A⁰ ((algebraMap A K) ↑J.den)) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I + J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I ⊓ J)))

case e'_3
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
I J : FractionalIdeal A⁰ K
this :
  spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I + J)) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * (I ⊓ J))) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))
⊢ I * J *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * spanSingleton A⁰ ((algebraMap A K) ↑I.den) *
          spanSingleton A⁰ ((algebraMap A K) ↑J.den) *
        spanSingleton A⁰ ((algebraMap A K) ↑J.den)) =
    spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * I) *
      (spanSingleton A⁰ ((algebraMap A K) ↑I.den) * (spanSingleton A⁰ ((algebraMap A K) ↑J.den) * J))