awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
⊢ ∃ (i : ℤ[X]) (_ :
    i.natDegree ≤ finrank ℚ K ∧ ∀ (i_1 : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (i.coeff i_1)),
    x ∈ (↑(roots (map (algebraMap ℤ K) i)).toFinset : Set K)
have h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
Tactic: have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ ∃ (i : ℤ[X]) (_ :
    i.natDegree ≤ finrank ℚ K ∧ ∀ (i_1 : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (i.coeff i_1)),
    x ∈ (↑(roots (map (algebraMap ℤ K) i)).toFinset : Set K)
have refine_1 : natDegree (minpoly ℤ x) ≤ finrank ℚ K
Tactic: refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
refine_1 : natDegree (minpoly ℤ x) ≤ finrank ℚ K
⊢ ∃ (i : ℤ[X]) (_ :
    i.natDegree ≤ finrank ℚ K ∧ ∀ (i_1 : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (i.coeff i_1)),
    x ∈ (↑(roots (map (algebraMap ℤ K) i)).toFinset : Set K)
have refine_2 : ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ x) i)
Tactic: refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℤ x) ≤ finrank ℚ K
have refine_1 : natDegree (minpoly ℚ x) ≤ finrank ℚ K
Tactic: rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ x) i)
have refine_2 : LE.le (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) (↑(↑C : ℤ) : ℝ)
Tactic: rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ LE.le (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) (↑(↑C : ℤ) : ℝ)
have refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
Tactic: refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
have refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
Tactic: rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
have refine_2₁ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (coeff (minpoly ℤ x) i) : ℚ)
Tactic: rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
refine_2₁ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (coeff (minpoly ℤ x) i) : ℚ)
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
have refine_2₂ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) (↑(coeff (minpoly ℤ x) i) : ℚ)
Tactic: rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
refine_2₁ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (coeff (minpoly ℤ x) i) : ℚ)
refine_2₂ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) (↑(coeff (minpoly ℤ x) i) : ℚ)
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
have refine_2₃ : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℤ x) i‖
Tactic: rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
refine_2₁ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (coeff (minpoly ℤ x) i) : ℚ)
refine_2₂ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) (↑(coeff (minpoly ℤ x) i) : ℚ)
refine_2₃ : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℤ x) i‖
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
have refine_2₄ : Eq (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) |(↑(coeff (minpoly ℤ x) i) : ℝ)|
Tactic: rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊
this :
  Set.Finite.{u_1} (α := K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
x : K
hx :
  Membership.mem (γ := Set K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖(map (algebraMap ℤ ℚ) (minpoly ℤ x)).coeff i‖
refine_2₁ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (coeff (minpoly ℤ x) i) : ℚ)
refine_2₂ : (↑|coeff (minpoly ℤ x) i| : ℝ) = norm (E := ℚ) (↑(coeff (minpoly ℤ x) i) : ℚ)
refine_2₃ : (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℤ x) i‖
refine_2₄ : Eq (α := ℝ) (↑|coeff (minpoly ℤ x) i| : ℝ) |(↑(coeff (minpoly ℤ x) i) : ℝ)|
⊢ (↑|coeff (minpoly ℤ x) i| : ℝ) = ‖coeff (minpoly ℚ x) i‖
have refine_2₅ : Eq (α := ℝ) |(↑(coeff (minpoly ℤ x) i) : ℝ)| |(↑(coeff (minpoly ℤ x) i) : ℝ)|
Tactic: rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
let let₁ let₂ :
  Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
⊢ Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
have let₃ : let C := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊;
∀
  (this :
    Set.Finite.{u_1} (α := K)
      (⋃ (f : ℤ[X]),
        ⋃ (_ :
          f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
          (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))),
  Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
Tactic: classical
  let C := Nat.ceil (max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2))
  have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
  refine this.subset fun x hx => ?_; simp_rw [mem_iUnion]
  have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
  refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
  · rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
    exact minpoly.natDegree_le x
  rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
  refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
  rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
B : ℝ
let let₁ let₂ :
  Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
let₃ :
  let C := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊;
  ∀
    (this :
      Set.Finite.{u_1} (α := K)
        (⋃ (f : ℤ[X]),
          ⋃ (_ :
            f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
            (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))),
    Set.Finite.{u_1} (α := K)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
⊢ Set.Finite.{u_1} (α := K)
    {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B}
have let₄ : let C := ⌈max B 1 ^ finrank ℚ K * (↑((finrank ℚ K).choose (finrank ℚ K / 2)) : ℝ)⌉₊;
∀
  (this :
    Set.Finite.{u_1} (α := K)
      (⋃ (f : ℤ[X]),
        ⋃ (_ :
          f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
          (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K)))
  (x : K)
  (hx :
    Membership.mem (γ := Set K)
      {x : K | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ B} x),
  Membership.mem (γ := Set K)
    (⋃ (f : ℤ[X]),
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
        (↑(roots (map (algebraMap ℤ K) f)).toFinset : Set K))
    x
Tactic: classical
  let C := Nat.ceil (max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2))
  have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
  refine this.subset fun x hx => ?_; simp_rw [mem_iUnion]
  have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
  refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
  · rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
    exact minpoly.natDegree_le x
  rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
  refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
  rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
have obtain : ∀ (a b : ℕ) (habne : a ≠ b) (h : x ^ a = x ^ b), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
Tactic: obtain ⟨a, -, b, -, habne, h⟩ :=
    Set.Infinite.exists_ne_map_eq_of_mapsTo (f := (x ^ · : ℕ → K)) Set.infinite_univ
      (fun a _ => mem_setOf.mpr <|
        ⟨hxi.pow a, fun φ => by simp [pow_le_one₀ (norm_nonneg (φ x)) <| hx φ]⟩)
      (finite_of_norm_le K A (1 : ℝ))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
have inr : ∀
  (this :
    ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
      [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
      (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
      (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1)
  (hlt : ¬b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
Tactic: wlog hlt : b < a
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
inr :
  ∀
    (this :
      ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
        [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
        (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
        (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1)
    (hlt : ¬b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
have wlog : ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_6 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] {x : K} (hx₀ : x ≠ 0) (hxi : IsIntegral ℤ x)
  (hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1) (a b : ℕ) (habne : a ≠ b)
  (h : x ^ a = x ^ b) (hlt : b < a), ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
Tactic: wlog hlt : b < a
Cleared hypotheses: inst_1, inst_3, inst_4, x, hx₀, hxi, hx, a, b, habne, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
have refine : x ^ (a - b) = 1
Tactic: refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
Goal:
K_1 : Type u_1
inst : Field K_1
A_1 : Type u_2
inst_1 : NormedField A_1
K : Type u_1
inst_2 : Field K
inst_3 : NumberField K
A : Type u_2
inst_4 : NormedField A
inst_5 : IsAlgClosed A
inst_6 : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1
have h₁ : x ^ (a - b) = 1 ∨ x ^ b = 0
Tactic: rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h
Cleared hypotheses: h, hlt
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) x : A) = 1
⊢ ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1
have apply : x ≠ 0
Tactic: apply pow_eq_one_of_norm_le_one K A _ hxi fun φ ↦ le_of_eq <| hx φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
A : Type u_2
inst_2 : NormedField A
inst_3 : IsAlgClosed A
inst_4 : NormedAlgebra ℚ A
hxi : IsIntegral.{0, u_1} ℤ (A := K) 0
hx : ∀ (φ : K →+* A), norm.{u_2} (E := A) ((φ : (a : K) → A) 0 : A) = 1
⊢ False
have hx₁ : ∀ (φ : K →+* A), False
Tactic: simp_rw [map_zero, norm_zero, zero_ne_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (goal)
Goal:
K : Type u_1
inst : Field K
k : Type u_2
inst_1 : Field k
inst_2 : Algebra k K
inst_3 : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (AlgHom.toRingHom.{u_2, u_1, 0} (R := k) IsAlgClosed.lift)
      (algebraMap k K) =
    φ
have rw : @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑IsAlgClosed.lift : K →+* ℂ) (algebraMap k K) = φ
Tactic: rw [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower, RingHom.algebraMap_toAlgebra']