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
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 :
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
hb : Ne (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ)
have hd : Ne (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) 0
Tactic: rw [div_eq_div_iff]
-- 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 : 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₀
⊢ HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
have h₁ : Eq.{u_2 + 1} (α := Submodule R K) ((fun (x : Submodule R K) ↦ I.den • x) (a • (↑I : Submodule R K)))
  ((fun (x : Submodule R K) ↦ I.den • x) (Submodule.map (Algebra.linearMap R K) I₀))
Tactic: replace h := congr_arg (I.den • ·) h
Cleared hypotheses: h
-- 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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h :
  Eq.{u_2 + 1} (α := Submodule R K) ((fun (x : Submodule R K) ↦ I.den • x) (a • (↑I : Submodule R K)))
    ((fun (x : Submodule R K) ↦ I.den • x) (Submodule.map (Algebra.linearMap R K) I₀))
⊢ HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
have h' : Eq.{u_2 + 1} (α := Submodule R K) ((fun (x : Submodule R K) ↦ a • x) (I.den • (↑I : Submodule R K)))
  ((fun (x : Submodule R K) ↦ a • x) (Submodule.map (Algebra.linearMap R K) I.num))
Tactic: have h' := congr_arg (a • ·) (den_mul_self_eq_num I)
-- 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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : I.den • a • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) a (Submodule.map (Algebra.linearMap R K) I.num)
⊢ HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
have h₁ : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
Tactic: rw [smul_comm] at h
Cleared hypotheses: h, 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) a (Submodule.map (Algebra.linearMap R K) I.num)
⊢ HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
have rw : ∀ (h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num),
  HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
Tactic: rw [h, Submonoid.smul_def, Submonoid.smul_def, ← Submodule.ideal_span_singleton_smul,
      ← Submodule.ideal_span_singleton_smul, ← Submodule.map_smul'', ← Submodule.map_smul'',
      (LinearMap.map_injective ?_).eq_iff, smul_eq_mul, smul_eq_mul] 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) a (Submodule.map (Algebra.linearMap R K) I.num)
rw :
  ∀ (h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num),
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
      HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
        (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
⊢ HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
have rw₁ : ∀
  (h' :
    Eq (α := Submodule R K)
      (Submodule.map (Algebra.linearMap R K) (HSMul.hSMul (α := Ideal R) (Ideal.span {(↑I.den : R)}) I₀))
      (Submodule.map (Algebra.linearMap R K) (HSMul.hSMul (α := Ideal R) (Ideal.span {(↑a : R)}) I.num))),
  Eq (α := Submodule R R) (LinearMap.ker (Algebra.linearMap R K)) ⊥
Tactic: rw [h, Submonoid.smul_def, Submonoid.smul_def, ← Submodule.ideal_span_singleton_smul,
      ← Submodule.ideal_span_singleton_smul, ← Submodule.map_smul'', ← Submodule.map_smul'',
      (LinearMap.map_injective ?_).eq_iff, smul_eq_mul, smul_eq_mul] 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
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num
⊢ HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : R)| : ℚ) =
    HMul.hMul (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)
have simp_rw : Eq (α := ℚ)
  (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
        ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)}) : ℕ)) :
    ℚ)
  (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
        ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
    ℚ)
Tactic: simp_rw [← Nat.cast_natAbs, ← Nat.cast_mul, ← Ideal.absNorm_span_singleton]
-- 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.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num
⊢ Eq (α := ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)}) : ℕ)) :
      ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
have rw : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
  (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
        ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
    ℚ)
Tactic: rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
-- 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.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num
rw :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
⊢ Eq (α := ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)}) : ℕ)) :
      ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
have rw₁ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
Tactic: rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
-- 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.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num
rw :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
rw₁ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
⊢ Eq (α := ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)}) : ℕ)) :
      ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
have rw₂ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)} * I.num)) : ℚ)
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
Tactic: rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
-- 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.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num
rw :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
rw₁ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
rw₂ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)} * I.num)) : ℚ)
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
⊢ Eq (α := ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)}) : ℕ)) :
      ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
have rw₃ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)} * I₀)) : ℚ)
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
Tactic: rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
-- 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.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
h' : Ideal.span {(↑I.den : R)} * I₀ = Ideal.span {(↑a : R)} * I.num
rw :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
rw₁ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I.num * Ideal.span {(↑a : R)})) : ℚ)
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
rw₂ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)} * I.num)) : ℚ)
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
rw₃ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)} * I₀)) : ℚ)
    (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
⊢ Eq (α := ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I.num : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑a : R)}) : ℕ)) :
      ℚ)
    (↑(HMul.hMul (α := ℕ) (β := ℕ) ((Ideal.absNorm : (a : Ideal R) → ℕ) I₀ : ℕ)
          ((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {(↑I.den : R)}) : ℕ)) :
      ℚ)
have rw₄ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
  (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : R)})) : ℚ)
Tactic: rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]
-- 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
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (num.{u_1, u_2} (S := R⁰) (P := K) 0)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑(den.{u_1, u_2} (P := K) 0) : R)| : ℚ) =
    0
have rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
Tactic: rw [num_zero_eq, Submodule.zero_eq_bot, Ideal.absNorm_bot, Nat.cast_zero, zero_div]
-- 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
⊢ 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 : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) ⊤) : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) = 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 (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
⊢ 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₁ : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) = 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 (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
⊢ 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₂ : HDiv.hDiv (α := ℚ) 1 (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑1 : R)| : ℚ) = 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 (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
⊢ 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₃ : HDiv.hDiv (α := ℚ) 1 (↑|(Algebra.norm ℤ : (a : R) → ℤ) 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 (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
⊢ 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₄ : HDiv.hDiv (α := ℚ) 1 (↑|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 (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
⊢ 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₅ : HDiv.hDiv (α := ℚ) 1 (↑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 (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
⊢ 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₆ : 1 / 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]