awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : ¬I = 0
⊢ spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) (↑I.den : R₁)) ≤ I⁻¹

Tactic:
exact spanSingleton_le_iff_mem.2 (den_mem_inv hI)

Premises used: Iff.mpr, FractionalIdeal.spanSingleton_le_iff_mem, FractionalIdeal.den_mem_inv
-- Module: Mathlib.RingTheory.FractionalIdeal.Inverse
Goal:
K : Type u_3
inst : Field K
R₁ : Type u_4
inst_1 : CommRing R₁
inst_2 : IsDomain R₁
inst_3 : Algebra R₁ K
inst_4 : IsFractionRing R₁ K
I : FractionalIdeal.{u_4, u_3} (R := R₁) R₁⁰ K
hI : I ≠ ⊥
⊢ ⊥ < I * I⁻¹

Tactic:
lt_of_lt_of_le (coeIdeal_ne_zero.2 (hI ∘ num_eq_zero_iff.1)).bot_lt I.num_le_mul_inv

Premises used: Iff.mpr, Function.comp, FractionalIdeal.num_le_mul_inv, Iff.mp, FractionalIdeal.num_eq_zero_iff, Ne.bot_lt, lt_of_lt_of_le, FractionalIdeal.coeIdeal_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
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
hd : Ne (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : 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)| : ℚ)

Tactic:
rw [div_eq_div_iff]

Premises used: div_eq_div_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 : 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₀
⊢ 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
-- 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 : 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₀))
⊢ 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)
-- 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 : 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)
⊢ 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

Premises used: SMulCommClass.smul_comm
-- 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 : 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)
h₁ :
  a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) I.den (Submodule.map (Algebra.linearMap R K) I₀)
⊢ a • I.den • (↑I : Submodule R K) = HSMul.hSMul (β := Submodule R K) a (Submodule.map (Algebra.linearMap R K) I.num)

Tactic:
rw [smul_comm] at h

Premises used: SMulCommClass.smul_comm
-- 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 : 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)| : ℚ)
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)) ⊥
⊢ 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'

Premises used: Submodule.ideal_span_singleton_smul, LinearMap.map_injective, Submodule.map_smul'', Function.Injective.eq_iff, Submonoid.smul_def, smul_eq_mul
-- 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 : 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
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)}) : ℕ)) :
      ℚ)
⊢ 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:
simp_rw [← Nat.cast_natAbs, ← Nat.cast_mul, ← Ideal.absNorm_span_singleton]

Premises used: Nat.cast_natAbs, Nat.cast_mul, 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
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)})) : ℚ)
rw₄ rw₅ :
  Eq (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) (I₀ * Ideal.span {(↑I.den : 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)}) : ℕ)) :
      ℚ)

Tactic:
rw [← map_mul, ← map_mul, mul_comm, ← h', mul_comm]

Premises used: map_mul, mul_comm
-- 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 : 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' :
  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:
LinearMap.ker_eq_bot.mpr (IsFractionRing.injective R K)

Premises used: Iff.mpr, LinearMap.ker_eq_bot, IsFractionRing.injective
-- 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 : 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' :
  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:
exact LinearMap.ker_eq_bot.mpr (IsFractionRing.injective R K)

Premises used: Iff.mpr, LinearMap.ker_eq_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
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₀
⊢ Ne (α := ℚ) (↑|(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 : 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₀
⊢ Ne (α := ℚ) (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑a : 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
rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : 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

Tactic:
rw [num_zero_eq, Submodule.zero_eq_bot, Ideal.absNorm_bot, Nat.cast_zero, zero_div]

Premises used: zero_div, FractionalIdeal.num_zero_eq, Submodule.zero_eq_bot, Nat.cast_zero, Ideal.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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
IsFractionRing.injective R K

Premises used: IsFractionRing.injective
-- 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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
exact IsFractionRing.injective R K

Premises used: IsFractionRing.injective
-- 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
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥R⁰) (β := Submodule R K) 1 (↑1 : Submodule R K) =
    Submodule.map (Algebra.linearMap R K) ⊤

Tactic:
simp [Submodule.one_eq_range]

Premises used: Submodule.one_eq_range
-- 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
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
rw₇ rw₈ : Eq (α := ℚ) 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

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]

Premises used: OneMemClass.coe_one, Ideal.absNorm_top, map_one, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, abs_one, Top.top, OfNat.ofNat, one_div_one, Nat.cast_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
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ 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
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
this : Eq (α := R →ₗ[R] K) (Algebra.linearMap R K) (AlgHom.toLinearMap (IsScalarTower.toAlgHom R R K))
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)
⊢ (I.den * J.den) • (↑(I * J) : Submodule R K) = Submodule.map (Algebra.linearMap R K) (I.num * J.num)

Tactic:
rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]

Premises used: FractionalIdeal.coe_mul, Submodule.map_mul, FractionalIdeal.den_mul_self_eq_num
-- Module: Mathlib.RingTheory.FractionalIdeal.Norm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
K : Type u_2
inst_4 : CommRing K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
this : Eq (α := R →ₗ[R] K) (Algebra.linearMap R K) (AlgHom.toLinearMap (IsScalarTower.toAlgHom R R K))
⊢ (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:
Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _

Premises used: Set.Mem, Submodule.mul_smul_mul_eq_smul_mul_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 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 : Submodule R K) * (↑J : Submodule R K)) =
    I.den • (↑I : Submodule R K) * J.den • (↑J : Submodule R K)

Tactic:
exact Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _

Premises used: Submodule.mul_smul_mul_eq_smul_mul_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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ (absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I =
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)

Tactic:
rfl

Premises used: 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 : 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)| : ℚ)
rw₃ 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)| : ℚ)
⊢ (absNorm : (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]

Premises used: MonoidWithZeroHom.coe_mk, FractionalIdeal.absNorm, ZeroHom.coe_mk, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm
-- 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 : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ 0 ≤
    HDiv.hDiv (α := ℚ) (↑((Ideal.absNorm : (a : Ideal R) → ℕ) I.num) : ℚ)
      (↑|(Algebra.norm ℤ : (a : R) → ℤ) (↑I.den : R)| : ℚ)

Tactic:
positivity
-- 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
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) ⊥ : ℚ) (0 : ℚ)

Tactic:
absNorm.map_zero'

Premises used: ZeroHom.map_zero', FractionalIdeal.absNorm, MonoidWithZeroHom.toZeroHom
-- 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
⊢ ZeroHom.toFun.{u_2, 0} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑absNorm : ZeroHom (FractionalIdeal R⁰ K) ℚ)
      1 =
    1

Tactic:
absNorm.map_one'

Premises used: FractionalIdeal.absNorm, MonoidWithZeroHom.map_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
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) 1 : ℚ) (1 : ℚ)

Tactic:
convert! absNorm.map_one'

Premises used: FractionalIdeal.absNorm, MonoidWithZeroHom.map_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 : IsDomain K
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
⊢ Eq (α := ℚ) ((absNorm : (a : FractionalIdeal R⁰ K) → ℚ) I : ℚ) (0 : ℚ) ↔ I = 0

Tactic:
⟨fun h ↦ zero_of_num_eq_bot zero_notMem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩

Premises used: FractionalIdeal.zero_of_num_eq_bot, FractionalIdeal.absNorm_bot, Eq.rec, Iff.intro, Eq.symm