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
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
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B
have 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
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
-- 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
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
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B
have 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
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
-- 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 : K
⊢ 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
have 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
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]
-- 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 : 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
have refine_1 : ((∀ (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)), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨fun w h_ne ↦ ?_, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
-- 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 : K
refine_1 :
  ((∀ (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)), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
⊢ ((∀ (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
have refine_2 : ((∀ (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: refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨fun w h_ne ↦ ?_, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
-- 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 : 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)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have pos : ∀ (hw : w.IsReal), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: by_cases hw : IsReal w
-- 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 : 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) : ℝ)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have neg : ∀ (hw : ¬w.IsReal), (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: by_cases hw : IsReal w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
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) : ℝ)
have h₃ : Membership.mem (α := ℂ) (γ := Set ℂ)
  (if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w sorry = 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)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody (hypothesis)
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 : ℂ)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have h₃ : if Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) w sorry = 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₂
Cleared hypotheses: h₂
-- 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 : 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) : ℝ)
⊢ (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
have neg : ∀ (h₂ : (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₂
Cleared hypotheses: h₂
-- 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 : 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
⊢ 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 : ℂ)
have 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 : ℂ)
Tactic: by_cases h_ne : w = w₀
-- 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 : 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 : ℂ)
⊢ 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 : ℂ)
have 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 : ℂ)
Tactic: by_cases h_ne : w = w₀
-- 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 : 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 : ℂ)
have neg : Membership.mem (α := ℂ) (γ := Set ℂ) (ball 0 (↑(f w) : ℝ)) ((w.embedding : (a : K) → ℂ) x : ℂ)
Tactic: rw [if_neg (by exact Subtype.coe_ne_coe.1 h_ne)]
-- 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 : 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 ℂ) (ball 0 (↑(f w) : ℝ)) ((w.embedding : (a : K) → ℂ) x : ℂ)
have neg : (w : (a : K) → ℝ) x < (↑(f w) : ℝ)
Tactic: rw [mem_ball_zero_iff, norm_embedding_eq]
-- 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 : x ∈ convexBodyLT' K f w₀
⊢ -x ∈ convexBodyLT' K f w₀
have 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))
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 ⊢
Cleared hypotheses: hx