awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) ⊤) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) = 1
rw₁ : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) = 1
rw₂ : HDiv.hDiv (α := ℚ) 1 (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) = 1
rw₃ : HDiv.hDiv (α := ℚ) 1 (↑|(Algebra.norm ℤ : (a : R) → ℤ) 1| : ℚ) = 1
rw₄ : HDiv.hDiv (α := ℚ) 1 (↑|1| : ℚ) = 1
rw₅ : HDiv.hDiv (α := ℚ) 1 (↑1 : ℚ) = 1
rw₆ : 1 / 1 = 1
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (num.{u_1, u_2} (S := R⁰) (P := K) 1)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑(den.{u_1, u_2} (P := K) 1) : R)| : ℚ) =
    1
have rw₇ : Eq (α := ℚ) 1 1
Tactic: rw [absNorm_div_norm_eq_absNorm_div_norm 1 ⊤ (by simp [Submodule.one_eq_range]),
      Ideal.absNorm_top, Nat.cast_one, OneMemClass.coe_one, map_one, abs_one,
      Int.cast_one,
      one_div_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (hypothesis)
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
⊢ (I.den * J.den) • (↑(I * J) : Submodule R K) = Submodule.map (Algebra.linearMap R K) (I.num * J.num)
have this : Eq (α := R →ₗ[R] K) (Algebra.linearMap R K) (AlgHom.toLinearMap (IsScalarTower.toAlgHom R R K))
Tactic: have : Algebra.linearMap R K = (IsScalarTower.toAlgHom R R K).toLinearMap := rfl
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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
this : Eq (α := R →ₗ[R] K) (Algebra.linearMap R K) (AlgHom.toLinearMap (IsScalarTower.toAlgHom R R K))
⊢ (I.den * J.den) • (↑(I * J) : Submodule R K) = Submodule.map (Algebra.linearMap R K) (I.num * J.num)
have rw : (I.den * J.den) • ((↑I : Submodule R K) * (↑J : Submodule R K)) =
  I.den • (↑I : Submodule R K) * J.den • (↑J : Submodule R K)
Tactic: rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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
⊢ 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)| : ℚ)
have 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)| : ℚ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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)| : ℚ)
⊢ 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)| : ℚ)
have 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)| : ℚ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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)| : ℚ)
⊢ 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)| : ℚ)
have 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)| : ℚ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • (↑I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀
⊢ (absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have rw : ({
        toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
          HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
            (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
        map_zero' := sorry, map_one' := sorry, map_mul' := sorry } :
      (a : FractionalIdeal R⁰ K) → ℚ)
    I =
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
Tactic: rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk,
    ZeroHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • (↑I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀
rw :
  ({
          toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
            HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
              (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : FractionalIdeal R⁰ K) → ℚ)
      I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
⊢ (absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have rw₁ : ({
        toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
          HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
            (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
        map_zero' := sorry, map_one' := sorry, map_mul' := sorry } :
      (a : FractionalIdeal R⁰ K) → ℚ)
    I =
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
Tactic: rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk,
    ZeroHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • (↑I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀
rw :
  ({
          toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
            HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
              (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : FractionalIdeal R⁰ K) → ℚ)
      I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
rw₁ :
  ({
          toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
            HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
              (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : FractionalIdeal R⁰ K) → ℚ)
      I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
⊢ (absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have rw₂ : ({
        toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
          HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
            (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
        map_zero' := sorry } :
      (a : FractionalIdeal R⁰ K) → ℚ)
    I =
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
Tactic: rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk,
    ZeroHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • (↑I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀
rw :
  ({
          toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
            HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
              (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : FractionalIdeal R⁰ K) → ℚ)
      I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
rw₁ :
  ({
          toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
            HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
              (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : FractionalIdeal R⁰ K) → ℚ)
      I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
rw₂ :
  ({
          toFun := fun (I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) ↦
            HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
              (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ),
          map_zero' := ⋯ } :
        (a : FractionalIdeal R⁰ K) → ℚ)
      I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
⊢ (absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have rw₃ : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) =
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
Tactic: rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk,
    ZeroHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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
inst_7 : IsDomain K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ) ↔ I = 0
have refine : ∀ (h : Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ)), I.num = ⊥
Tactic: refine ⟨fun h ↦ zero_of_num_eq_bot zero_notMem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (hypothesis)
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
inst_7 : IsDomain K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
h : Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ)
⊢ I.num = ⊥
have h₁ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ) 0 ∨
  Eq (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0
Tactic: rw [absNorm_eq, div_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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
inst_7 : IsDomain K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
h :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ) 0 ∨
    Eq (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0
⊢ I.num = ⊥
have refine : ¬Eq (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0
Tactic: refine Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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₀ : Ideal R
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥R⁰) (β := Submodule R K) 1 (↑(↑I₀ : FractionalIdeal R⁰ K) : Submodule R K) =
    Submodule.map (Algebra.linearMap R K) I₀
have rw : Eq (α := Submodule R K) (↑(↑I₀ : FractionalIdeal R⁰ K) : Submodule R K) (Submodule.map (Algebra.linearMap R K) I₀)
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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₀ : Ideal R
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (↑I₀ : FractionalIdeal R⁰ K) : ℚ)
    ((↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) : ℚ)
have rw : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) =
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
Tactic: rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, map_one, abs_one,
    Int.cast_one, _root_.div_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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₀ : Ideal R
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (↑I₀ : FractionalIdeal R⁰ K) : ℚ)
    ((↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) : ℚ)
have rw₁ : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) 1| : ℚ) =
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
Tactic: rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, map_one, abs_one,
    Int.cast_one, _root_.div_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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₀ : Ideal R
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
rw₁ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) 1| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (↑I₀ : FractionalIdeal R⁰ K) : ℚ)
    ((↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) : ℚ)
have rw₂ : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|1| : ℚ) =
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
Tactic: rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, map_one, abs_one,
    Int.cast_one, _root_.div_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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₀ : Ideal R
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
rw₁ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) 1| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
rw₂ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|1| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (↑I₀ : FractionalIdeal R⁰ K) : ℚ)
    ((↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) : ℚ)
have rw₃ : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑1 : ℚ) =
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
Tactic: rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, map_one, abs_one,
    Int.cast_one, _root_.div_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Norm (goal)
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₀ : Ideal R
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
rw₁ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) 1| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
rw₂ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|1| : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
rw₃ :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑1 : ℚ) =
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (↑I₀ : FractionalIdeal R⁰ K) : ℚ)
    ((↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) : ℚ)
have rw₄ : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) 1 = (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
Tactic: rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, map_one, abs_one,
    Int.cast_one, _root_.div_one]