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₀ : 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₀) : ℚ)
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₅ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑((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 (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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
⊢ Eq (α := ℚ)
    (|((Basis.det.{0, u_2, u_3} (R := ℚ) (M := K) (ι := ι)
                (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b) :
              K [⋀^ι]→ₗ[ℚ] ℚ) :
            (a : ι → K) → ℚ)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K)))| :
      ℚ)
    ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ)
have this : Nontrivial K
Tactic: have := IsFractionRing.nontrivial R K
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ Eq (α := ℚ)
    (|((Basis.det.{0, u_2, u_3} (R := ℚ) (M := K) (ι := ι)
                (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b) :
              K [⋀^ι]→ₗ[ℚ] ℚ) :
            (a : ι → K) → ℚ)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K)))| :
      ℚ)
    ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ)
have rw : |Matrix.det.{0, u_3} (n := ι)
      (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
        (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
          (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
  HDiv.hDiv (α := ℚ)
    |(↑(Matrix.det
            (b.toMatrix
              (Function.comp (β := ↥I.num) (Subtype.val (p := fun (x : R) ↦ x ∈ I.num))
                (⇑bI.num : (a : ι) → ↥I.num)))) :
        ℚ)|
    |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
Tactic: rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Nat.cast_natAbs, Int.cast_abs,
    Int.cast_abs, Basis.det_apply, Basis.det_apply]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ (RingHom.mapMatrix (algebraMap ℤ ℚ) : (a : Matrix ι ι ℤ) → Matrix ι ι ℚ)
      (b.toMatrix
        (Function.comp (β := ↥I.num) (Subtype.val (p := fun (x : R) ↦ x ∈ I.num)) (⇑bI.num : (a : ι) → ↥I.num))) =
    b₀.toMatrix
      (HSMul.hSMul (α := K) (β := ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
        (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
          (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))
have a : ∀ (i j : ι),
  (RingHom.mapMatrix (algebraMap ℤ ℚ) : (a : Matrix ι ι ℤ) → Matrix ι ι ℚ)
      (b.toMatrix
        (Function.comp (β := ↥I.num) (Subtype.val (p := fun (x : R) ↦ x ∈ I.num)) (⇑bI.num : (a : ι) → ↥I.num)))
      i j =
    b₀.toMatrix
      (HSMul.hSMul (α := K) (β := ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
        (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
          (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))
      i j
Tactic: ext : 2
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i j : ι
⊢ (RingHom.mapMatrix (algebraMap ℤ ℚ) : (a : Matrix ι ι ℤ) → Matrix ι ι ℚ)
      (b.toMatrix
        (Function.comp (β := ↥I.num) (Subtype.val (p := fun (x : R) ↦ x ∈ I.num)) (⇑bI.num : (a : ι) → ↥I.num)))
      i j =
    b₀.toMatrix
      (HSMul.hSMul (α := K) (β := ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
        (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
          (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))
      i j
have a : Eq (α := ℚ)
  ((((Basis.repr (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b) : (a : K) → ι →₀ ℚ)
            (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
              ((↑((bI : (a : ι) → ↥(↑I : Submodule R K)) j) : K) : K)) :
          ι →₀ ℚ) :
        (a : ι) → ℚ)
      i :
    ℚ)
  ((((b₀.repr : (a : K) → ι →₀ ℚ)
            (HMul.hMul (α := ι → K) (β := ι → K)
              ((algebraMap K (ι → K) : (a : K) → ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K) : ι → K)
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K)))
              j) :
          ι →₀ ℚ) :
        (a : ι) → ℚ)
      i :
    ℚ)
Tactic: simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
      ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
      Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
      Algebra.smul_def]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    HDiv.hDiv (α := ℚ) (β := ℚ)
      (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ)
            (Matrix.det
              (b.toMatrix
                (Function.comp (β := ↥I.num) (Subtype.val (p := fun (x : R) ↦ x ∈ I.num))
                  (⇑bI.num : (a : ι) → ↥I.num))))| :
        ℚ)
      (|(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)| : ℚ)
have rw : |Matrix.det.{0, u_3} (n := ι)
      (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
        (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
          (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
  |(b₀.toMatrix
          (HSMul.hSMul (α := K) (β := ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
            (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
              (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))).det| /
    |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
Tactic: rw [RingHom.map_det, show RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
      b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI)) by
    ext : 2
    simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
      ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
      Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
      Algebra.smul_def]
    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
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ Ne (α := ℚ) (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ)| : ℚ) (0 : ℚ)
have rw : ¬(↑I.den : R) = 0
Tactic: rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : IsDomain K
ι : Type u_3
inst_10 : Fintype ι
inst_11 : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
bI : Basis.{u_3, 0, u_2} ι ℤ ↥(↑I : Submodule R K)
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b
bI.num : Basis.{u_3, 0, u_1} ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |Matrix.det.{0, u_3} (n := ι)
        (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
          (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
            (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
    |(b₀.toMatrix
            (HSMul.hSMul (α := K) (β := ι → K) ((algebraMap R K : (a : R) → K) (↑I.den : R) : K)
              (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
                (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))).det| /
      |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
have rw : |Matrix.det.{0, u_3} (n := ι)
      (Basis.toMatrix (Basis.localizationLocalization.{0, 0, u_1, u_2, u_3} ℚ ℤ⁰ (A := R) K b)
        (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
          (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))| =
  |(HMul.hMul (α := Matrix ι ι ℚ) (β := Matrix ι ι ℚ)
          (((Algebra.leftMulMatrix b₀ : AlgHom.{0, u_2, u_3} ℚ K (Matrix ι ι ℚ)) : (a : K) → Matrix ι ι ℚ)
              ((algebraMap R K : (a : R) → K) (↑I.den : R)) :
            Matrix ι ι ℚ)
          (b₀.toMatrix
            (Function.comp (β := ↥(↑I : Submodule R K)) (Subtype.val (p := fun (x : K) ↦ x ∈ (↑I : Submodule R K)))
              (⇑bI : (a : ι) → ↥(↑I : Submodule R K))))).det| /
    |(↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ)|
Tactic: rw [Basis.toMatrix_smul, Matrix.det_mul, abs_mul, ← Algebra.norm_eq_matrix_det,
    Algebra.norm_localization ℤ ℤ⁰, show (Algebra.norm ℤ (den I : R) : ℚ) =
    algebraMap ℤ ℚ (Algebra.norm ℤ (den I : R)) by rfl, mul_div_assoc, mul_div_cancel₀ _ (by
    rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
    exact nonZeroDivisors.coe_ne_zero _)]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (spanSingleton R⁰ x) : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
have this : IsDomain K
Tactic: have : IsDomain K := IsFractionRing.isDomain R
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (spanSingleton R⁰ x) : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
have obtain : ∀ (d : ↥(R⁰ : Submonoid R)) (r : R) (hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x),
  Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (spanSingleton R⁰ x) : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
Tactic: obtain ⟨d, ⟨r, hr⟩⟩ := IsLocalization.exists_integer_multiple R⁰ x
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (spanSingleton R⁰ x) : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
have rw : HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {r})) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [absNorm_eq' d (Ideal.span {r})]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {r})) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (spanSingleton R⁰ x) : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)
have rw₁ : HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) =
  Submodule.map (Algebra.linearMap R K) (Ideal.span {r})
Tactic: rw [absNorm_eq' d (Ideal.span {r})]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {r})) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw : HDiv.hDiv (α := ℚ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : R) → ℤ) r)) : ℚ)
    (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [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
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ HDiv.hDiv (α := ℚ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : R) → ℤ) r)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have simp_rw : HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: simp_rw [Nat.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
      (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ Ne (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) (0 : ℚ)
have rw : ¬(↑d : R) = 0
Tactic: rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw : HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]
-- 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 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥(R⁰ : Submonoid R)
r : R
hr : (algebraMap R K : (a : R) → K) r = (↑d : R) • x
rw :
  HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((↑d : R) • x)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (β := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) r : K)| : ℚ)
      (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
have rw₁ : HDiv.hDiv (α := ℚ) (β := ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) (HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑d : R) : K) x)| : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap R K : (a : R) → K) (↑d : R) : K)| : ℚ) =
  |(Algebra.norm ℚ : (a : K) → ℚ) x|
Tactic: rw [hr, Algebra.smul_def, map_mul, abs_mul, mul_div_assoc, mul_div_cancel₀ _ (by
      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
      exact nonZeroDivisors.coe_ne_zero _)]