-- Mathlib/NumberTheory/NumberField/ProductFormula.lean
theorem FinitePlace.prod_eq_inv_abs_norm {x : K} (h_x_nezero : x ≠ 0) :
    ∏ᶠ w : FinitePlace K, w x = |(Algebra.norm ℚ) x|⁻¹

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Tactic:
have ha : a ≠ 0 := by
  rintro rfl
  simp at h_x_nezero

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Proof state:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)) * ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℤ) a)

Tactic:
norm_cast

Result:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) * ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℤ) a)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ↑((Algebra.norm ℤ) b) ≠ 0

Tactic:
simp [hb]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b : 𝓞 K
hb : b ≠ 0
h_x_nezero : (algebraMap (𝓞 K) K) 0 / (algebraMap (𝓞 K) K) b ≠ 0
⊢ False

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / |↑((Algebra.norm ℤ) b)|⁻¹ =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹

Tactic:
rw [← inv_eq_iff_eq_inv, inv_inv_div_inv, ← abs_div]

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b)| =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|

Proof state:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))

Tactic:
have hb₀ : ((Algebra.norm ℤ) b : ℝ) ≠ 0 := by simp [hb]

Result:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ ↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b)| =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|

Tactic:
congr

Result:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b : 𝓞 K
hb : b ≠ 0
h_x_nezero : (algebraMap (𝓞 K) K) 0 / (algebraMap (𝓞 K) K) b ≠ 0
⊢ False

Tactic:
simp at h_x_nezero

Result:
no goals

Proof state:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) * ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℤ) a)

Tactic:
rw [coe_norm_int a, coe_norm_int b, ← MonoidHom.map_mul, div_mul_cancel₀ _
  (RingOfIntegers.coe_ne_zero_iff.mpr hb)]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w x = ↑|(Algebra.norm ℚ) x|⁻¹

Tactic:
rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Tactic:
apply nonZeroDivisors.ne_zero at hb

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Proof state:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ ↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))

Tactic:
refine (eq_div_of_mul_eq hb₀ ?_).symm

Result:
case intro.intro.intro.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ ↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)) * ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℤ) a)

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Tactic:
simp_rw [map_div₀, Rat.cast_inv, Rat.cast_abs, finprod_div_distrib (mulSupport_finite_int ha)
  (mulSupport_finite_int hb), prod_eq_inv_abs_norm_int ha, prod_eq_inv_abs_norm_int hb]

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / |↑((Algebra.norm ℤ) b)|⁻¹ =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹