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 }
x : K
h :
  (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
h₁ : ∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
h₂ :
  |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
    |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
      HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = (↑w₀ : InfinitePlace K)
neg : Membership.mem (α := ℂ) (γ := Set ℂ) (ball 0 (↑(f w) : ℝ)) ((w.embedding : (a : K) → ℂ) x : ℂ)
⊢ Membership.mem (α := ℂ) (γ := Set ℂ)
    (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w hw = w₀ then
      {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑(f w) : ℝ) 2}
    else ball 0 (↑(f w) : ℝ))
    ((w.embedding : (a : K) → ℂ) x : ℂ)

Tactic:
rw [if_neg (by exact Subtype.coe_ne_coe.1 h_ne)]

Premises used: 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 }
x : K
h :
  (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
h₁ : ∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
h₂ :
  |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
    |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
      HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = (↑w₀ : InfinitePlace K)
neg : (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ Membership.mem (α := ℂ) (γ := Set ℂ) (ball 0 (↑(f w) : ℝ)) ((w.embedding : (a : K) → ℂ) x : ℂ)

Tactic:
rw [mem_ball_zero_iff, norm_embedding_eq]

Premises used: NumberField.InfinitePlace.norm_embedding_eq, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
x : K
h :
  (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
h₁ : ∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
h₂ :
  |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
    |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
      HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = (↑w₀ : InfinitePlace K)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
h₁ w h_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
x : K
h :
  (∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)) ∧
    |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
        HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
h₁ : ∀ (w : InfinitePlace K), w ≠ (↑w₀ : InfinitePlace K) → (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
h₂ :
  |Complex.re (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| < 1 ∧
    |Complex.im (((↑w₀ : InfinitePlace K).embedding : (a : K) → ℂ) x)| <
      HPow.hPow (β := ℕ) (↑(f (↑w₀ : InfinitePlace K)) : ℝ) 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = (↑w₀ : InfinitePlace K)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
exact h₁ w h_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
x : mixedSpace K
hx : x ∈ convexBodyLT' K f w₀
simp :
  ∀
    (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))
⊢ -x ∈ convexBodyLT' K f w₀

Tactic:
simp only [Set.mem_prod, Set.mem_pi, Set.mem_univ, mem_ball, dist_zero_right, Real.norm_eq_abs,
    true_implies, Subtype.forall, Prod.fst_neg, Pi.neg_apply, norm_neg, Prod.snd_neg] at hx ⊢

Premises used: Prod.snd_neg, Prod.fst_neg, Subtype.forall, Set.mem_pi, Metric.mem_ball, Set.mem_prod, true_implies, norm_neg, Set.mem_univ, dist_zero_right, Pi.neg_apply, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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))

Tactic:
hx
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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))
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))
⊢ (∀ (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))

Tactic:
convert! hx using 3
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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)))
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)))
⊢ 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))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
h_1 : 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:
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 }
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
h_1 : ¬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:
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 }
⊢ Convex ℝ (convexBodyLT' K f w₀)

Tactic:
Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => ?_))

Premises used: convex_pi, convex_ball, Convex.prod, OfNat.ofNat, Subtype.val, NNReal.toReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w : InfinitePlace K // w.IsComplex }
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)) : ℝ))
⊢ Convex ℝ (convexBodyLT' K f w₀)

Tactic:
refine Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => ?_))

Premises used: convex_pi, convex_ball, Convex.prod
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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}
neg : ¬x = w₀ → Convex ℝ (E := ℂ) (ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ))
⊢ 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)) : ℝ))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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₀
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}
⊢ Convex ℝ (E := ℂ) {x_1 : ℂ | |x_1.re| < 1 ∧ |x_1.im| < HPow.hPow (β := ℕ) (↑(f (↑x : InfinitePlace K)) : ℝ) 2}

Tactic:
simp_rw [abs_lt]

Premises used: abs_lt
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℂ |
      (-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:
Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
      ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))

Premises used: Set.Mem, setOf, convex_halfSpace_im_gt, convex_halfSpace_im_lt, Set.inter, Convex.inter, convex_halfSpace_re_lt, convex_halfSpace_re_gt
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 : ℂ |
      (-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:
refine Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
      ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))

Premises used: convex_halfSpace_im_gt, convex_halfSpace_im_lt, Convex.inter, convex_halfSpace_re_lt, convex_halfSpace_re_gt
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 := ℂ) (ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ))

Tactic:
convex_ball _ _

Premises used: convex_ball
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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 := ℂ) (ball 0 (↑(f (↑x : InfinitePlace K)) : ℝ))

Tactic:
exact convex_ball _ _

Premises used: convex_ball
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ convexBodyLT'Factor K ≠ 0

Tactic:
mul_ne_zero (pow_ne_zero _ two_ne_zero) (pow_ne_zero _ pi_ne_zero)

Premises used: NNReal.pi_ne_zero, pow_ne_zero, two_ne_zero, mul_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 1 ≤ convexBodyLT'Factor K

Tactic:
one_le_mul (one_le_pow₀ one_le_two) (one_le_pow₀ (one_le_two.trans Real.two_le_pi))

Premises used: Real.two_le_pi, one_le_pow₀, one_le_two, one_le_mul, LE.le.trans
-- 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
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
rw₁ : NullMeasurableSet (α := ℂ) {x : ℂ | |x.re| < 1 ∧ |x.im| < HPow.hPow (β := ℕ) (↑B : ℝ) 2} volume
⊢ (volume : (a : Set ℂ) → ℝ≥0∞) {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]

Premises used: MeasureTheory.MeasurePreserving.symm, Complex.volume_preserving_equiv_real_prod, MeasureTheory.MeasurePreserving.measure_preimage
-- 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
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))
⊢ {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))

Tactic:
ext
-- 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
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)
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
⊢ 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:
simp_rw [Set.mem_setOf_eq, Set.mem_prod, Set.mem_Ioo, abs_lt]

Premises used: Set.mem_Ioo, Set.mem_setOf_eq, Set.mem_prod, abs_lt
-- 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
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
⊢ (volume : (a : Set (ℝ × ℝ)) → ℝ≥0∞) {a : ℝ × ℝ | |a.1| < 1 ∧ |a.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]]
-- 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
⊢ HMul.hMul (α := ℝ≥0∞) 2 2 = 4

Tactic:
norm_num