-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
ha_ne_zero : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {a})) 0
hJ_ne_zero : Ne (α := Associates (Ideal R)) (Associates.mk J) 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' :
  I' =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a')⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
ha'_ne_zero : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {a'})) 0
hJ'_ne_zero : Ne (α := Associates (Ideal R)) (Associates.mk J') 0
rw :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      I' =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₁ :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a')⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        ((↑J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₂ :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal R⁰ K) *
        HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
          (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a')⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
          ((↑J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₃ :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
          (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a')⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
          ((↑J' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
        (↑J : FractionalIdeal R⁰ K)) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₄ :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a')⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
          (↑J : FractionalIdeal R⁰ K))) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₅ :
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
        (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a')⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
        (↑J : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₆ :
  spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
        (↑J : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
rw₇ :
  spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
        (↑J : FractionalIdeal R⁰ K) =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J : FractionalIdeal R⁰ K)
        (↑J' : FractionalIdeal R⁰ K))
rw₈ :
  spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
        (↑J : FractionalIdeal R⁰ K) =
    spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) a' : K))⁻¹ *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J : FractionalIdeal R⁰ K) (↑J' : FractionalIdeal R⁰ K)
rw₉ :
  spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
        (↑J : FractionalIdeal R⁰ K) =
    spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J : FractionalIdeal R⁰ K) (↑J' : FractionalIdeal R⁰ K)
rw₁₀ rw₁₁ :
  spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K)
        (↑J : FractionalIdeal R⁰ K) =
    spanSingleton R⁰
        (HMul.hMul (α := K) (β := K) (((algebraMap R K : (a : R) → K) a)⁻¹ : K)
          (((algebraMap R K : (a : R) → K) a')⁻¹ : K)) *
      HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K) (↑J : FractionalIdeal R⁰ K)
⊢ I * I' =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) (a * a'))⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑(J * J') : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)

Tactic:
rw [haJ, haJ', mul_assoc, mul_comm (J : FractionalIdeal R⁰ K), mul_assoc, ← mul_assoc,
      spanSingleton_mul_spanSingleton, coeIdeal_mul, map_mul, mul_inv,
      mul_comm (J : FractionalIdeal R⁰ K)]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, mul_inv, mul_assoc, FractionalIdeal.coeIdeal_mul, map_mul, mul_comm, FractionalIdeal.coeIdeal