awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) w.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
simp_rw₁ :
  ∏ x_1 : InfinitePlace K, HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) ^ x_1.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (c • x) =
    HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have simp_rw₂ : ∏ x_1 : InfinitePlace K,
    |c| ^ x_1.mult * HPow.hPow (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) x_1.mult =
  |c| ^ finrank ℚ K * ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) w.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
simp_rw₁ :
  ∏ x_1 : InfinitePlace K, HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) ^ x_1.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
simp_rw₂ :
  ∏ x_1 : InfinitePlace K,
      |c| ^ x_1.mult * HPow.hPow (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) x_1.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (c • x) =
    HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have simp_rw₃ : HMul.hMul (α := ℝ) (∏ x : InfinitePlace K, |c| ^ x.mult)
    (∏ x_1 : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) x_1.mult) =
  |c| ^ finrank ℚ K * ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) w.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
simp_rw₁ :
  ∏ x_1 : InfinitePlace K, HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) ^ x_1.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
simp_rw₂ :
  ∏ x_1 : InfinitePlace K,
      |c| ^ x_1.mult * HPow.hPow (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) x_1.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
simp_rw₃ :
  HMul.hMul (α := ℝ) (∏ x : InfinitePlace K, |c| ^ x.mult)
      (∏ x_1 : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) x_1.mult) =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (c • x) =
    HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have simp_rw₄ : HPow.hPow (β := ℕ) |c| (∑ i : InfinitePlace K, i.mult) *
    ∏ x_1 : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) x_1.mult =
  |c| ^ finrank ℚ K * ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
⊢ (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1
have fst : ∀ (x : { w : InfinitePlace K // w.IsReal }),
  (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)).1 x =
    (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1).1
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
fst :
  ∀ (x : { w : InfinitePlace K // w.IsReal }),
    (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)).1
        x =
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
            1).1
        x
⊢ (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1
have snd : ∀ (x : { w : InfinitePlace K // w.IsComplex }),
  (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)).2 x =
    (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1).2
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c| ^ finrank ℚ K
have rw : (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
    (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1) =
  |c| ^ finrank ℚ K
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
    mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
rw :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
        1) =
    |c| ^ finrank ℚ K
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c| ^ finrank ℚ K
have rw₁ : HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ) = |c| ^ finrank ℚ K
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
    mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
rw :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
        1) =
    |c| ^ finrank ℚ K
rw₁ : HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ) = |c| ^ finrank ℚ K
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c| ^ finrank ℚ K
have rw₂ : |c| ^ finrank ℚ K * 1 = |c| ^ finrank ℚ K
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
    mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
rw :
  (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
        1) =
    |c| ^ finrank ℚ K
rw₁ : HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) 1 : ℝ) = |c| ^ finrank ℚ K
rw₂ : |c| ^ finrank ℚ K * 1 = |c| ^ finrank ℚ K
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c| ^ finrank ℚ K
have rw₃ : |c| ^ finrank ℚ K = |c| ^ finrank ℚ K
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
    mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) : ℝ)
have simp_rw : Eq (α := ℝ)
  (∏ w : InfinitePlace K,
    HPow.hPow (α := ℝ)
      ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
      w.mult)
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
simp_rw :
  Eq (α := ℝ)
    (∏ w : InfinitePlace K,
      HPow.hPow (α := ℝ)
        ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
        w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) : ℝ)
have simp_rw₁ : Eq (α := ℝ) (∏ x_1 : InfinitePlace K, HPow.hPow (α := ℝ) ((x_1 : (a : K) → ℝ) x : ℝ) x_1.mult)
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw : Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)| : ℝ) 1
Tactic: rw [norm_eq_norm, Units.norm, Rat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
rw : Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)| : ℝ) 1
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw₁ : Eq (α := ℝ) (↑1 : ℝ) 1
Tactic: rw [norm_eq_norm, Units.norm, Rat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : (𝓞 K)ˣ
rw : Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)| : ℝ) 1
rw₁ : Eq (α := ℝ) (↑1 : ℝ) 1
⊢ Eq (α := ℝ)
    ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K) :
      ℝ)
    (1 : ℝ)
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [norm_eq_norm, Units.norm, Rat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
hx : Membership.mem (γ := Set (mixedSpace K)) (Set.range (ι := K) (⇑(mixedEmbedding K) : (a : K) → mixedSpace K)) x
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔ x = 0
have obtain : ∀ (a : K),
  Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
Tactic: obtain ⟨a, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
have rw : Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) 0 ↔
  Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
Tactic: rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
rw :
  Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
have rw₁ : Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ)| 0 ↔
  Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
Tactic: rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
rw :
  Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₁ :
  Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ)| 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
have rw₂ : Eq (α := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ) 0 ↔
  Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
Tactic: rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
rw :
  Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₁ :
  Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ)| 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₂ :
  Eq (α := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
have rw₃ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) a : ℚ) (0 : ℚ) ↔
  Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
Tactic: rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
rw :
  Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₁ :
  Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ)| 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₂ :
  Eq (α := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₃ :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) a : ℚ) (0 : ℚ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
have rw₄ : a = 0 ↔ Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
Tactic: rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
rw :
  Eq (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) a| : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₁ :
  Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ)| 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₂ :
  Eq (α := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) a) : ℝ) 0 ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₃ :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) a : ℚ) (0 : ℚ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
rw₄ : a = 0 ↔ Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
⊢ Eq (α := ℝ)
      ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) :
        ℝ)
      (0 : ℝ) ↔
    Eq (α := mixedSpace K) ((mixedEmbedding K : (a : K) → mixedSpace K) a : mixedSpace K) (0 : mixedSpace K)
have rw₅ : a = 0 ↔ a = 0
Tactic: rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Continuous.{u_1, 0} (X := mixedSpace K) (Y := ℝ) (⇑mixedEmbedding.norm : (a : mixedSpace K) → ℝ)
have refine : ∀ (x : InfinitePlace K),
  Membership.mem (γ := Finset (InfinitePlace K)) univ x →
    Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
      HPow.hPow (α := ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ) x.mult
Tactic: refine continuous_finsetProd Finset.univ fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ x
⊢ Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    HPow.hPow (α := ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ) x.mult
have simp_rw : Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
  if h : x.IsReal then ‖a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) x h)‖ ^ x.mult
  else ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) x sorry)‖ ^ x.mult
Tactic: simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dite_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ x
⊢ Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    if h : x.IsReal then ‖a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) x h)‖ ^ x.mult
    else ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) x ⋯)‖ ^ x.mult
have pos : ∀ (h : x.IsReal),
  Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    ‖a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) x h)‖ ^ x.mult
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ x
pos :
  ∀ (h : x.IsReal),
    Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
      ‖a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) x h)‖ ^ x.mult
⊢ Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    if h : x.IsReal then ‖a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) x h)‖ ^ x.mult
    else ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) x ⋯)‖ ^ x.mult
have neg : ∀ (h : ¬x.IsReal),
  Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) x sorry)‖ ^ x.mult
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ fundamentalDomain (ι := index K) (K := ℝ) (stdBasis K) =
    SProd.sprod (α := Set ((i : { w : InfinitePlace K // w.IsReal }) → ℝ)) (β :=
      Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℂ))
      (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) Set.univ
        fun (x : { w : InfinitePlace K // w.IsReal }) ↦ Set.Ico 0 1)
      (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ) Set.univ
        fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
        Set.preimage (β := Fin 2 → ℝ) (⇑measurableEquivPi : (a : ℂ) → Fin 2 → ℝ)
          (Set.pi (α := fun (a : Fin 2) ↦ ℝ) Set.univ fun (x : Fin 2) ↦ Set.Ico 0 1))
have h : ∀ (x : mixedSpace K),
  Membership.mem (γ := Set (mixedSpace K)) (fundamentalDomain (ι := index K) (K := ℝ) (stdBasis K)) x ↔
    x ∈
      SProd.sprod (α := Set ((i : { w : InfinitePlace K // w.IsReal }) → ℝ)) (β :=
        Set ((i : { w : InfinitePlace K // w.IsComplex }) → ℂ))
        (Set.pi (α := fun (i : { w : InfinitePlace K // w.IsReal }) ↦ ℝ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsReal }) ↦ Set.Ico 0 1)
        (Set.pi (α := fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ) Set.univ
          fun (x : { w : InfinitePlace K // w.IsComplex }) ↦
          Set.preimage (β := Fin 2 → ℝ) (⇑measurableEquivPi : (a : ℂ) → Fin 2 → ℝ)
            (Set.pi (α := fun (a : Fin 2) ↦ ℝ) Set.univ fun (x : Fin 2) ↦ Set.Ico 0 1))
Tactic: ext