awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : Membership.mem (γ := Set (realSpace K)) (compactSet K) x
obtain :
  ∀ (c : ℝ) (hc : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) c) (y : realSpace K)
    (hy :
      Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w = w₀ then {0} else Set.Icc 0 1)
        y)
    (hx₀ :
      Ne.{u_1 + 1} (α := realSpace K)
        ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y)) 0),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
      ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y))
refine_1 :
  ∀ (c : ℝ) (hc : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) c) (y : realSpace K)
    (hy :
      Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w = w₀ then {0} else Set.Icc 0 1)
        y)
    (hx₀ :
      Ne.{u_1 + 1} (α := realSpace K)
        ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y)) 0),
    Membership.mem (γ := Set (realSpace K)) (closure (paramSet K)) fun (w : InfinitePlace K) ↦
      if w = w₀ then Real.log c else y w
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
have refine_2 : ∀ (c : ℝ) (hc : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) c) (y : realSpace K)
  (hy :
    Membership.mem (γ := Set (realSpace K))
      (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then {0} else Set.Icc 0 1)
      y)
  (hx₀ :
    Ne.{u_1 + 1} (α := realSpace K)
      ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y)) 0),
  Eq.{u_1 + 1} (α := realSpace K)
    ((↑expMapBasis : realSpace K → realSpace K) fun (w : InfinitePlace K) ↦ if w = w₀ then Real.log c else y w)
    ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y))
Tactic: classical
  obtain ⟨c, hc, ⟨_, ⟨y, hy, rfl⟩, rfl⟩⟩ := hx₁
  refine ⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩
  · rw [closure_paramSet, Set.mem_univ_pi]
    intro w
    split_ifs with h
    · refine Real.log_nonpos hc.1 hc.2
    · simpa [h] using hy w (Set.mem_univ _)
  · have hc' : 0 < c := by
      contrapose! hx₀
      rw [le_antisymm hx₀ hc.1, zero_smul]
    rw [expMapBasis_apply'', if_pos rfl, Real.exp_log hc']
    congr with w
    split_ifs with h
    · simpa [h, eq_comm] using hy w₀
    · rfl
Cleared hypotheses: x, hx₀, hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x
have simp : ∀
  (hx₁ :
    ∃ (x_1 : realSpace K),
      Membership.mem (γ := Set (realSpace K))
          (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
          x_1 ∧
        (↑expMapBasis : realSpace K → realSpace K) x_1 = x),
  ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x_1 ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x_1 • (↑expMapBasis : realSpace K → realSpace K) a = x
Tactic: simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ :
  ∃ (x_1 : realSpace K),
    Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
        x_1 ∧
      (↑expMapBasis : realSpace K → realSpace K) x_1 = x
⊢ ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x_1 ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x_1 • (↑expMapBasis : realSpace K → realSpace K) a = x
have obtain : ∀ (y : realSpace K)
  (hy :
    Membership.mem (γ := Set (realSpace K))
      (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
      y)
  (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0),
  ∃ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x • (↑expMapBasis : realSpace K → realSpace K) a = (↑expMapBasis : realSpace K → realSpace K) y
Tactic: obtain ⟨y, hy, rfl⟩ := hx₁
Cleared hypotheses: x, hx₀, hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : realSpace K
hy :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
    y
hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0
⊢ HSMul.hSMul (β := realSpace K) (Real.exp (y w₀))
      ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else y i) =
    (↑expMapBasis : realSpace K → realSpace K) y
have rw : HSMul.hSMul (β := realSpace K) (Real.exp (y w₀))
    ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else y i) =
  HSMul.hSMul (β := realSpace K) (Real.exp (y w₀))
    ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦ if i = w₀ then 0 else y i)
Tactic: rw [expMapBasis_apply'' y]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : realSpace K
hy :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
    y
hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0
⊢ ∃ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x • (↑expMapBasis : realSpace K → realSpace K) a = (↑expMapBasis : realSpace K → realSpace K) y
have refine_1 : Real.exp (y w₀) ≤ 1
Tactic: refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : realSpace K
hy :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
    y
hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0
refine_1 : Real.exp (y w₀) ≤ 1
⊢ ∃ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x • (↑expMapBasis : realSpace K → realSpace K) a = (↑expMapBasis : realSpace K → realSpace K) y
have refine_2 : ∀ (w : InfinitePlace K), Membership.mem (γ := Set ℝ) (if w = w₀ then {0} else Set.Icc 0 1) (if w = w₀ then 0 else y w)
Tactic: refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : realSpace K
hy :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
    y
hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0
w : InfinitePlace K
⊢ Membership.mem (γ := Set ℝ) (if w = w₀ then {0} else Set.Icc 0 1) (if w = w₀ then 0 else y w)
have pos : ∀ (h : w = w₀), Membership.mem (γ := Set ℝ) {0} 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
y : realSpace K
hy :
  Membership.mem (γ := Set (realSpace K))
    (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
      if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
    y
hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0
w : InfinitePlace K
pos : ∀ (h : w = w₀), Membership.mem (γ := Set ℝ) {0} 0
⊢ Membership.mem (γ := Set ℝ) (if w = w₀ then {0} else Set.Icc 0 1) (if w = w₀ then 0 else y w)
have neg : ∀ (h : ¬w = w₀), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (y w)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x
have simp : ∀
  (hx₁ :
    ∃ (x_1 : realSpace K),
      Membership.mem (γ := Set (realSpace K))
          (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
            if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
          x_1 ∧
        (↑expMapBasis : realSpace K → realSpace K) x_1 = x),
  ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x_1 ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x_1 • (↑expMapBasis : realSpace K → realSpace K) a = x
Tactic: classical
  simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
simp :
  ∀
    (hx₁ :
      ∃ (x_1 : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
            x_1 ∧
          (↑expMapBasis : realSpace K → realSpace K) x_1 = x),
    ∃ (x_1 : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x_1 ∧
        ∃ (a : realSpace K),
          Membership.mem (γ := Set (realSpace K))
              (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
                if w = w₀ then {0} else Set.Icc 0 1)
              a ∧
            x_1 • (↑expMapBasis : realSpace K → realSpace K) a = x
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x
have simp₁ : ∀ (y : realSpace K)
  (hy :
    Membership.mem (γ := Set (realSpace K))
      (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
      y)
  (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0),
  ∃ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x ∧
      ∃ (a : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then {0} else Set.Icc 0 1)
            a ∧
          x • (↑expMapBasis : realSpace K → realSpace K) a = (↑expMapBasis : realSpace K → realSpace K) y
Tactic: classical
  simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)
Cleared hypotheses: x, hx₀, hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
simp :
  ∀
    (hx₁ :
      ∃ (x_1 : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
            x_1 ∧
          (↑expMapBasis : realSpace K → realSpace K) x_1 = x),
    ∃ (x_1 : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x_1 ∧
        ∃ (a : realSpace K),
          Membership.mem (γ := Set (realSpace K))
              (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
                if w = w₀ then {0} else Set.Icc 0 1)
              a ∧
            x_1 • (↑expMapBasis : realSpace K → realSpace K) a = x
simp₁ :
  ∀ (y : realSpace K)
    (hy :
      Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
        y)
    (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0),
    ∃ (x : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x ∧
        ∃ (a : realSpace K),
          Membership.mem (γ := Set (realSpace K))
              (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
                if w = w₀ then {0} else Set.Icc 0 1)
              a ∧
            x • (↑expMapBasis : realSpace K → realSpace K) a = (↑expMapBasis : realSpace K → realSpace K) y
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x
have refine_1 : ∀ (y : realSpace K)
  (hy :
    Membership.mem (γ := Set (realSpace K))
      (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
      y)
  (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0), Real.exp (y w₀) ≤ 1
Tactic: classical
  simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)
Cleared hypotheses: x, hx₀, hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : x ≠ 0
hx₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
simp :
  ∀
    (hx₁ :
      ∃ (x_1 : realSpace K),
        Membership.mem (γ := Set (realSpace K))
            (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
              if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
            x_1 ∧
          (↑expMapBasis : realSpace K → realSpace K) x_1 = x),
    ∃ (x_1 : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x_1 ∧
        ∃ (a : realSpace K),
          Membership.mem (γ := Set (realSpace K))
              (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
                if w = w₀ then {0} else Set.Icc 0 1)
              a ∧
            x_1 • (↑expMapBasis : realSpace K → realSpace K) a = x
simp₁ :
  ∀ (y : realSpace K)
    (hy :
      Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
        y)
    (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0),
    ∃ (x : ℝ),
      Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x ∧
        ∃ (a : realSpace K),
          Membership.mem (γ := Set (realSpace K))
              (Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
                if w = w₀ then {0} else Set.Icc 0 1)
              a ∧
            x • (↑expMapBasis : realSpace K → realSpace K) a = (↑expMapBasis : realSpace K → realSpace K) y
refine_1 :
  ∀ (y : realSpace K)
    (hy :
      Membership.mem (γ := Set (realSpace K))
        (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
          if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
        y)
    (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0), Real.exp (y w₀) ≤ 1
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x
have refine_2 : ∀ (y : realSpace K)
  (hy :
    Membership.mem (γ := Set (realSpace K))
      (Set.pi (α := fun (i : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then Set.Iic 0 else Set.Icc 0 1)
      y)
  (hx₀ : (↑expMapBasis : realSpace K → realSpace K) y ≠ 0) (w : InfinitePlace K),
  Membership.mem (γ := Set ℝ) (if w = w₀ then {0} else Set.Icc 0 1) (if w = w₀ then 0 else y w)
Tactic: classical
  simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢
  obtain ⟨y, hy, rfl⟩ := hx₁
  refine ⟨Real.exp (y w₀), ⟨Real.exp_nonneg _, ?_⟩,
        fun i ↦ if i = w₀ then 0 else y i, Set.mem_univ_pi.mpr fun w ↦ ?_,
        by rw [expMapBasis_apply'' y]⟩
  · exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))
  · split_ifs with h
    · rfl
    · simpa [h] using hy w (Set.mem_univ _)
Cleared hypotheses: x, hx₀, hx₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realSpace K)) (compactSet K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
have h : ∀ (x : realSpace K),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
have pos : ∀ (hx₀ : x = 0),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
Tactic: by_cases hx₀ : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
pos :
  ∀ (hx₀ : x = 0),
    Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
      Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
        x
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
have neg : ∀ (hx₀ : ¬x = 0),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
Tactic: by_cases hx₀ : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : ¬x = 0
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
have neg : ∀
  (hx :
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
      x),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x
Tactic: refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : ¬x = 0
hx :
  Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x
have hx₁ : Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
Tactic: simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Set (realSpace K)) (compactSet K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
have h : ∀ (x : realSpace K),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
Tactic: classical
  ext x
  by_cases hx₀ : x = 0
  · simpa [hx₀] using zero_mem_compactSet K
  · refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
    simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx
    exact compactSet_eq_union_aux₂ hx₀ hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
      Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
        x
⊢ Eq (α := Set (realSpace K)) (compactSet K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
have pos : ∀ (x : realSpace K) (hx₀ : x = 0),
  Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x
Tactic: classical
  ext x
  by_cases hx₀ : x = 0
  · simpa [hx₀] using zero_mem_compactSet K
  · refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
    simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx
    exact compactSet_eq_union_aux₂ hx₀ hx