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
refine : ∀ (w : InfinitePlace K), IsCompact (X := ℝ) (if w = w₀ then {0} else Set.Icc 0 1)
⊢ IsCompact (X := realSpace K) (compactSet K)

Tactic:
refine isCompact_Icc.smul_set <| (isCompact_univ_pi fun w ↦ ?_).image_of_continuousOn
    (continuous_expMapBasis K).continuousOn

Premises used: Continuous.continuousOn, isCompact_univ_pi, CompactIccSpace.isCompact_Icc, NumberField.mixedEmbedding.fundamentalCone.continuous_expMapBasis, IsCompact.image_of_continuousOn, IsCompact.smul_set
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
pos : w = w₀ → IsCompact (X := ℝ) {0}
neg : ¬w = w₀ → IsCompact (X := ℝ) (Set.Icc 0 1)
⊢ IsCompact (X := ℝ) (if w = w₀ then {0} else Set.Icc 0 1)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : w = w₀
⊢ IsCompact (X := ℝ) {0}

Tactic:
isCompact_singleton

Premises used: isCompact_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : w = w₀
⊢ IsCompact (X := ℝ) {0}

Tactic:
exact isCompact_singleton

Premises used: isCompact_singleton
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : ¬w = w₀
⊢ IsCompact (X := ℝ) (Set.Icc 0 1)

Tactic:
isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
h : ¬w = w₀
⊢ IsCompact (X := ℝ) (Set.Icc 0 1)

Tactic:
exact isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) 0

Tactic:
Set.zero_mem_smul_iff.mpr (Or.inl ⟨Set.left_mem_Icc.mpr zero_le_one, ?_⟩)

Premises used: Iff.mpr, Set.Mem, Set.zero_mem_smul_iff, zero_le_one, Set.left_mem_Icc, And.intro, Or.inl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  Set.Nonempty.{u_1} (α := realSpace K)
    ((↑expMapBasis : realSpace K → realSpace K) ''
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then {0} else Set.Icc 0 1)
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) 0

Tactic:
refine Set.zero_mem_smul_iff.mpr (Or.inl ⟨Set.left_mem_Icc.mpr zero_le_one, ?_⟩)

Premises used: Iff.mpr, Set.zero_mem_smul_iff, zero_le_one, Set.left_mem_Icc, And.intro, Or.inl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ∀ (i : InfinitePlace K), Set.Nonempty (α := ℝ) (if i = w₀ then {0} else Set.Icc 0 1)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Set.Nonempty.{u_1} (α := realSpace K)
    ((↑expMapBasis : realSpace K → realSpace K) ''
      Set.pi (α := fun (a : InfinitePlace K) ↦ ℝ) Set.univ fun (w : InfinitePlace K) ↦
        if w = w₀ then {0} else Set.Icc 0 1)

Tactic:
exact Set.image_nonempty.mpr (Set.univ_pi_nonempty_iff.mpr (by aesop))

Premises used: Iff.mpr, Set.image_nonempty, Set.univ_pi_nonempty_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
hx : Membership.mem (γ := Set (realSpace K)) (compactSet K) x
w : InfinitePlace K
obtain :
  ∀ (c : ℝ) (hc : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) c) (a : realSpace K)
    (ha :
      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),
    LE.le (α := ℝ) 0 ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) a) w)
⊢ 0 ≤ x w

Tactic:
obtain ⟨c, hc, ⟨_, ⟨⟨a, ha, rfl⟩, _, rfl⟩⟩⟩ := hx

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
c : ℝ
hc : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) c
a : realSpace K
ha :
  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
⊢ LE.le (α := ℝ) 0 ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) a) w)

Tactic:
mul_nonneg hc.1 (expMapBasis_pos _ _).le

Premises used: mul_nonneg, LT.lt.le, And.left, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
c : ℝ
hc : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) c
a : realSpace K
ha :
  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
⊢ LE.le (α := ℝ) 0 ((fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) a) w)

Tactic:
exact mul_nonneg hc.1 (expMapBasis_pos _ _).le

Premises used: mul_nonneg, LT.lt.le, And.left, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_pos
-- 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)) (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))
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x

Tactic:
obtain ⟨c, hc, ⟨_, ⟨y, hy, rfl⟩, rfl⟩⟩ := hx₁

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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))

Tactic:
⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩

Premises used: Set.Mem, setOf, Real.log, NumberField.Units.dirichletUnitTheorem.w₀, And.intro, Exists.intro, Set.image, Eq, ite
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
refine_1 :
  Membership.mem (γ := Set (realSpace K)) (closure (paramSet K)) fun (w : InfinitePlace K) ↦
    if w = w₀ then Real.log c else y w
refine_2 :
  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))
⊢ 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))

Tactic:
refine ⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
refine_1 :
  ∀ (i : InfinitePlace K),
    Membership.mem (γ := Set ℝ) (if i = w₀ then Set.Iic 0 else Set.Icc 0 1) (if i = w₀ then Real.log c else y i)
⊢ Membership.mem (γ := Set (realSpace K)) (closure (paramSet K)) fun (w : InfinitePlace K) ↦
    if w = w₀ then Real.log c else y w

Tactic:
rw [closure_paramSet, Set.mem_univ_pi]

Premises used: NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, Set.mem_univ_pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
w : InfinitePlace K
pos : ∀ (h : w = w₀), Membership.mem (γ := Set ℝ) (Set.Iic 0) (Real.log c)
neg : ∀ (h : ¬w = w₀), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) (y w)
⊢ Membership.mem (γ := Set ℝ) (if w = w₀ then Set.Iic 0 else Set.Icc 0 1) (if w = w₀ then Real.log c 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
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
w : InfinitePlace K
h : w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Iic 0) (Real.log c)

Tactic:
Real.log_nonpos hc.1 hc.2

Premises used: Set.Mem, setOf, Real.log_nonpos, And.right, And.left, Set.Iic
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
w : InfinitePlace K
h : w = w₀
⊢ Membership.mem (γ := Set ℝ) (Set.Iic 0) (Real.log c)

Tactic:
refine Real.log_nonpos hc.1 hc.2

Premises used: Real.log_nonpos, And.right, And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
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
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
contrapose! : ∀ (hx₀ : c ≤ 0), c • (↑expMapBasis : realSpace K → realSpace K) y = 0
⊢ 0 < c

Tactic:
contrapose! hx₀
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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₀ : c ≤ 0
rw : HSMul.hSMul (α := ℝ) 0 ((↑expMapBasis : realSpace K → realSpace K) y) = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := realSpace K) 0 0
⊢ c • (↑expMapBasis : realSpace K → realSpace K) y = 0

Tactic:
rw [le_antisymm hx₀ hc.1, zero_smul]

Premises used: le_antisymm, zero_smul, And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ 0 < c

Tactic:
have hc' : 0 < c := by
      contrapose! hx₀
      rw [le_antisymm hx₀ hc.1, zero_smul]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
hc' : 0 < c
refine_2 :
  HSMul.hSMul (β := realSpace K) c
      ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦
        if i = w₀ then 0 else if i = w₀ then Real.log c else y i) =
    (fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y)
⊢ 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:
rw [expMapBasis_apply'', if_pos rfl, Real.exp_log hc']

Premises used: if_pos, Real.exp_log, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'', rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
hc' : 0 < c
refine_2 : ∀ (w : InfinitePlace K), (if w = w₀ then 0 else if w = w₀ then Real.log c else y w) = y w
⊢ HSMul.hSMul (β := realSpace K) c
      ((↑expMapBasis : realSpace K → realSpace K) fun (i : InfinitePlace K) ↦
        if i = w₀ then 0 else if i = w₀ then Real.log c else y i) =
    (fun (x1 : ℝ) (x2 : realSpace K) ↦ x1 • x2) c ((↑expMapBasis : realSpace K → realSpace K) y)

Tactic:
congr with w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
hc' : 0 < c
w : InfinitePlace K
pos : ∀ (h : w = w₀), 0 = y w
neg : ∀ (h : ¬w = w₀), y w = y w
⊢ (if w = w₀ then 0 else if w = w₀ then Real.log c else y w) = 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
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
hc' : 0 < c
w : InfinitePlace K
h : w = w₀
⊢ 0 = y w

Tactic:
simpa [h, eq_comm] using hy w₀

Premises used: eq_comm, NumberField.Units.dirichletUnitTheorem.w₀
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
hc' : 0 < c
w : InfinitePlace K
h : ¬w = w₀
⊢ y w = y w

Tactic:
rfl
-- 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)) (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
refine_2 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))
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x

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

Premises used: if_pos, eq_comm, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply'', Set.mem_univ_pi, rfl
-- 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
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) x

Tactic:
simp only [closure_paramSet, Set.mem_image, Set.mem_smul, exists_exists_and_eq_and] at hx₁ ⊢

Premises used: Set.mem_smul, Set.mem_image, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, exists_exists_and_eq_and