awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
h_card :
  Set.ncard (α := ℤ[X])
      {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} =
    ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)
h_subset :
  Subset (α := Set ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)}
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}
h_finite :
  Set.Finite (α := ℤ[X])
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}
⊢ Set.Finite (α := ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)} ∧
    Set.ncard (α := ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)} ≤
      Set.ncard (α := ℤ[X])
        {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}

Tactic:
⟨h_finite.subset h_subset, Set.ncard_le_ncard h_subset h_finite⟩

Premises used: Set.Finite.subset, And.intro, Set.ncard_le_ncard
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
h_card :
  Set.ncard (α := ℤ[X])
      {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} =
    ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)
h_subset :
  Subset (α := Set ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)}
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}
h_finite :
  Set.Finite (α := ℤ[X])
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}
⊢ Set.Finite (α := ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)} ∧
    Set.ncard (α := ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)} ≤
      Set.ncard (α := ℤ[X])
        {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}

Tactic:
exact ⟨h_finite.subset h_subset, Set.ncard_le_ncard h_subset h_finite⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
⊢ Set.Finite (α := ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)}

Tactic:
(card_mahlerMeasure n B).1

Premises used: _private.0.Polynomial.card_mahlerMeasure, And.left
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
⊢ Set.ncard (α := ℤ[X]) {p : ℤ[X] | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)} ≤
    ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)

Tactic:
(card_mahlerMeasure n B).2

Premises used: _private.0.Polynomial.card_mahlerMeasure, And.right
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
inl : ∀ (hn : n = 0), (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
inr : ∀ (hn : n ≠ 0), (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
rcases eq_or_ne n 0 with hn | hn

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n = 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this_1 : NeZero n
this : Eq (α := ℝ) (∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖) 1
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
simpa [mahlerMeasure_eq_leadingCoeff_mul_prod_roots, cyclotomic.monic n ℂ,
      Polynomial.cyclotomic.roots_eq_primitiveRoots_val]

Premises used: Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots, Polynomial.cyclotomic.roots_eq_primitiveRoots_val, Polynomial.cyclotomic.monic, Complex
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
inr : Eq (α := ℝ) (∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖) 1
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
suffices ∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖ = 1 by
    simpa [mahlerMeasure_eq_leadingCoeff_mul_prod_roots, cyclotomic.monic n ℂ,
      Polynomial.cyclotomic.roots_eq_primitiveRoots_val]
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this_1 : NeZero n
this : ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1
⊢ ∀ (x : ℝ),
    Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : ℂ) ↦ max 1 ‖x‖) (primitiveRoots n ℂ).val) x → x = 1

Tactic:
simpa
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
inr : ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1
⊢ Eq (α := ℝ) (∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖) 1

Tactic:
suffices ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1 from Multiset.prod_eq_one (by simpa)
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
x : ℂ
hz : x ∈ primitiveRoots n ℂ
⊢ ‖x‖ ≤ 1

Tactic:
(IsPrimitiveRoot.norm'_eq_one (isPrimitiveRoot_of_mem_primitiveRoots hz) hn).le

Premises used: Eq.le, IsPrimitiveRoot.norm'_eq_one, isPrimitiveRoot_of_mem_primitiveRoots
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
x : ℂ
hz : x ∈ primitiveRoots n ℂ
⊢ ‖x‖ ≤ 1

Tactic:
exact (IsPrimitiveRoot.norm'_eq_one (isPrimitiveRoot_of_mem_primitiveRoots hz) hn).le

Premises used: Eq.le, IsPrimitiveRoot.norm'_eq_one, isPrimitiveRoot_of_mem_primitiveRoots
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
inl : p = 0 → ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
inr : ∀ (hp : p ≠ 0), ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
rcases eq_or_ne p 0 with _ | hp

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
h_1 : p = 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ ≤ 1

Tactic:
have h_ineq := h ▸ (leadingCoeff_le_mahlerMeasure <| p.map (castRingHom ℂ))
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : ‖(map (castRingHom ℂ) p).leadingCoeff‖ ≤ 1
inr : ∀ (h_ineq : norm (E := ℂ) (↑p.leadingCoeff : ℂ) ≤ 1), norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast] at ⊢ h_ineq

Premises used: eq_intCast, Polynomial.leadingCoeff_map_of_injective, Int.castRingHom, Complex, RingHom.injective_int
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : norm (E := ℂ) (↑p.leadingCoeff : ℂ) ≤ 1
inr : ∀ (h_ineq : |p.leadingCoeff| ≤ 1), |p.leadingCoeff| = 1
⊢ norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1

Tactic:
norm_cast at ⊢ h_ineq
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : |p.leadingCoeff| ≤ 1
⊢ |p.leadingCoeff| = 1

Tactic:
grind [leadingCoeff_eq_zero]

Premises used: Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
have := norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one h
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
this : ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
⊢ norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1

Tactic:
rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast] at this

Premises used: eq_intCast, Polynomial.leadingCoeff_map_of_injective, Int.castRingHom, Complex, RingHom.injective_int
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
this : norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (this : |p.leadingCoeff| = 1), |p.leadingCoeff| = 1
⊢ |p.leadingCoeff| = 1

Tactic:
norm_cast at this
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ p.leadingCoeff = 1 ∨ p.leadingCoeff = -1

Tactic:
have : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1 := abs_eq_abs.mp <|
    abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one h
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (1 / p.leadingCoeff) : ℤ[X]) p).Monic

Tactic:
aesop (add safe (by simp [Monic.def]))
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
⊢ (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (1 / p.leadingCoeff) : ℤ[X]) p).Monic

Tactic:
have : (C (1 / p.leadingCoeff) * p).Monic := by aesop (add safe (by simp [Monic.def]))
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this_1 : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
this : (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (1 / p.leadingCoeff) : ℤ[X]) p).Monic
⊢ IsIntegral ℤ z

Tactic:
grind [IsIntegral, RingHom.IsIntegralElem, mem_roots', IsRoot.def, eval₂_mul, eval_map]

Premises used: Polynomial.eval_map, Polynomial.IsRoot.def, RingHom.IsIntegralElem, Polynomial.eval₂_mul, IsIntegral, Polynomial.mem_roots'
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ ‖z‖ ≤ max 1 ‖z‖

Tactic:
le_max_right 1 ‖z‖

Premises used: le_max_right, Norm.norm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ max 1 ‖z‖ ≤ prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) (map (castRingHom ℂ) p).roots)

Tactic:
mem_le_prod_of_one_le (fun a ↦ le_max_left 1 ‖a‖) hz

Premises used: Norm.norm, Multiset.mem_le_prod_of_one_le, OfNat.ofNat, le_max_left
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ LE.le (α := ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) (map (castRingHom ℂ) p).roots)) 1

Tactic:
grind [prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff,
        norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one]

Premises used: Polynomial.norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one, Polynomial.prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
max : LE.le (α := ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ Max.max 1 ‖a‖) (map (castRingHom ℂ) p).roots)) 1
⊢ ‖z‖ ≤ 1

Tactic:
calc
  ‖z‖ ≤ max 1 ‖z‖ := le_max_right 1 ‖z‖
  _   ≤ ((p.map (castRingHom ℂ)).roots.map (fun a ↦ max 1 ‖a‖)).prod :=
        mem_le_prod_of_one_le (fun a ↦ le_max_left 1 ‖a‖) hz
  _   ≤ 1 := by grind [prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff,
        norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one]

Premises used: le_max_right, Norm.norm, Polynomial.roots, Multiset.map, Multiset.prod, Multiset.mem_le_prod_of_one_le, Max.max, Int.castRingHom, Polynomial.map, Complex, OfNat.ofNat, le_max_left
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this_1 : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
this : ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1
obtain : ∀ (n : ℕ) (hn₀ : 0 < n) (hn₁ : y ^ n = 1), ∃ (n : ℕ), 0 < n ∧ z ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ z ^ n = 1

Tactic:
obtain ⟨n, hn₀, hn₁⟩ := this
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
n : ℕ
hn₀ : 0 < n
hn₁ : y ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ z ^ n = 1

Tactic:
⟨n, hn₀, congrArg (algebraMap K ℂ) hn₁⟩

Premises used: Algebra.algebraMap, congrArg, Membership.mem, Subtype, And.intro, Exists.intro, Complex, DFunLike.coe
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
n : ℕ
hn₀ : 0 < n
hn₁ : y ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ z ^ n = 1

Tactic:
exact ⟨n, hn₀, congrArg (algebraMap K ℂ) hn₁⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
suffices : ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ z ^ n = 1

Tactic:
suffices ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1 by
    obtain ⟨n, hn₀, hn₁⟩ := this
    exact ⟨n, hn₀, congrArg (algebraMap K ℂ) hn₁⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
⊢ ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1

Tactic:
NumberField.Embeddings.pow_eq_one_of_norm_le_one (x := y) K ℂ (Subtype.coe_ne_coe.mp hz₀)
    (coe_isIntegral_iff.mp <| isIntegral_of_mahlerMeasure_eq_one h hz)
    fun φ ↦ norm_root_le_one_of_mahlerMeasure_eq_one h ?_

Premises used: NumberField.Embeddings.pow_eq_one_of_norm_le_one, Set.Mem, Membership.mem, Subtype, IntermediateField.coe_isIntegral_iff, Iff.mp, Polynomial.isIntegral_of_mahlerMeasure_eq_one, Complex, Polynomial.norm_root_le_one_of_mahlerMeasure_eq_one, Subtype.coe_ne_coe
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
refine : ∀ (φ : ↥K →+* ℂ), Membership.mem (α := ℂ) (p.aroots ℂ) ((φ : (a : ↥K) → ℂ) y : ℂ)
⊢ ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1

Tactic:
refine NumberField.Embeddings.pow_eq_one_of_norm_le_one (x := y) K ℂ (Subtype.coe_ne_coe.mp hz₀)
    (coe_isIntegral_iff.mp <| isIntegral_of_mahlerMeasure_eq_one h hz)
    fun φ ↦ norm_root_le_one_of_mahlerMeasure_eq_one h ?_

Premises used: NumberField.Embeddings.pow_eq_one_of_norm_le_one, Membership.mem, Subtype, IntermediateField.coe_isIntegral_iff, Iff.mp, Polynomial.isIntegral_of_mahlerMeasure_eq_one, Complex, Polynomial.norm_root_le_one_of_mahlerMeasure_eq_one, Subtype.coe_ne_coe
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
rw :
  ∀ (hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)),
    let K : IntermediateField ℚ ℂ := ℚ⟮z⟯;
    let y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯;
    ∀ (φ : ↥K →+* ℂ),
      p ≠ 0 ∧ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ Membership.mem (α := ℂ) (p.aroots ℂ) ((φ : (a : ↥K) → ℂ) y : ℂ)

Tactic:
rw [mem_aroots] at hz ⊢

Premises used: Polynomial.mem_aroots
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
⊢ p ≠ 0 ∧ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
⟨hz.1, ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
refine : Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ p ≠ 0 ∧ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
refine ⟨hz.1, ?_⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
rw : (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) (map (RingHom.id ℤ) p) : ℂ)
| (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)

Tactic:
rw [← map_id (p := p)]

Premises used: Polynomial.map_id
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
conv_rhs :
  Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
    (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) (map (RingHom.id ℤ) p) : ℂ)
⊢ Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
    (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)

Tactic:
conv_rhs => rw [← map_id (p := p)]

Premises used: Polynomial.map_id
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
a :
  ∀ (x : ℤ),
    Eq (α := ℂ) ((RingHom.comp (algebraMap ℤ ℂ) (RingHom.id ℤ) : (a : ℤ) → ℂ) x : ℂ)
      ((ψ.comp (algebraMap ℤ ↥K) : (a : ℤ) → ℂ) x : ℂ)
⊢ RingHom.comp (algebraMap ℤ ℂ) (RingHom.id ℤ) = ψ.comp (algebraMap ℤ ↥K)

Tactic:
ext
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
x : ℤ
⊢ Eq (α := ℂ) ((RingHom.comp (algebraMap ℤ ℂ) (RingHom.id ℤ) : (a : ℤ) → ℂ) x : ℂ)
    ((ψ.comp (algebraMap ℤ ↥K) : (a : ℤ) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
⊢ Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
    (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) (map (RingHom.id ℤ) p) : ℂ)

Tactic:
exact p.map_aeval_eq_aeval_map (by ext; simp) y

Premises used: Polynomial.map_aeval_eq_aeval_map
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
⊢ ∀ (ψ : ↥K →+* ℂ),
    Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
      (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)

Tactic:
have H (ψ : K →+* ℂ) : ψ ((aeval y) p) = (aeval (ψ y)) p := by
    conv_rhs => rw [← map_id (p := p)]
    exact p.map_aeval_eq_aeval_map (by ext; simp) y
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
H :
  ∀ (ψ : ↥K →+* ℂ),
    Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
      (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
rw : Eq (α := ℂ) (((aeval ((algebraMap ↥K ℂ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
rw [← H, map_eq_zero_iff _ φ.injective,
    ← map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ↥K ℂ), H]

Premises used: Membership.mem, Subtype, RingHom.injective, map_eq_zero_iff, FaithfulSMul.algebraMap_injective, Complex
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
H :
  ∀ (ψ : ↥K →+* ℂ),
    Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
      (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
⊢ Eq (α := ℂ) (((aeval ((algebraMap ↥K ℂ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
hz.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
H :
  ∀ (ψ : ↥K →+* ℂ),
    Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
      (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
⊢ Eq (α := ℂ) (((aeval ((algebraMap ↥K ℂ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
exact hz.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
obtain : ∀ (w : ℕ), 0 < w → ∀ (hz_pow : z ^ w = 1), ∃ (n : ℕ), 0 < n ∧ IsPrimitiveRoot z n
⊢ ∃ (n : ℕ), 0 < n ∧ IsPrimitiveRoot z n

Tactic:
obtain ⟨_, _, hz_pow⟩ := pow_eq_one_of_mahlerMeasure_eq_one h hz₀ hz

Premises used: Polynomial.pow_eq_one_of_mahlerMeasure_eq_one
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
w : ℕ
left : 0 < w
hz_pow : z ^ w = 1
⊢ w ≠ 0

Tactic:
omega