-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodyLT'_volume :
    volume (convexBodyLT' K f w₀) = convexBodyLT'Factor K * ∏ w, (f w) ^ (mult w)

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x => Real.lt✝ |x.re| 1

Tactic:
exact measurableSet_lt (measurable_norm.comp Complex.measurable_re) measurable_const

Result:
no goals

Proof state:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ ∏ x ∈ Finset.univ.erase w₀,
      volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x)) =
    ∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)

Result:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
w' : { w // w.IsComplex }
hw' : w' ∈ Finset.univ.erase w₀
⊢ volume (if w' = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w') ^ 2} else ball 0 ↑(f ↑w')) =
    ENNReal.ofReal ↑(f ↑w') ^ 2 * ↑pi

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ i : { w // w.IsComplex }, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
rw [← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]

Result:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀,
          volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x))) *
        volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀))) =
    (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume {a | |a.1| < 1 ∧ |a.2| < ↑B ^ 2} = 4 * ↑B ^ 2

Tactic:
rw [show {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < B ^ 2} =
  Set.Ioo (-1 : ℝ) (1 : ℝ) ×ˢ Set.Ioo (- (B : ℝ) ^ 2) ((B : ℝ) ^ 2) by
    ext; simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]]

Result:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume (Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)) = 4 * ↑B ^ 2

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (↑2 ^ nrRealPlaces K * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) *
        (↑2 ^ 2 * ↑(f ↑w₀) ^ 2)) =
    (↑2 ^ nrRealPlaces K * ↑2 ^ 2 * ↑pi ^ (nrComplexPlaces K - 1) * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑(f ↑w₀) ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (convexBodyLT' K f w₀) =
    (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]

Result:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ i : { w // w.IsComplex }, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2)) =
    (↑2 ^ nrRealPlaces K * ∏ x : { w // w.IsReal }, ENNReal.ofReal ↑(f ↑x)) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ (nrComplexPlaces K - 1) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
simp_rw [ofReal_mul (by norm_num : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
  Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, ofReal_ofNat,
  ofReal_coe_nnreal, coe_ofNat]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀,
          volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x))) *
        volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀))) =
    (∏ x : { w // w.IsReal }, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
congr 2

Result:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ ∏ x ∈ Finset.univ.erase w₀,
      volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x)) =
    ∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2