-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
lemma embedding_mul_absNorm (v : HeightOneSpectrum (𝓞 K)) {x : 𝓞 (WithVal (v.valuation K))}
    (h_x_nezero : x ≠ 0) : ‖embedding v x‖ * absNorm (v.maxPowDividing (span {x})) = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ‖(embedding v) ↑x‖ * ↑(absNorm (v.maxPowDividing (span {x}))) = 1

Tactic:
rw [maxPowDividing, map_pow, Nat.cast_pow, norm_def, adicAbv_def,
  WithZeroMulInt.toNNReal_neg_apply _
    ((v.valuation K).ne_zero_iff.mpr (coe_ne_zero_iff.mpr h_x_nezero))]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ↑(↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (WithZero.unzero ⋯)) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ Multiplicative.toAdd (WithZero.unzero ⋯) + ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors) = 0

Tactic:
simp [valuation_eq_intValuationDef, intValuationDef_if_neg, h_x_nezero]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ↑(↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (WithZero.unzero ⋯)) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Tactic:
push_cast

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (WithZero.unzero ⋯) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^ Multiplicative.toAdd (WithZero.unzero ⋯) *
      ↑(absNorm v.asIdeal) ^ (Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors =
    1

Tactic:
rw [← zpow_natCast, ← zpow_add₀ <| mod_cast (zero_lt_one.trans (one_lt_absNorm_nnreal v)).ne']

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^
      (Multiplicative.toAdd (WithZero.unzero ⋯) +
        ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors)) =
    1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ ↑(absNorm v.asIdeal) ^
      (Multiplicative.toAdd (WithZero.unzero ⋯) +
        ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors)) =
    1

Tactic:
rw [zpow_eq_one_iff_right₀ (Nat.cast_nonneg' _) (mod_cast (one_lt_absNorm_nnreal v).ne')]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
h_x_nezero : x ≠ 0
⊢ Multiplicative.toAdd (WithZero.unzero ⋯) + ↑((Associates.mk v.asIdeal).count (Associates.mk (span {x})).factors) = 0