awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_7 : IsDomain K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
refine : ∀ (h : Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ)), I.num = ⊥
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ) ↔ I = 0

Tactic:
refine ⟨fun h ↦ zero_of_num_eq_bot zero_notMem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩
-- 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
inst_7 : IsDomain K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
h : Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ)
⊢ 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

Premises used: FractionalIdeal.absNorm_eq, div_eq_zero_iff
-- 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
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 = ⊥

Tactic:
Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_

Premises used: Nat.cast_eq_zero, Iff.mp, Ideal.absNorm_eq_zero_iff, Or.resolve_right
-- 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
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
refine : ¬Eq (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0
⊢ I.num = ⊥

Tactic:
refine Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_

Premises used: Nat.cast_eq_zero, Iff.mp, Ideal.absNorm_eq_zero_iff, Or.resolve_right
-- 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
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
⊢ ¬Eq (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ) 0

Tactic:
simp [Algebra.norm_eq_zero_iff]

Premises used: Algebra.norm_eq_zero_iff
-- 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₀ : Ideal R
rw : Eq (α := Submodule R K) (↑(↑I₀ : FractionalIdeal R⁰ K) : Submodule R K) (Submodule.map (Algebra.linearMap R K) I₀)
⊢ 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₀

Tactic:
rw [one_smul]

Premises used: one_smul
-- 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₀ : Ideal R
⊢ Eq (α := Submodule R K) (↑(↑I₀ : FractionalIdeal R⁰ K) : Submodule R K) (Submodule.map (Algebra.linearMap R K) I₀)

Tactic:
rfl
-- 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₀ : 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₀) : ℚ)
rw₅ rw₆ : Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I₀) : ℚ)
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (↑I₀ : FractionalIdeal R⁰ K) : ℚ)
    ((↑((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]

Premises used: FractionalIdeal.absNorm_eq', OneMemClass.coe_one, map_one, abs_one, OfNat.ofNat, div_one, Int.cast_one
-- 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
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)
⊢ Nontrivial K

Tactic:
have := IsFractionRing.nontrivial R K
-- 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
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 ⋯))
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)) : ℚ)|
⊢ 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 : ℚ)

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]

Premises used: FractionalIdeal.num, Int.cast_abs, Nat.cast_natAbs, FractionalIdeal.absNorm_eq, Ideal.natAbs_det_basis_change, Module.Basis.det_apply
-- 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
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 ⋯))
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
⊢ (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))))

Tactic:
ext : 2
-- 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
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 : ι
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 :
      ℚ)
⊢ (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:
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]

Premises used: LinearEquiv.restrictScalars_apply, RingHom.mapMatrix_apply, Rat, Matrix.map_apply, nonZeroDivisors, Int, Module.Basis.localizationLocalization_repr_algebraMap, Submonoid.smul_def, Module.Basis.toMatrix_apply, Module.Basis.map_apply, Algebra.smul_def, Function.comp_apply, FractionalIdeal.equivNum_apply
-- 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
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 : ι
⊢ 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:
rfl
-- 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
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 ⋯))
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)) : ℚ)|
⊢ |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)) : ℚ)| : ℚ)

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]

Premises used: RingHom.map_det
-- 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
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 (α := ℚ) ((↑((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)) : ℚ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R) : ℤ) : ℚ)

Tactic:
rfl
-- 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
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 ⋯))
rw : ¬(↑I.den : R) = 0
⊢ Ne (α := ℚ) (|(algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : R) → ℤ) (↑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]

Premises used: Algebra.norm_eq_zero_iff_of_basis, IsFractionRing.to_map_eq_zero_iff, ne_eq, abs_eq_zero
-- 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
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.den : R) = 0

Tactic:
nonZeroDivisors.coe_ne_zero _

Premises used: nonZeroDivisors.coe_ne_zero
-- 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
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.den : R) = 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

Premises used: nonZeroDivisors.coe_ne_zero
-- 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
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
⊢ IsDomain K

Tactic:
have : IsDomain K := IsFractionRing.isDomain R
-- 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
inst_7 : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst_8 : Algebra ℚ K
inst_9 : Module.Finite ℚ K
x : K
this : IsDomain K
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| : ℚ)
⊢ 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

Premises used: nonZeroDivisors, IsLocalization.exists_integer_multiple
-- 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
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|
rw₁ :
  HSMul.hSMul (β := Submodule R K) d (↑(spanSingleton R⁰ x) : Submodule R K) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {r})
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) (spanSingleton R⁰ x) : ℚ)
    (|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℚ)

Tactic:
rw [absNorm_eq' d (Ideal.span {r})]

Premises used: FractionalIdeal.absNorm_eq', Ideal.span, Singleton.singleton
-- 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
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 (α := ℚ) (↑(Int.natAbs ((Algebra.norm ℤ : (a : R) → ℤ) r)) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|
⊢ HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (Ideal.span {r})) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑d : R)| : ℚ) =
    |(Algebra.norm ℚ : (a : K) → ℚ) x|

Tactic:
rw [Ideal.absNorm_span_singleton]

Premises used: Ideal.absNorm_span_singleton
-- 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
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 (α := ℚ) ((↑((Algebra.norm ℤ : (a : ?m.124) → ℤ) ?m.129) : ℚ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : ?m.124) → ℤ) ?m.129 : ℤ) : ℚ)

Tactic:
rfl