-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * J.num)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑(I.den * J.den) : R)| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) *
      HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₁ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * J.num)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) ((↑I.den : R) * (↑J.den : R))| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) *
      HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₂ :
  HDiv.hDiv (α := ℚ)
      (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
            ((Ideal.absNorm : (a : Ideal R) → ℕ) J.num : ℕ)) :
        ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) ((↑I.den : R) * (↑J.den : R))| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) *
      HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₃ :
  HDiv.hDiv (α := ℚ)
      (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
            ((Ideal.absNorm : (a : Ideal R) → ℕ) J.num : ℕ)) :
        ℚ)
      (↑|HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)| :
        ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) *
      HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₄ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      (↑|HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)| :
        ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) *
      HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₅ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      (↑|HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)| :
        ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      HMul.hMul (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₆ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |(↑(HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)) :
          ℚ)| =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      HMul.hMul (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₇ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |(↑(HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)) :
          ℚ)| =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      HMul.hMul (α := ℚ) |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)
rw₈ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |(↑(HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)) :
          ℚ)| =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      HMul.hMul (α := ℚ) |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
        |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)) : ℚ)|
rw₉ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |(↑(HMul.hMul (α := ℤ) (β := ℤ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)
              ((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R) : ℤ)) :
          ℚ)| =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |HMul.hMul (α := ℚ) (↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)
          (↑((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)) : ℚ)|
rw₁₀ rw₁₁ :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |HMul.hMul (α := ℚ) (↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)
          (↑((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)) : ℚ)| =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ) /
      |HMul.hMul (α := ℚ) (↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)
          (↑((Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)) : ℚ)|
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I * J).num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑(I * J).den : R)| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) *
      HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) J.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑J.den : R)| : ℚ)

Tactic:
rw [absNorm_div_norm_eq_absNorm_div_norm (I.den * J.den) (I.num * J.num) (by
        have : Algebra.linearMap R K = (IsScalarTower.toAlgHom R R K).toLinearMap := rfl
        rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]
        exact Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _),
      Submonoid.coe_mul, map_mul, map_mul, Nat.cast_mul, div_mul_div_comm,
      Int.cast_abs, Int.cast_abs, Int.cast_abs, ← abs_mul, Int.cast_mul]

Premises used: FractionalIdeal.num, Int.cast_abs, HMul.hMul, div_mul_div_comm, abs_mul, map_mul, Int.cast_mul, FractionalIdeal.den, Nat.cast_mul, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, Submonoid.coe_mul