-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_span_singleton [Module.Finite ℚ K] (x : K) :
    absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ x)|

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

Tactic:
have : IsDomain K := IsFractionRing.isDomain R

Result:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| ≠ 0

Tactic:
rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]

Result:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ¬↑d = 0

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑((Algebra.norm ℤ) ?m.176908) = (algebraMap ℤ ℚ) ((Algebra.norm ℤ) ?m.178170)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ¬↑d = 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ d • ↑(spanSingleton R⁰ x) = Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Tactic:
ext

Result:
case intro.intro.h
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
x✝ : K
⊢ x✝ ∈ d • ↑(spanSingleton R⁰ x) ↔ x✝ ∈ Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Proof state:
case intro.intro.h
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
x✝ : K
⊢ x✝ ∈ d • ↑(spanSingleton R⁰ x) ↔ x✝ ∈ Submodule.map (Algebra.linearMap R K) (Ideal.span {r})

Tactic:
simp_rw [← SetLike.mem_coe, Submodule.coe_pointwise_smul, Set.mem_smul_set, SetLike.mem_coe,
  mem_coe, mem_spanSingleton, Submodule.mem_map, Algebra.linearMap_apply, Submonoid.smul_def,
  Ideal.mem_span_singleton', exists_exists_eq_and, _root_.map_mul, hr, ← Algebra.smul_def,
  smul_comm (d : R)]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑(Ideal.absNorm (Ideal.span {r})) / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

Tactic:
rw [Ideal.absNorm_span_singleton]

Result:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑((Algebra.norm ℤ) r).natAbs / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

Proof state:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ |(Algebra.norm ℚ) ((algebraMap R K) r)| / |(Algebra.norm ℚ) ((algebraMap R K) ↑d)| = |(Algebra.norm ℚ) x|

Tactic:
rw [hr, Algebra.smul_def, _root_.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 _)]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

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

Result:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ ↑(Ideal.absNorm (Ideal.span {r})) / ↑|(Algebra.norm ℤ) ↑d| = |(Algebra.norm ℚ) x|

case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDedekindDomain R
inst✝⁷ : Module.Free ℤ R
inst✝⁶ : Module.Finite ℤ R
K : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝¹ : Algebra ℚ K
inst✝ : Module.Finite ℚ K
x : K
this : IsDomain K
d : ↥R⁰
r : R
hr : (algebraMap R K) r = ↑d • x
⊢ d • ↑(spanSingleton R⁰ x) = Submodule.map (Algebra.linearMap R K) (Ideal.span {r})