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
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
h : ¬w₁.IsReal
⊢ Ne (α := ℝ) (↑2 : ℝ) 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
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
let let₁ let₂ :
  ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B
refine_1 :
  let S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult;
  ∀ (w : InfinitePlace K),
    w ≠ w₁ →
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w =
        f w
refine_2 refine_2₁ :
  let 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
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B

Tactic:
classical
  let S := ∏ w ∈ Finset.univ.erase w₁, (f w) ^ mult w
  refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩
  · exact fun w hw => Function.update_of_ne hw _ f
  · 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]
    · rw [Finset.prod_ne_zero_iff]
      exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))
    · rw [mult]; split_ifs <;> norm_num

Premises used: NNReal.rpow_natCast, mul_assoc, NumberField.InfinitePlace.mult, NNReal.rpow_mul, Finset.prod_congr, Finset.prod_ne_zero_iff, Function.update_self, mul_one, NNReal.rpow_one, inv_mul_cancel₀, 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 }
x : K
simp_rw :
  ((∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
          ((a.embedding : (a : K) → ℂ) x : ℂ)) ↔
    (∀ (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
⊢ Membership.mem (α := mixedSpace K) (convexBodyLT' K f w₀)
      ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) ↔
    (∀ (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

Tactic:
simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
    forall_true_left, Pi.ringHom_apply, mem_ball_zero_iff, ← Complex.norm_real,
    embedding_of_isReal_apply, norm_embedding_eq, Subtype.forall]

Premises used: forall_true_left, NumberField.mixedEmbedding, NumberField.InfinitePlace.norm_embedding_eq, Subtype.forall, Set.mem_pi, Complex.norm_real, NumberField.InfinitePlace.embedding_of_isReal_apply, Set.mem_prod, Set.mem_univ, Pi.ringHom_apply, RingHom.prod_apply, 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
⊢ ((∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
          ((a.embedding : (a : K) → ℂ) x : ℂ)) ↔
    (∀ (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

Tactic:
⟨fun ⟨h₁, h₂⟩ ↦ ⟨fun w h_ne ↦ ?_, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩

Premises used: _private.0.NumberField.mixedEmbedding.convexBodyLT'_mem.match_1, abs, Complex.im, NumberField.InfinitePlace.embedding, Complex.re, And, HPow.hPow, And.intro, LT.lt, Iff.intro, _private.0.NumberField.mixedEmbedding.convexBodyLT'_mem.match_2, OfNat.ofNat, Subtype.val, DFunLike.coe, 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 }
x : K
h :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
h₂ :
  ∀ (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) : ℝ))
      ((a.embedding : (a : K) → ℂ) x : ℂ)
w : InfinitePlace K
h_ne : w ≠ (↑w₀ : InfinitePlace K)
pos : ∀ (hw : w.IsReal), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
neg : ∀ (hw : ¬w.IsReal), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
by_cases hw : IsReal w

Premises used: NumberField.InfinitePlace.IsReal
-- 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 :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
h₂ :
  ∀ (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) : ℝ))
      ((a.embedding : (a : K) → ℂ) x : ℂ)
w : InfinitePlace K
h_ne : w ≠ (↑w₀ : InfinitePlace K)
hw : w.IsReal
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
norm_embedding_eq w _ ▸ h₁ w hw

Premises used: NumberField.InfinitePlace.norm_embedding_eq, Eq.rec, Eq.symm
-- 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 :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
h₂ :
  ∀ (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) : ℝ))
      ((a.embedding : (a : K) → ℂ) x : ℂ)
w : InfinitePlace K
h_ne : w ≠ (↑w₀ : InfinitePlace K)
hw : w.IsReal
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

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

Tactic:
specialize h₂ w (not_isReal_iff_isComplex.mp hw)

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

Tactic:
rw [apply_ite (w.embedding x ∈ ·), Set.mem_setOf_eq,
        mem_ball_zero_iff, norm_embedding_eq] at h₂

Premises used: NumberField.InfinitePlace.norm_embedding_eq, Membership.mem, apply_ite, Set.mem_setOf_eq, NumberField.InfinitePlace.embedding, DFunLike.coe, 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 :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
w : InfinitePlace K
h_ne : w ≠ (↑w₀ : InfinitePlace K)
hw : ¬w.IsReal
h₂ :
  if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w ⋯ = w₀ then
    |Complex.re ((w.embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im ((w.embedding : (a : K) → ℂ) x)| < HPow.hPow (β := ℕ) (↑(f w) : ℝ) 2
  else (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ ¬Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w ⋯ = w₀

Tactic:
Subtype.coe_ne_coe.1 h_ne

Premises used: Iff.mp, Subtype.coe_ne_coe
-- 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 :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
w : InfinitePlace K
h_ne : w ≠ (↑w₀ : InfinitePlace K)
hw : ¬w.IsReal
h₂ :
  if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w ⋯ = w₀ then
    |Complex.re ((w.embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im ((w.embedding : (a : K) → ℂ) x)| < HPow.hPow (β := ℕ) (↑(f w) : ℝ) 2
  else (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ ¬Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w ⋯ = w₀

Tactic:
exact Subtype.coe_ne_coe.1 h_ne

Premises used: Iff.mp, Subtype.coe_ne_coe
-- 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 :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
w : InfinitePlace K
h_ne : w ≠ (↑w₀ : InfinitePlace K)
hw : ¬w.IsReal
h₂ :
  if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w ⋯ = w₀ then
    |Complex.re ((w.embedding : (a : K) → ℂ) x)| < 1 ∧
      |Complex.im ((w.embedding : (a : K) → ℂ) x)| < HPow.hPow (β := ℕ) (↑(f w) : ℝ) 2
  else (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
neg neg₁ neg₂ neg₃ : ∀ (h₂ : (w : (a : K) → ℝ) x < (↑(f w) : ℝ)), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
rwa [if_neg (by exact Subtype.coe_ne_coe.1 h_ne)] at h₂

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 :
  (∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(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) : ℝ))
        ((a.embedding : (a : K) → ℂ) x : ℂ)
h₁ : ∀ (a : InfinitePlace K) (b : a.IsReal), (a : (a : K) → ℝ) x < (↑(f a) : ℝ)
h₂ :
  ∀ (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) : ℝ))
      ((a.embedding : (a : K) → ℂ) x : ℂ)
⊢ |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

Tactic:
simpa [if_true] using h₂ w₀.val w₀.prop

Premises used: if_true, Subtype.prop, 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 }
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.IsReal
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
h₁ w (ne_of_isReal_isComplex hw w₀.prop)

Premises used: NumberField.InfinitePlace.ne_of_isReal_isComplex, Subtype.prop
-- 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.IsReal
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)

Tactic:
exact h₁ w (ne_of_isReal_isComplex hw w₀.prop)

Premises used: NumberField.InfinitePlace.ne_of_isReal_isComplex, Subtype.prop
-- 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
pos :
  ∀ (h_ne : w = (↑w₀ : InfinitePlace K)),
    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 : ℂ)
neg :
  ∀ (h_ne : ¬w = (↑w₀ : InfinitePlace K)),
    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 : ℂ)
⊢ 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:
by_cases h_ne : w = w₀
-- 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)
⊢ 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:
simpa [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)
⊢ ¬Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w hw = w₀

Tactic:
Subtype.coe_ne_coe.1 h_ne

Premises used: Iff.mp, Subtype.coe_ne_coe
-- 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)
⊢ ¬Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w hw = w₀

Tactic:
exact Subtype.coe_ne_coe.1 h_ne

Premises used: Iff.mp, Subtype.coe_ne_coe