awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
simp_rw :
  HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2 * ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
have simp_rw₁ : HMul.hMul (α := ℝ≥0∞) (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2)
      (∏ x : { w : InfinitePlace K // w.IsComplex }, (↑pi : ℝ≥0∞)) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ 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) *
      (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
Tactic: simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
simp_rw :
  HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2 * ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
simp_rw₁ :
  HMul.hMul (α := ℝ≥0∞) (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal 2)
        (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      HMul.hMul (α := ℝ≥0∞)
        (∏ x : { w : InfinitePlace K // w.IsComplex },
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2)
        (∏ x : { w : InfinitePlace K // w.IsComplex }, (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
have simp_rw₂ : (ENNReal.ofReal 2 ^ Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsReal }) Finset.univ *
      ∏ 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) *
      (↑pi : ℝ≥0∞) ^ Finset.card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) Finset.univ) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ 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) *
      (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
Tactic: simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
⊢ (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have simp_rw : (↑(convexBodyLTFactor K) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥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) =
  (↑(convexBodyLTFactor K) : ℝ≥0∞) *
    (↑(HMul.hMul (α := ℝ≥0)
          (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
          (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)) :
      ℝ≥0∞)
Tactic: simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
simp_rw :
  (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑(HMul.hMul (α := ℝ≥0)
            (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
            (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)) :
        ℝ≥0∞)
⊢ (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have simp_rw₁ : (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥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) =
  (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥0∞) *
    ((↑(∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) : ℝ≥0∞) *
      (↑(∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) : ℝ≥0∞))
Tactic: simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
simp_rw :
  (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      (↑(HMul.hMul (α := ℝ≥0)
            (∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)
            (∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult)) :
        ℝ≥0∞)
simp_rw₁ :
  (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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) =
    (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥0∞) *
      ((↑(∏ w : { w : InfinitePlace K // w.IsReal }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) : ℝ≥0∞) *
        (↑(∏ w : { w : InfinitePlace K // w.IsComplex }, f (↑w : InfinitePlace K) ^ (↑w : InfinitePlace K).mult) :
          ℝ≥0∞))
⊢ (↑(convexBodyLTFactor K) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥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) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have simp_rw₂ : (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥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) =
  (↑(HPow.hPow (α := ℝ≥0) 2 (nrRealPlaces K)) : ℝ≥0∞) * (↑(pi ^ nrComplexPlaces K) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥0∞)
      (∏ a : { w : InfinitePlace K // w.IsReal }, (↑(f (↑a : InfinitePlace K) ^ (↑a : InfinitePlace K).mult) : ℝ≥0∞))
      (∏ a : { w : InfinitePlace K // w.IsComplex }, (↑(f (↑a : InfinitePlace K) ^ (↑a : InfinitePlace K).mult) : ℝ≥0∞))
Tactic: simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have _ : ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
  HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
Tactic: calc
    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ∏ x : {w // InfinitePlace.IsComplex w}, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K
          * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)))
          * ((∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) *
            NNReal.pi ^ nrComplexPlaces K) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
    _ = (convexBodyLTFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, .ofReal (f x.val)) *
        (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
      simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
      ring
    _ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
_ :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have _₁ : HMul.hMul (α := ℝ≥0∞)
    (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
    (∏ x : { w : InfinitePlace K // w.IsComplex },
      HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
  ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ 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) *
      (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
Tactic: calc
    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ∏ x : {w // InfinitePlace.IsComplex w}, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K
          * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)))
          * ((∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) *
            NNReal.pi ^ nrComplexPlaces K) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
    _ = (convexBodyLTFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, .ofReal (f x.val)) *
        (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
      simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
      ring
    _ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
_ :
  ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞))
_₁ :
  HMul.hMul (α := ℝ≥0∞)
      (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (2 * (↑(f (↑x : InfinitePlace K)) : ℝ)))
      (∏ x : { w : InfinitePlace K // w.IsComplex },
        HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2 * (↑pi : ℝ≥0∞)) =
    ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ 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) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K)
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) (convexBodyLT K f) =
    (↑(convexBodyLTFactor K) : ℝ≥0∞) * (↑(∏ w : InfinitePlace K, f w ^ w.mult) : ℝ≥0∞)
have _₂ : ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
      ∏ 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) *
      (↑pi : ℝ≥0∞) ^ nrComplexPlaces K) =
  (↑(convexBodyLTFactor K) : ℝ≥0∞) *
    HMul.hMul (α := ℝ≥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: calc
    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
          ∏ x : {w // InfinitePlace.IsComplex w}, ENNReal.ofReal (f x.val) ^ 2 * NNReal.pi := by
      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball, Complex.volume_ball]
    _ = ((2 : ℝ≥0) ^ nrRealPlaces K
          * (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)))
          * ((∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2) *
            NNReal.pi ^ nrComplexPlaces K) := by
      simp_rw [ofReal_mul (by simp : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
        Finset.card_univ, ofReal_ofNat, ofReal_coe_nnreal, coe_ofNat]
    _ = (convexBodyLTFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, .ofReal (f x.val)) *
        (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
      simp_rw [convexBodyLTFactor, coe_mul, ENNReal.coe_pow]
      ring
    _ = (convexBodyLTFactor K) * ∏ w, (f w) ^ (mult w) := by
      simp_rw [prod_eq_prod_mul_prod, coe_mul, coe_finsetProd, mult_isReal, mult_isComplex,
        pow_one, ENNReal.coe_pow, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B
have refine_1 : ∀ (w : InfinitePlace K),
  w ≠ w₁ →
    Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w = f w
Tactic: refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
refine_1 :
  ∀ (w : InfinitePlace K),
    w ≠ w₁ →
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w =
        f w
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B
have refine_2 : ∏ w : InfinitePlace K,
    Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
      w.mult =
  B
Tactic: refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
w : InfinitePlace K
hw : w ∈ Finset.erase Finset.univ w₁
⊢ Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
      w.mult =
    f w ^ w.mult
have rw : f w ^ w.mult = f w ^ w.mult
Tactic: rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∏ w : InfinitePlace K,
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
        w.mult =
    B
have refine_2 : S ≠ 0
Tactic: rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_self,
      Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)],
      ← NNReal.rpow_natCast, ← NNReal.rpow_mul, inv_mul_cancel₀, NNReal.rpow_one, mul_assoc,
      inv_mul_cancel₀, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
refine_2 : S ≠ 0
⊢ ∏ w : InfinitePlace K,
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
        w.mult =
    B
have refine_2₁ : Ne (α := ℝ) (↑w₁.mult : ℝ) 0
Tactic: rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_self,
      Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)],
      ← NNReal.rpow_natCast, ← NNReal.rpow_mul, inv_mul_cancel₀, NNReal.rpow_one, mul_assoc,
      inv_mul_cancel₀, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ S ≠ 0
have refine_2 : ∀ a ∈ Finset.erase Finset.univ w₁, f a ^ a.mult ≠ 0
Tactic: rw [Finset.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ Ne (α := ℝ) (↑(if w₁.IsReal then 1 else 2) : ℝ) 0
have pos : w₁.IsReal → Ne (α := ℝ) (↑1 : ℝ) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
pos : w₁.IsReal → Ne (α := ℝ) (↑1 : ℝ) 0
⊢ Ne (α := ℝ) (↑(if w₁.IsReal then 1 else 2) : ℝ) 0
have neg : ¬w₁.IsReal → Ne (α := ℝ) (↑2 : ℝ) 0
Tactic: split_ifs