awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
simp_rw :
  (Measure.prod volume volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-1) 1) : ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) :
        ℝ≥0∞) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₂ :
  ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 - -HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₃ :
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
      ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₄ :
  ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2 + HPow.hPow (β := ℕ) (↑B : ℝ) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (2 * HPow.hPow (β := ℕ) (↑B : ℝ) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₆ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * ENNReal.ofReal (HPow.hPow (β := ℕ) (↑B : ℝ) 2)) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₇ :
  ENNReal.ofReal 2 * (ENNReal.ofReal 2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₈ : 2 * (2 * HPow.hPow (β := ℕ) (ENNReal.ofReal (↑B : ℝ)) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₉ : 2 * (2 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2) = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw₁₀ : HMul.hMul (α := ℝ≥0∞) 2 2 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2 = 4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2

Tactic:
simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]

Premises used: ENNReal.ofReal_mul, mul_assoc, two_mul, ENNReal.ofReal_ofNat, MeasureTheory.Measure.prod_prod, one_add_one_eq_two, MeasureTheory.Measure.volume_eq_prod, NNReal.coe_nonneg, ENNReal.ofReal_coe_nnreal, zero_le_two, Real.volume_Ioo, ENNReal.ofReal_pow, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ NullMeasurableSet (α := ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} volume

Tactic:
(MeasurableSet.inter ?_ ?_).nullMeasurableSet

Premises used: Set.Mem, MeasurableSet.nullMeasurableSet, setOf, Set.inter, MeasurableSet.inter
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
refine_1 : MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.re| 1
refine_2 : MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.im| (HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ NullMeasurableSet (α := ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} volume

Tactic:
refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasurableSet.inter
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.re| 1

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

Premises used: measurable_norm, Measurable.comp, abs, Complex.measurable_re, measurableSet_lt, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.re| 1

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

Premises used: measurable_norm, Measurable.comp, Complex.measurable_re, measurableSet_lt, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.im| (HPow.hPow (β := ℕ) (↑B : ℝ) 2)

Tactic:
measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const

Premises used: measurable_norm, Measurable.comp, abs, Complex.measurable_im, measurableSet_lt, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ MeasurableSet (α := ℂ) fun (x : ℂ) ↦ Real.lt✝ |x.im| (HPow.hPow (β := ℕ) (↑B : ℝ) 2)

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

Premises used: measurable_norm, Measurable.comp, Complex.measurable_im, measurableSet_lt, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
⊢ ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2

Tactic:
have vol_box : ∀ B : ℝ≥0, volume {x : ℂ | |x.re| < 1 ∧ |x.im| < B ^ 2} = 4 * B ^ 2 := by
    intro B
    rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
    · simp_rw [Set.preimage_setOf_eq, Complex.measurableEquivRealProd_symm_apply]
      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]]
      simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
        ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
        ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
    · refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
      · exact measurableSet_lt (measurable_norm.comp Complex.measurable_re) measurable_const
      · exact measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
simp_rw :
  HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ i : { w : InfinitePlace K // w.IsComplex },
        (volume : (a : Set ℂ) → ℝ≥0∞)
          (if i = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑i : InfinitePlace K)) : ℝ) 2}
          else ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT' K f w₀) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))

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

Premises used: MeasureTheory.volume_pi, Real.volume_ball, MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.volume_eq_prod, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
rw :
  (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (∏ x ∈ Finset.erase Finset.univ w₀,
            (volume : (a : Set ℂ) → ℝ≥0∞)
              (if x = w₀ then
                {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
              else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞)
        ((volume : (a : Set ℂ) → ℝ≥0∞)
            (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
            else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ i : { w : InfinitePlace K // w.IsComplex },
        (volume : (a : Set ℂ) → ℝ≥0∞)
          (if i = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑i : InfinitePlace K)) : ℝ) 2}
          else ball 0 (↑(f (↑i : InfinitePlace K)) : ℝ))) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))

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

Premises used: Finset.mem_univ, Finset.prod_erase_mul
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
e_a :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ w₀,
      (volume : (a : Set ℂ) → ℝ≥0∞)
        (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x ∈ Finset.erase Finset.univ w₀,
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
e_a₁ :
  (volume : (a : Set ℂ) → ℝ≥0∞)
      (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) =
    4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2
⊢ (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (∏ x ∈ Finset.erase Finset.univ w₀,
            (volume : (a : Set ℂ) → ℝ≥0∞)
              (if x = w₀ then
                {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
              else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞)
        ((volume : (a : Set ℂ) → ℝ≥0∞)
            (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
            else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) :
          ℝ≥0∞) =
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ))) *
      ((∏ x ∈ Finset.erase Finset.univ w₀,
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2))

Tactic:
congr 2
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ w₀,
      (volume : (a : Set ℂ) → ℝ≥0∞)
        (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x ∈ Finset.erase Finset.univ w₀,
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))

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

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
e_a :
  ∀ (w' : { w : InfinitePlace K // w.IsComplex }) (hw' : w' ∈ Finset.erase Finset.univ w₀),
    (volume : (a : Set ℂ) → ℝ≥0∞)
        (if w' = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w' : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ w₀,
      (volume : (a : Set ℂ) → ℝ≥0∞)
        (if x = w₀ then {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
        else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x ∈ Finset.erase Finset.univ w₀,
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))

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

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
w' : { w : InfinitePlace K // w.IsComplex }
hw' : w' ∈ Finset.erase Finset.univ w₀
e_a :
  (volume : (a : Set ℂ) → ℝ≥0∞) (ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
e_a₁ e_a₂ :
  HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)
⊢ (volume : (a : Set ℂ) → ℝ≥0∞)
      (if w' = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w' : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑w' : InfinitePlace K)) : ℝ)) =
    HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑w' : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)

Tactic:
rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]

Premises used: Finset.ne_of_mem_erase, Complex.volume_ball, if_neg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set ℂ) → ℝ≥0∞)
      (if w₀ = w₀ then {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑w₀ : InfinitePlace K)) : ℝ)) =
    4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2

Tactic:
simpa only [ite_true] using vol_box (f w₀)

Premises used: ite_true, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ LE.le (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ 4 = HPow.hPow (β := ℕ) (↑2 : ℝ≥0∞) 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
rw :
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (HPow.hPow (β := ℕ) (↑2 : ℝ≥0∞) 2 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)) =
    ((↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K) * HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * pi ^ (nrComplexPlaces K - 1)) :
          ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)
⊢ ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (4 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)) =
    ((↑(convexBodyLT'Factor K) : ℝ≥0∞) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2

Tactic:
rw [show (4 : ℝ≥0∞) = (2 : ℝ≥0) ^ 2 by norm_num, convexBodyLT'Factor, pow_add,
        ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀), ofReal_coe_nnreal]

Premises used: Finset.mem_univ, Finset.prod_erase_mul, pow_add, ENNReal.ofReal_coe_nnreal, NumberField.mixedEmbedding.convexBodyLT'Factor
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
vol_box :
  ∀ (B : ℝ≥0),
    (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
      4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
          (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        (HPow.hPow (β := ℕ) (↑2 : ℝ≥0∞) 2 * HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K * HPow.hPow (β := ℕ) (↑2 : ℝ≥0∞) 2 * (↑pi : ℝ≥0∞) ^ (nrComplexPlaces K - 1) *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x ∈ Finset.erase Finset.univ w₀, HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ≥0∞) 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x =
    ∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ 0 ≤ convexBodySumFun x

Tactic:
Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _))

Premises used: Iff.mpr, mul_nonneg, Nat.cast_pos, LT.lt.le, Finset.sum_nonneg, NumberField.InfinitePlace.mult_pos, NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
simp_rw :
  LE.le (α := ℝ)
    (∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (x + y) : ℝ))
    (∑ x_1 : InfinitePlace K,
      (↑x_1.mult : ℝ) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ)
          ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) y : ℝ))
⊢ convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y

Tactic:
simp_rw [convexBodySumFun, ← Finset.sum_add_distrib, ← mul_add]

Premises used: NumberField.mixedEmbedding.convexBodySumFun, Finset.sum_add_distrib, mul_add
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x y : mixedSpace K
⊢ LE.le (α := ℝ)
    (∑ w : InfinitePlace K,
      HMul.hMul (α := ℝ) (β := ℝ) ((↑w.mult : ℝ) : ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (x + y) : ℝ))
    (∑ x_1 : InfinitePlace K,
      (↑x_1.mult : ℝ) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ)
          ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) y : ℝ))

Tactic:
Finset.sum_le_sum
    fun _ _ ↦ mul_le_mul_of_nonneg_left (normAtPlace_add_le _ x y) (Nat.cast_pos.mpr mult_pos).le

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.le, NumberField.mixedEmbedding.normAtPlace_add_le, NumberField.InfinitePlace.mult_pos, Finset.sum_le_sum, mul_le_mul_of_nonneg_left