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
w₀ : { w : InfinitePlace K // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      Membership.mem (γ := Set ℂ)
        (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b = w₀ then
          {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
        else ball 0 (↑(f a) : ℝ))
        (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b))
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      Membership.mem (γ := Set ℂ)
        (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b = w₀ then
          {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
        else ball 0 (↑(f a) : ℝ))
        (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b))
have h : ∀ (a : InfinitePlace K) (a_1 : a.IsComplex),
  Membership.mem (γ := Set ℂ)
      (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a a_1 = w₀ then
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      else ball 0 (↑(f a) : ℝ))
      (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a a_1)) ↔
    Membership.mem (γ := Set ℂ)
      (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a a_1 = w₀ then
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      else ball 0 (↑(f a) : ℝ))
      (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a a_1))
Tactic: convert! hx using 3
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      Membership.mem (γ := Set ℂ)
        (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b = w₀ then
          {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
        else ball 0 (↑(f a) : ℝ))
        (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b))
a : InfinitePlace K
h : a.IsComplex
⊢ Membership.mem (γ := Set ℂ)
      (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ then
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      else ball 0 (↑(f a) : ℝ))
      (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)) ↔
    Membership.mem (γ := Set ℂ)
      (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ then
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      else ball 0 (↑(f a) : ℝ))
      (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h))
have pos : Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ →
  (Membership.mem (γ := Set ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)) ↔
    Membership.mem (γ := Set ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)))
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
w₀ : { w : InfinitePlace K // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      Membership.mem (γ := Set ℂ)
        (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b = w₀ then
          {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
        else ball 0 (↑(f a) : ℝ))
        (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b))
a : InfinitePlace K
h : a.IsComplex
pos :
  Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ →
    (Membership.mem (γ := Set ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
        (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)) ↔
      Membership.mem (γ := Set ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
        (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)))
⊢ Membership.mem (γ := Set ℂ)
      (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ then
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      else ball 0 (↑(f a) : ℝ))
      (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)) ↔
    Membership.mem (γ := Set ℂ)
      (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ then
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f a) : ℝ) 2}
      else ball 0 (↑(f a) : ℝ))
      (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h))
have neg : ¬Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h = w₀ →
  (Membership.mem (γ := Set ℂ) (ball 0 (↑(f a) : ℝ))
      (-x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)) ↔
    Membership.mem (γ := Set ℂ) (ball 0 (↑(f a) : ℝ))
      (x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a h)))
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
w₀ : { w : InfinitePlace K // w.IsComplex }
⊢ Convex ℝ (convexBodyLT' K f w₀)
have refine : ∀ (x : { w : InfinitePlace K // w.IsComplex }),
  Membership.mem (γ := Set { w : InfinitePlace K // w.IsComplex }) Set.univ x →
    Convex ℝ (E := ℂ)
      (if x = w₀ then {x_2 : ℂ | |x_2.re| < 1 ∧ |x_2.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
      else ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ))
Tactic: refine Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ x : { w : InfinitePlace K // w.IsComplex }
h : Membership.mem (γ := Set { w : InfinitePlace K // w.IsComplex }) Set.univ x
⊢ Convex ℝ (E := ℂ)
    (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)) : ℝ))
have pos : x = w₀ → Convex ℝ (E := ℂ) {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
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
w₀ x : { w : InfinitePlace K // w.IsComplex }
h : Membership.mem (γ := Set { w : InfinitePlace K // w.IsComplex }) Set.univ x
pos :
  x = w₀ →
    Convex ℝ (E := ℂ) {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
⊢ Convex ℝ (E := ℂ)
    (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)) : ℝ))
have neg : ¬x = w₀ → Convex ℝ (E := ℂ) (ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ))
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
w₀ x : { w : InfinitePlace K // w.IsComplex }
h : Membership.mem (γ := Set { w : InfinitePlace K // w.IsComplex }) Set.univ x
h_1 : x = w₀
⊢ Convex ℝ (E := ℂ) {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
have pos : Convex ℝ (E := ℂ)
  {x_1 : ℂ |
    (-1 < x_1.re ∧ x_1.re < 1) ∧
      -HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2 < x_1.im ∧
        x_1.im < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}
Tactic: simp_rw [abs_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
have rw : (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
    (Set.preimage (β := ℂ) (⇑Complex.measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ)
      {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2}) =
  4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
Tactic: rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
rw :
  (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞)
      (Set.preimage (β := ℂ) (⇑Complex.measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ)
        {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2}) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
⊢ (volume : (a : Set ℂ) → ℝ≥0∞) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have rw₁ : NullMeasurableSet (α := ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} volume
Tactic: rw [← (Complex.volume_preserving_equiv_real_prod.symm).measure_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
⊢ {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
    SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
have h : ∀ (x : ℝ × ℝ),
  Membership.mem (γ := Set (ℝ × ℝ)) {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} x ↔
    x ∈
      SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
x : ℝ × ℝ
⊢ Membership.mem (γ := Set (ℝ × ℝ)) {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} x ↔
    x ∈
      SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
have h : |x.1| < 1 ∧ |x.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2 ↔
  x ∈
    SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1) (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
Tactic: simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
x : ℝ × ℝ
h :
  |x.1| < 1 ∧ |x.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2 ↔
    x ∈
      SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
⊢ Membership.mem (γ := Set (ℝ × ℝ)) {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} x ↔
    x ∈
      SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
have h₁ : |x.1| < 1 ∧ |x.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2 ↔
  Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x.1 ∧
    x.2 ∈ Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)
Tactic: simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
inst_1 : NumberField K
B : ℝ≥0
x : ℝ × ℝ
h :
  |x.1| < 1 ∧ |x.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2 ↔
    x ∈
      SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
h₁ :
  |x.1| < 1 ∧ |x.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2 ↔
    Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x.1 ∧
      x.2 ∈ Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2)
⊢ Membership.mem (γ := Set (ℝ × ℝ)) {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} x ↔
    x ∈
      SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))
have h₂ : |x.1| < 1 ∧ |x.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2 ↔
  (-1 < x.1 ∧ x.1 < 1) ∧ -HPow.hPow (β := ℕ) (↑B : ℝ) 2 < x.2 ∧ x.2 < HPow.hPow (β := ℕ) (↑B : ℝ) 2
Tactic: simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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∞) {a : ℝ × ℝ | |a.1| < 1 ∧ |a.2| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have rw : (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: 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]]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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∞)
      (SProd.sprod (α := Set ℝ) (Set.Ioo (-1) 1)
        (Set.Ioo (-HPow.hPow (β := ℕ) (↑B : ℝ) 2) (HPow.hPow (β := ℕ) (↑B : ℝ) 2))) =
    4 * HPow.hPow (β := ℕ) (↑B : ℝ≥0∞) 2
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
⊢ (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
have simp_rw₂ : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 (-1)) *
    ENNReal.ofReal (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
⊢ (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
have simp_rw₃ : ENNReal.ofReal (HAdd.hAdd (α := ℝ) 1 1) *
    ENNReal.ofReal (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
⊢ (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
have simp_rw₄ : ENNReal.ofReal 2 * ENNReal.ofReal (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (goal)
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
⊢ (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
have simp_rw₅ : ENNReal.ofReal 2 * ENNReal.ofReal (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]