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
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
have 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 φ)
Tactic: refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x φ) : ℂ)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x (ComplexEmbedding.conjugate φ) : ℂ)
have refine_1 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
  ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x (ComplexEmbedding.conjugate φ) : ℂ)
Tactic: rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ) : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x φ) : ℂ)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x (ComplexEmbedding.conjugate φ) : ℂ)
have refine_1₁ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
  ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ)
Tactic: rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x φ) : ℂ)
    ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x (ComplexEmbedding.conjugate φ) : ℂ)
have refine_1₂ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ)
Tactic: rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
have refine_2 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
Tactic: rw [Pi.zero_apply, Pi.zero_apply, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ) : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
have refine_2₁ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ) (0 : ℂ)
Tactic: rw [Pi.zero_apply, Pi.zero_apply, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
have refine_2₂ : Eq (α := ℂ) 0 0
Tactic: rw [Pi.zero_apply, Pi.zero_apply, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((x_1 + x_2) φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
have refine_3 : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ + x_2 φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((x_1 + x_2) φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
have refine_3₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ + x_2 φ) = x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((x_1 + x_2) φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
have refine_3₂ : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_2 φ) : ℂ) =
  x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((x_1 + x_2) φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
have refine_3₃ : HAdd.hAdd (β := ℂ) (x_1 (ComplexEmbedding.conjugate φ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_2 φ) : ℂ) =
  x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((x_1 + x_2) φ) = (x_1 + x_2) (ComplexEmbedding.conjugate φ)
have refine_3₄ : x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ) =
  x_1 (ComplexEmbedding.conjugate φ) + x_2 (ComplexEmbedding.conjugate φ)
Tactic: rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) ((a • x_1) φ) = (a • x_1) (ComplexEmbedding.conjugate φ)
have refine_4 : HMul.hMul (β := ℂ) (↑a : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) : ℂ) = (a • x_1) (ComplexEmbedding.conjugate φ)
Tactic: rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]
-- 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
r : ℝ
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have inl : ∀ (hr : r < 0),
  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
-- 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
r : ℝ
inl :
  ∀ (hr : r < 0),
    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
have inr : ∀ (hr : 0 ≤ 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
-- 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
r : ℝ
hr : r < 0
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have inl : ∀ (φ : K →+* ℂ),
  norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
Tactic: obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))
-- 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
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have inl : ¬norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
Tactic: refine iff_of_false ?_ ?_
-- 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
r : ℝ
hr : r < 0
φ : K →+* ℂ
inl : ¬norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have inl₁ : ¬∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
Tactic: refine iff_of_false ?_ ?_
-- 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
r : ℝ
hr : 0 ≤ r
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ r ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
have inr : ∀ (r : NNReal),
  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
Cleared hypotheses: r, hr
-- 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
r : NNReal
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ (↑r : ℝ)
have inr : (↑(nnnorm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ)) : ℝ) ≤ (↑r : ℝ) ↔
  ∀ (φ : K →+* ℂ), (↑(nnnorm (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]
-- 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
r : NNReal
inr :
  (↑(nnnorm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ)) : ℝ) ≤ (↑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 : ℝ)
have inr₁ : (↑(Finset.sup Finset.univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)) : ℝ) ≤ (↑r : ℝ) ↔
  ∀ (φ : K →+* ℂ), (↑(nnnorm (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]
-- 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
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 : ℝ)
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ (↑r : ℝ)
have inr₂ : (Finset.sup Finset.univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)) ≤ r ↔
  ∀ (φ : K →+* ℂ), nnnorm (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]
-- 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
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
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ (↑r : ℝ)
have inr₃ : (∀ (b : K →+* ℂ),
    Membership.mem (γ := Finset (K →+* ℂ)) Finset.univ b → nnnorm (E := ℂ) ((b : (a : K) → ℂ) x : ℂ) ≤ r) ↔
  ∀ (φ : K →+* ℂ), nnnorm (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]
-- 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
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
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x : (K →+* ℂ) → ℂ) ≤ (↑r : ℝ) ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ (↑r : ℝ)
have inr₄ : (∀ (b : K →+* ℂ), True → nnnorm (E := ℂ) ((b : (a : K) → ℂ) x : ℂ) ≤ r) ↔
  ∀ (φ : K →+* ℂ), nnnorm (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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
r : ℝ
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
have inl : ∀ (hr : r < 0), ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
Tactic: obtain hr | _ := lt_or_ge r 0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
have inr : 0 ≤ r → ((↑(integerLattice K) : Set ((K →+* ℂ) → ℂ)) ∩ Metric.closedBall 0 r).Finite
Tactic: obtain hr | _ := lt_or_ge r 0