awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
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
⊢ ∃ (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:
obtain ⟨y, hy, rfl⟩ := hx₁

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
rw 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)
⊢ 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

Tactic:
rw [expMapBasis_apply'' y]

Premises used: NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply''
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
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)
⊢ ∃ (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:
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]⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
⊢ y w₀ ≤ 0

Tactic:
simpa using hy w₀ (Set.mem_univ _)

Premises used: NumberField.Units.dirichletUnitTheorem.w₀, Set.mem_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
⊢ Real.exp (y w₀) ≤ 1

Tactic:
exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))

Premises used: Iff.mpr, Real.exp_le_one_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
neg : ∀ (h : ¬w = w₀), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (y w)
⊢ Membership.mem (γ := Set ℝ) (if w = w₀ then {0} else Set.Icc 0 1) (if w = w₀ then 0 else y w)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
h : w = w₀
⊢ Membership.mem (γ := Set ℝ) {0} 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
h : ¬w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (y w)

Tactic:
simpa [h] using hy w (Set.mem_univ _)

Premises used: Set.mem_univ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
refine_2 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)
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) 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 _)

Premises used: Iff.mpr, Set.mem_smul, Set.mem_image, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, exists_exists_and_eq_and, Real.exp_le_one_iff, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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})

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
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
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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

Tactic:
simpa [hx₀] using zero_mem_compactSet K

Premises used: NumberField.mixedEmbedding.fundamentalCone.zero_mem_compactSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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

Tactic:
⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩

Premises used: NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₁, Iff.intro, Set.mem_union_left, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx₀ : ¬x = 0
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
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x ↔
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0}) x

Tactic:
refine ⟨fun hx ↦ Set.mem_union_left _ (compactSet_eq_union_aux₁ hx₀ hx), fun hx ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x

Tactic:
simp only [Set.union_singleton, Set.mem_insert_iff, hx₀, false_or] at hx

Premises used: false_or, Set.mem_insert_iff, Set.union_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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

Tactic:
compactSet_eq_union_aux₂ hx₀ hx

Premises used: NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₂
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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

Tactic:
exact compactSet_eq_union_aux₂ hx₀ hx

Premises used: NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₂
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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
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
neg neg₁ :
  ∀ (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
⊢ Eq (α := Set (realSpace K)) (compactSet K) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})

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

Premises used: false_or, Set.mem_insert_iff, NumberField.mixedEmbedding.fundamentalCone.zero_mem_compactSet, Set.union_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
    ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) (compactSet K)

Tactic:
rw [compactSet_eq_union]

Premises used: NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
    ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})

Tactic:
Set.subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K))
    ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0})

Tactic:
exact Set.subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Subset (α := Set (mixedSpace K))
    (closure (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
    (normAtAllPlaces ⁻¹' compactSet K)
⊢ Subset (α := Set (mixedSpace K)) (closure (normLeOne K)) (normAtAllPlaces ⁻¹' compactSet K)

Tactic:
rw [normLeOne_eq_preimage]

Premises used: NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (mixedSpace K))
    (closure (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
    (normAtAllPlaces ⁻¹' compactSet K)

Tactic:
((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)

Premises used: HasSubset.Subset.trans, Set.preimage_mono, NumberField.mixedEmbedding.continuous_normAtAllPlaces, Continuous.closure_preimage_subset
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  Subset (α := Set (realSpace K)) (closure ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)) (compactSet K)
⊢ Subset (α := Set (mixedSpace K))
    (closure (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K))
    (normAtAllPlaces ⁻¹' compactSet K)

Tactic:
refine ((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)

Premises used: HasSubset.Subset.trans, Set.preimage_mono, NumberField.mixedEmbedding.continuous_normAtAllPlaces, Continuous.closure_preimage_subset
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) (closure ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)) (compactSet K)

Tactic:
(isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_

Premises used: Iff.mpr, NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet, IsClosed.closure_subset_iff, IsCompact.isClosed
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) (compactSet K)
⊢ Subset (α := Set (realSpace K)) (closure ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)) (compactSet K)

Tactic:
refine (isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_

Premises used: Iff.mpr, NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet, IsClosed.closure_subset_iff, IsCompact.isClosed
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) (compactSet K)

Tactic:
(Set.image_mono subset_closure).trans (expMapBasis_closure_subset_compactSet _)

Premises used: subset_closure, Set.image_mono, HasSubset.Subset.trans, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Subset (α := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) (compactSet K)

Tactic:
exact (Set.image_mono subset_closure).trans (expMapBasis_closure_subset_compactSet _)

Premises used: subset_closure, Set.image_mono, HasSubset.Subset.trans, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0} =ᶠ[ae (F := Measure (realSpace K)) volume]
    (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)
⊢ compactSet K =ᶠ[ae (F := Measure (realSpace K)) volume]
    (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)

Tactic:
rw [compactSet_eq_union]

Premises used: NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (ae (F := Measure (realSpace K)) volume).EventuallyEq (β := Prop) {0} ∅

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K) ∪ {0} =ᶠ[ae (F := Measure (realSpace K)) volume]
    (↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)

Tactic:
exact union_ae_eq_left_of_ae_eq_empty (by simp)

Premises used: MeasureTheory.union_ae_eq_left_of_ae_eq_empty
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ IsBounded (α := mixedSpace K) (normLeOne K)

Tactic:
rw [normLeOne_eq_preimage]

Premises used: NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
obtain :
  ∀ (C : ℝ)
    (hC :
      ∀ (x : realSpace K),
        Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C),
    IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this

Premises used: isBounded_iff_forall_norm_le, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, isBounded_iff_forall_norm_le, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this : IsBounded (α := realSpace K) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K)
C : ℝ
hC :
  ∀ (x : realSpace K),
    Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x → ‖x‖ ≤ C
refine :
  ∀ (x : mixedSpace K)
    (hx :
      Membership.mem (γ := Set (mixedSpace K))
        (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K) x),
    ‖x‖ ≤ C
⊢ IsBounded (α := mixedSpace K) (normAtAllPlaces ⁻¹' (↑expMapBasis : realSpace K → realSpace K) '' paramSet K)

Tactic:
refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, isBounded_iff_forall_norm_le, Exists.intro