-- 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
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) : ℝ)
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
refine_3 :
  (∀ (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) : ℝ)
refine_4 :
  (∀ (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 : ℂ)
⊢ ((∀ (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:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨fun w h_ne ↦ ?_, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩