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
n : ℕ
hn : 0 < n
have have₁ have₂ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have have₃ : ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
  lmarginal (X := fun (a : InfinitePlace K) ↦ ℝ)
      (fun (i : InfinitePlace K) ↦ Measure.restrict volume (if i = w₀ then Set.Iic 0 else Set.Ico 0 1)) (erase univ w₀)
      (fun (x : (i : InfinitePlace K) → ℝ) ↦
        ∫⁻ (xᵢ : ℝ) in Set.Iic 0,
          ENNReal.ofReal (Real.exp (Function.update (β := fun (a : InfinitePlace K) ↦ ℝ) x w₀ xᵢ w₀ * (↑n : ℝ))))
      0 =
    (↑n : ℝ≥0∞)⁻¹
Tactic: classical
  have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
  rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]
  simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ, if_neg
    (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico,
    sub_zero, ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]
  rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic
    hn, mul_zero, Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]
  filter_upwards with _ using Real.exp_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn : 0 < n
have have₁ have₂ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have₃ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    lmarginal (X := fun (a : InfinitePlace K) ↦ ℝ)
        (fun (i : InfinitePlace K) ↦ Measure.restrict volume (if i = w₀ then Set.Iic 0 else Set.Ico 0 1))
        (erase univ w₀)
        (fun (x : (i : InfinitePlace K) → ℝ) ↦
          ∫⁻ (xᵢ : ℝ) in Set.Iic 0,
            ENNReal.ofReal (Real.exp (Function.update (β := fun (a : InfinitePlace K) ↦ ℝ) x w₀ xᵢ w₀ * (↑n : ℝ))))
        0 =
      (↑n : ℝ≥0∞)⁻¹
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have have₄ : ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)), ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑n : ℝ≥0∞)⁻¹
Tactic: classical
  have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
  rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]
  simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ, if_neg
    (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico,
    sub_zero, ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]
  rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic
    hn, mul_zero, Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]
  filter_upwards with _ using Real.exp_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
n : ℕ
hn : 0 < n
have have₁ have₂ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have₃ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    lmarginal (X := fun (a : InfinitePlace K) ↦ ℝ)
        (fun (i : InfinitePlace K) ↦ Measure.restrict volume (if i = w₀ then Set.Iic 0 else Set.Ico 0 1))
        (erase univ w₀)
        (fun (x : (i : InfinitePlace K) → ℝ) ↦
          ∫⁻ (xᵢ : ℝ) in Set.Iic 0,
            ENNReal.ofReal (Real.exp (Function.update (β := fun (a : InfinitePlace K) ↦ ℝ) x w₀ xᵢ w₀ * (↑n : ℝ))))
        0 =
      (↑n : ℝ≥0∞)⁻¹
have₄ :
  ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
    ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp ((↑n : ℝ) * xᵢ)) = (↑n : ℝ≥0∞)⁻¹
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * (↑n : ℝ))) = (↑n : ℝ≥0∞)⁻¹
have have₅ : ∀ (hn : LT.lt (α := ℝ) 0 (↑n : ℝ)),
  (ae (F := Measure ℝ) (Measure.restrict volume (Set.Iic 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    Real.exp ((↑n : ℝ) * x)
Tactic: classical
  have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
  rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]
  simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ, if_neg
    (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico,
    sub_zero, ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]
  rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic
    hn, mul_zero, Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]
  filter_upwards with _ using Real.exp_nonneg _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsCompact (X := realSpace K) (compactSet K)
have refine : ∀ (w : InfinitePlace K), IsCompact (X := ℝ) (if w = w₀ then {0} else Set.Icc 0 1)
Tactic: refine isCompact_Icc.smul_set <| (isCompact_univ_pi fun w ↦ ?_).image_of_continuousOn
    (continuous_expMapBasis K).continuousOn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ IsCompact (X := ℝ) (if w = w₀ then {0} else Set.Icc 0 1)
have pos : w = w₀ → IsCompact (X := ℝ) {0}
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
pos : w = w₀ → IsCompact (X := ℝ) {0}
⊢ IsCompact (X := ℝ) (if w = w₀ then {0} else Set.Icc 0 1)
have neg : ¬w = w₀ → IsCompact (X := ℝ) (Set.Icc 0 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Membership.mem (γ := Set (realSpace K)) (compactSet K) 0
have 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)
Tactic: refine Set.zero_mem_smul_iff.mpr (Or.inl ⟨Set.left_mem_Icc.mpr zero_le_one, ?_⟩)
-- 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 : Membership.mem (γ := Set (realSpace K)) (compactSet K) x
w : InfinitePlace K
⊢ 0 ≤ x w
have 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)
Tactic: obtain ⟨c, hc, ⟨_, ⟨⟨a, ha, rfl⟩, _, rfl⟩⟩⟩ := hx
Cleared hypotheses: x, 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)) (compactSet K) x
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
have 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))
Tactic: obtain ⟨c, hc, ⟨_, ⟨y, hy, rfl⟩, 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
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))
have refine_1 : Membership.mem (γ := Set (realSpace K)) (closure (paramSet K)) fun (w : InfinitePlace K) ↦
  if w = w₀ then Real.log c else y w
Tactic: refine ⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ 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))
have 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))
Tactic: refine ⟨fun w ↦ if w = w₀ then Real.log c else y w, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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)) (closure (paramSet K)) fun (w : InfinitePlace K) ↦
    if w = w₀ then Real.log c else y w
have 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)
Tactic: rw [closure_paramSet, Set.mem_univ_pi]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ 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)
have pos : ∀ (h : w = w₀), Membership.mem (γ := Set ℝ) (Set.Iic 0) (Real.log c)
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
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)
⊢ 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)
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
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
have contrapose! : ∀ (hx₀ : c ≤ 0), c • (↑expMapBasis : realSpace K → realSpace K) y = 0
Tactic: contrapose! 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
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
⊢ c • (↑expMapBasis : realSpace K → realSpace K) y = 0
have rw : HSMul.hSMul (α := ℝ) 0 ((↑expMapBasis : realSpace K → realSpace K) y) = 0
Tactic: rw [le_antisymm hx₀ hc.1, zero_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ c • (↑expMapBasis : realSpace K → realSpace K) y = 0
have rw₁ : Eq.{u_1 + 1} (α := realSpace K) 0 0
Tactic: rw [le_antisymm hx₀ hc.1, zero_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (hypothesis)
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
⊢ 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))
have hc' : 0 < c
Tactic: have hc' : 0 < c := by
      contrapose! hx₀
      rw [le_antisymm hx₀ hc.1, zero_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ 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))
have 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)
Tactic: rw [expMapBasis_apply'', if_pos rfl, Real.exp_log hc']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ 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)
have refine_2 : ∀ (w : InfinitePlace K), (if w = w₀ then 0 else if w = w₀ then Real.log c else y w) = y w
Tactic: congr with w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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
⊢ (if w = w₀ then 0 else if w = w₀ then Real.log c else y w) = y w
have pos : ∀ (h : w = w₀), 0 = 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
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
⊢ (if w = w₀ then 0 else if w = w₀ then Real.log c else y w) = y w
have neg : ∀ (h : ¬w = w₀), y w = 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)) (compactSet K) x
⊢ Membership.mem (γ := Set (realSpace K)) ((↑expMapBasis : realSpace K → realSpace K) '' closure (paramSet K)) x
have 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))
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)) (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
have 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
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₁