awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
simp_rw :
  ¬¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₁ :
  (¬¬∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₂ :
  (∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₃ :
  (∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ∃ (x_1 : InfinitePlace K), ¬¬Eq (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ ¬Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]

Premises used: Classical.not_not, ne_eq, NumberField.mixedEmbedding.norm_eq_zero_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (c • x) =
    HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq]

Premises used: NumberField.InfinitePlace.sum_mult_eq, Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, NumberField.mixedEmbedding.normAtPlace_smul, mul_pow, NumberField.mixedEmbedding.norm_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
⊢ (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

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
rw₃ rw₄ : |c| ^ finrank ℚ K = |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

Tactic:
rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, norm_smul, map_one,
    mul_one]

Premises used: NumberField.mixedEmbedding.norm_smul, map_one, mul_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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| : ℝ)
simp_rw₁ :
  Eq (α := ℝ) (∏ x_1 : InfinitePlace K, HPow.hPow (α := ℝ) ((x_1 : (a : K) → ℝ) x : ℝ) x_1.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| : ℝ) : ℝ)

Tactic:
simp_rw [mixedEmbedding.norm_apply, normAtPlace_apply, prod_eq_abs_norm]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply, NumberField.InfinitePlace.prod_eq_abs_norm, NumberField.mixedEmbedding.norm_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
rw₂ 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 : ℝ)

Tactic:
rw [norm_eq_norm, Units.norm, Rat.cast_one]

Premises used: NumberField.mixedEmbedding.norm_eq_norm, NumberField.Units.norm, Rat.cast_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔ x = 0

Tactic:
obtain ⟨a, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
rw₅ rw₆ : a = 0 ↔ a = 0
⊢ 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:
rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
    map_eq_zero]

Premises used: NumberField.mixedEmbedding.norm_eq_norm, map_eq_zero, Rat.cast_abs, abs_eq_zero, Algebra.norm_eq_zero_iff, Rat.cast_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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) → ℝ)

Tactic:
continuous_finsetProd Finset.univ fun _ _ ↦ ?_

Premises used: Multiset.foldr, Finset.univ, Multiset.prod, Multiset.dedup, Finset.prod, continuous_finsetProd
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ Continuous.{u_1, 0} (X := mixedSpace K) (Y := ℝ) (⇑mixedEmbedding.norm : (a : mixedSpace K) → ℝ)

Tactic:
refine continuous_finsetProd Finset.univ fun _ _ ↦ ?_

Premises used: Finset.univ, continuous_finsetProd
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ x
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 ⋯)‖ ^ x.mult
⊢ Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    HPow.hPow (α := ℝ) ((normAtPlace x : (a : mixedSpace K) → ℝ) a : ℝ) x.mult

Tactic:
simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dite_pow]

Premises used: dite_pow, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, NumberField.mixedEmbedding.normAtPlace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
neg :
  ∀ (h : ¬x.IsReal),
    Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
      ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) x ⋯)‖ ^ 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

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ x
h_1 : x.IsReal
⊢ Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    ‖a.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) x h_1)‖ ^ x.mult

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfinitePlace K
h : Membership.mem (γ := Finset (InfinitePlace K)) univ x
h_1 : ¬x.IsReal
⊢ Continuous (Y := ℝ) fun (a : mixedSpace K) ↦
    ‖a.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) x ⋯)‖ ^ x.mult

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
⊢ (((Basis.repr (stdBasis K) : (a : mixedSpace K) → index K →₀ ℝ) x : index K →₀ ℝ) : (a : index K) → ℝ) (Sum.inl w) =
    x.1 w

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
⊢ (((Basis.repr (stdBasis K) : (a : mixedSpace K) → index K →₀ ℝ) x : index K →₀ ℝ) : (a : index K) → ℝ)
      (Sum.inr (w, 0)) =
    (x.2 w).re

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl, Sum.elim
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
⊢ (((Basis.repr (stdBasis K) : (a : mixedSpace K) → index K →₀ ℝ) x : index K →₀ ℝ) : (a : index K) → ℝ)
      (Sum.inr (w, 1)) =
    (x.2 w).im

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl, Sum.elim
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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:
simp [stdBasis, mem_fundamentalDomain, Complex.measurableEquivPi]

Premises used: NumberField.mixedEmbedding.stdBasis, Complex.measurableEquivPi, ZSpan.mem_fundamentalDomain
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  NullMeasurableSet (α := Fin 2 → ℝ) (Set.pi (α := fun (a : Fin 2) ↦ ℝ) Set.univ fun (x : Fin 2) ↦ Set.Ico 0 1) volume
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        (fundamentalDomain (ι := index K) (K := ℝ) (stdBasis K)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
    Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico,
    sub_zero, ENNReal.ofReal_one, prod_const_one, prod_const_one, prod_const_one, one_mul]

Premises used: MeasureTheory.volume_pi, sub_zero, Real.volume_Ico, MeasureTheory.Measure.prod_prod, ENNReal.ofReal_one, MeasureTheory.Measure.volume_eq_prod, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, Finset.prod_const_one, Complex.volume_preserving_equiv_pi, MeasureTheory.Measure.pi_pi, one_mul, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ NullMeasurableSet (α := Fin 2 → ℝ) (Set.pi (α := fun (a : Fin 2) ↦ ℝ) Set.univ fun (x : Fin 2) ↦ Set.Ico 0 1) volume

Tactic:
(MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)).nullMeasurableSet

Premises used: measurableSet_Ico, MeasurableSet.nullMeasurableSet, Set.countable_univ, MeasurableSet.pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ NullMeasurableSet (α := Fin 2 → ℝ) (Set.pi (α := fun (a : Fin 2) ↦ ℝ) Set.univ fun (x : Fin 2) ↦ Set.Ico 0 1) volume

Tactic:
exact (MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)).nullMeasurableSet

Premises used: measurableSet_Ico, MeasurableSet.nullMeasurableSet, Set.countable_univ, MeasurableSet.pi
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 : (c : index K) → K →+* ℂ
refine_2 :
  Function.Surjective (β := K →+* ℂ) fun (c : index K) ↦
    Sum.casesOn (motive :=
      fun (t : { w : InfinitePlace K // w.IsReal } ⊕ { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦
      (h : c = t) → K →+* ℂ) c
      (fun (w : { w : InfinitePlace K // w.IsReal }) (h : c = Sum.inl w) ↦ (↑w : InfinitePlace K).embedding)
      (fun (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) (h : c = Sum.inr wj) ↦
        Prod.casesOn (motive := fun (x : { w : InfinitePlace K // w.IsComplex } × Fin 2) ↦ K →+* ℂ) wj
          fun (w : { w : InfinitePlace K // w.IsComplex }) (j : Fin 2) ↦
          if j = 0 then (↑w : InfinitePlace K).embedding
          else ComplexEmbedding.conjugate (↑w : InfinitePlace K).embedding)
      ⋯
refine_3 : Fintype.card.{u_1} (index K) = Fintype.card.{u_1} (K →+* ℂ)
⊢ index K ≃ (K →+* ℂ)

Tactic:
refine Equiv.ofBijective (fun c => ?_)
    ((Fintype.bijective_iff_surjective_and_card _).mpr ⟨?_, ?_⟩)

Premises used: Iff.mpr, Fintype.bijective_iff_surjective_and_card, And.intro, Equiv.ofBijective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
⊢ K →+* ℂ

Tactic:
exact w.val.embedding

Premises used: NumberField.InfinitePlace.embedding, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
wj : { w : InfinitePlace K // w.IsComplex } × Fin 2
refine_1 : (w : { w : InfinitePlace K // w.IsComplex }) → (j : Fin 2) → K →+* ℂ
⊢ K →+* ℂ

Tactic:
rcases wj with ⟨w, j⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsComplex }
j : Fin 2
⊢ K →+* ℂ

Tactic:
exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding

Premises used: NumberField.ComplexEmbedding.conjugate, NumberField.InfinitePlace.embedding, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : index K
refine_1 : (w : { w : InfinitePlace K // w.IsReal }) → K →+* ℂ
refine_1₁ : (wj : { w : InfinitePlace K // w.IsComplex } × Fin 2) → K →+* ℂ
⊢ K →+* ℂ

Tactic:
cases c with
    | inl w => exact w.val.embedding
    | inr wj => rcases wj with ⟨w, j⟩
                exact if j = 0 then w.val.embedding else ComplexEmbedding.conjugate w.val.embedding