awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯

Tactic:
have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
⊢ IsTotallyComplex.{u_1} ↥ℚ⟮ζ⟯

Tactic:
have : IsTotallyComplex ℚ⟮ζ⟯ := isTotallyComplex ℚ⟮ζ⟯ hn₂
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this_3 : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
this : IsTotallyComplex.{u_1} ↥ℚ⟮ζ⟯
⊢ IsTotallyComplex K

Tactic:
isTotallyComplex_of_algebra ℚ⟮ζ⟯ K

Premises used: Rat, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, NumberField.isTotallyComplex_of_algebra
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this_3 : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
this : IsTotallyComplex.{u_1} ↥ℚ⟮ζ⟯
⊢ IsTotallyComplex K

Tactic:
exact isTotallyComplex_of_algebra ℚ⟮ζ⟯ K

Premises used: Rat, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, NumberField.isTotallyComplex_of_algebra
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsTotallyComplex K

Tactic:
have : IsTotallyComplex K := by
    have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ
    have : IsTotallyComplex ℚ⟮ζ⟯ := isTotallyComplex ℚ⟮ζ⟯ hn₂
    exact isTotallyComplex_of_algebra ℚ⟮ζ⟯ K
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this : IsTotallyComplex K
⊢ IsAbelianGalois ℚ K

Tactic:
have := isAbelianGalois S ℚ K
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this_3 : IsTotallyComplex K
this : IsAbelianGalois ℚ K
⊢ IsCMField K

Tactic:
IsCMField.of_isAbelianGalois K

Premises used: NumberField.IsCMField.of_isAbelianGalois
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this_3 : IsTotallyComplex K
this : IsAbelianGalois ℚ K
⊢ IsCMField K

Tactic:
exact IsCMField.of_isAbelianGalois K

Premises used: NumberField.IsCMField.of_isAbelianGalois
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension ⊤ ℚ K
⊢ IsCMField K

Tactic:
isCMField K (S := ⊤) ⟨3, trivial, Nat.lt_succ_self 2⟩

Premises used: trivial, Nat.lt_succ_self, And.intro, Exists.intro, OfNat.ofNat, IsCyclotomicExtension.Rat.isCMField
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Function.Injective (α := K) (β := (K →+* ℂ) → ℂ) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)

Tactic:
RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
⊢ Eq (α := ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x φ : ℂ) ((φ : (a : K) → ℂ) x : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

Tactic:
Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx

Premises used: Submodule.span_induction
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
refine_1 :
  ∀ (x : (K →+* ℂ) → ℂ)
    (h :
      Membership.mem (γ := Set ((K →+* ℂ) → ℂ)) (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
        x),
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
refine_2 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
refine_3 :
  ∀ (x x_1 : (K →+* ℂ) → ℂ),
    Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
        (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x →
      Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
          (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1 →
        ∀ (hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ))
          (hy : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) = x_1 (ComplexEmbedding.conjugate φ)),
          (starRingEnd ℂ : (a : ℂ) → ℂ) ((x + x_1) φ) = (x + x_1) (ComplexEmbedding.conjugate φ)
refine_4 :
  ∀ (a : ℝ) (x : (K →+* ℂ) → ℂ),
    Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
        (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x →
      ∀ (hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)),
        (starRingEnd ℂ : (a : ℂ) → ℂ) ((a • x) φ) = (a • x) (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

Tactic:
refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x_1 : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1
x : K
refine_1 :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x (ComplexEmbedding.conjugate φ) : ℂ)
refine_1₁ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
    ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ)
refine_1₂ refine_1₃ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x φ) : ℂ)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x (ComplexEmbedding.conjugate φ) : ℂ)

Tactic:
rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]

Premises used: NumberField.canonicalEmbedding.apply_at, NumberField.ComplexEmbedding.conjugate_coe_eq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
refine_2 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
refine_2₁ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ) (0 : ℂ)
refine_2₂ refine_2₃ : Eq (α := ℂ) 0 0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)

Tactic:
rw [Pi.zero_apply, Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx_1 :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
x_1 x_2 : (K →+* ℂ) → ℂ
h :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1
h_1 :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_2
hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) = x_1 (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_2 φ) = x_2 (ComplexEmbedding.conjugate φ)
refine_3 : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ + x_2 φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
refine_3₁ :
  (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ + x_2 φ) =
    x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
refine_3₂ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_2 φ) : ℂ) =
    x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
refine_3₃ :
  HAdd.hAdd (β := ℂ) (x_1 (ComplexEmbedding.conjugate φ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_2 φ) : ℂ) =
    x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
refine_3₄ refine_3₅ :
  x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ) =
    x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((x_1 + x_2) φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)

Tactic:
rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]

Premises used: map_add, Pi.add_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx_1 :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
a : ℝ
x_1 : (K →+* ℂ) → ℂ
h :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1
hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) = x_1 (ComplexEmbedding.conjugate φ)
refine_4 :
  HMul.hMul (β := ℂ) (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) : ℂ) = (a • x_1) (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((a • x_1) φ) = (a • x_1) (ComplexEmbedding.conjugate φ)

Tactic:
rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]

Premises used: Complex.real_smul, map_mul, Complex.conj_ofReal, Pi.smul_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx_1 :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
a : ℝ
x_1 : (K →+* ℂ) → ℂ
h :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1
hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) = x_1 (ComplexEmbedding.conjugate φ)
⊢ HMul.hMul (β := ℂ) (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) : ℂ) = (a • x_1) (ComplexEmbedding.conjugate φ)

Tactic:
congrArg ((a : ℂ) * ·) hx

Premises used: HMul.hMul, congrArg, Complex.ofReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx_1 :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
a : ℝ
x_1 : (K →+* ℂ) → ℂ
h :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1
hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) = x_1 (ComplexEmbedding.conjugate φ)
⊢ HMul.hMul (β := ℂ) (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) : ℂ) = (a • x_1) (ComplexEmbedding.conjugate φ)

Tactic:
exact congrArg ((a : ℂ) * ·) hx

Premises used: HMul.hMul, congrArg, Complex.ofReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
inl :
  ∀ (hr : r < 0),
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
inr :
  ∀ (hr : 0 ≤ r),
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
obtain hr | hr := lt_or_ge r 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
inl :
  ∀ (φ : K →+* ℂ),
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
iff_of_false ?_ ?_

Premises used: iff_of_false
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
inl : ¬norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
inl₁ : ¬∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
refine iff_of_false ?_ ?_

Premises used: iff_of_false
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r

Tactic:
(hr.trans_le (norm_nonneg _)).not_ge

Premises used: LT.lt.trans_le, LT.lt.not_ge, norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r

Tactic:
exact (hr.trans_le (norm_nonneg _)).not_ge

Premises used: LT.lt.trans_le, LT.lt.not_ge, norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
fun h => hr.not_ge (le_trans (norm_nonneg _) (h φ))

Premises used: LT.lt.not_ge, DFunLike.coe, Not, norm_nonneg, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
exact fun h => hr.not_ge (le_trans (norm_nonneg _) (h φ))

Premises used: LT.lt.not_ge, norm_nonneg, le_trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
inr :
  ∀ (r : NNReal),
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ (↑r : ℝ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ (↑r : ℝ)
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
lift r to NNReal using hr

Premises used: NNReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
r : NNReal
inr :
  (↑(nnnorm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ)) : ℝ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), (↑(nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)) : ℝ) ≤ (↑r : ℝ)
inr₁ :
  (↑(Finset.sup Finset.univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)) : ℝ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), (↑(nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)) : ℝ) ≤ (↑r : ℝ)
inr₂ :
  (Finset.sup Finset.univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)) ≤ r ↔
    ∀ (φ : K →+* ℂ), nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
inr₃ :
  (∀ (b : K →+* ℂ),
      Membership.mem (γ := Finset (K →+* ℂ)) Finset.univ b → nnnorm (E := ℂ) ((b : (a : K) → ℂ) x : ℂ) ≤ r) ↔
    ∀ (φ : K →+* ℂ), nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
inr₄ :
  (∀ (b : K →+* ℂ), True → nnnorm (E := ℂ) ((b : (a : K) → ℂ) x : ℂ) ≤ r) ↔
    ∀ (φ : K →+* ℂ), nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ (↑r : ℝ)

Tactic:
simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ,
      forall_true_left]

Premises used: Finset.mem_univ, forall_true_left, NumberField.canonicalEmbedding.nnnorm_eq, coe_nnnorm, Finset.sup_le_iff, NNReal.coe_le_coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
inl : ∀ (hr : r < 0), ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
inr : 0 ≤ r → ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite

Tactic:
obtain hr | _ := lt_or_ge r 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
hr : r < 0
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite

Tactic:
simp [Metric.closedBall_eq_empty.2 hr]

Premises used: Iff.mpr, Metric.closedBall_eq_empty
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
x : K
rw :
  Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
      ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
rw₁ rw₂ :
  norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
      ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
rw [← norm_le_iff, mem_closedBall_zero_iff]

Premises used: NumberField.canonicalEmbedding.norm_le_iff, mem_closedBall_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
⊢ ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r

Tactic:
have heq : ∀ x, canonicalEmbedding K x ∈ Metric.closedBall 0 r ↔
        ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r := by
      intro x; rw [← norm_le_iff, mem_closedBall_zero_iff]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
⊢ Set.Finite (α := (K →+* ℂ) → ℂ)
    (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})

Tactic:
(Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)

Premises used: Set.Finite.image, NumberField.Embeddings.finite_of_norm_le, NumberField.canonicalEmbedding, Complex, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h_1 : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
h :
  (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r =
    Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r}
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite

Tactic:
convert! (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)

Premises used: Set.Finite.image, NumberField.Embeddings.finite_of_norm_le, NumberField.canonicalEmbedding, Complex, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
h_1 : 0 ≤ r
heq :
  ∀ (x : K),
    Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ)) (Metric.closedBall 0 r)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ↔
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
h :
  ∀ (x : (K →+* ℂ) → ℂ),
    x ∈ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r ↔
      Membership.mem (γ := Set ((K →+* ℂ) → ℂ))
        (Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
          {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r})
        x
⊢ (↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r =
    Set.image (α := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r}

Tactic:
ext