awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
refine_1 :
  ∀ (p : (↑(boxPoly n B₁ B₂) : Type)),
    Membership.mem (α := Fin (n + 1) → ℤ)
      (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ))
      ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X]) : Fin (n + 1) → ℤ)
refine_2 :
  ∀
    (p :
      (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) :
        Type)),
    Membership.mem (α := ℤ[X]) (boxPoly n B₁ B₂)
      ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ) : ℤ[X])
⊢ (boxPoly n B₁ B₂).ncard =
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard
have refine_3 : Function.LeftInverse
  (fun
      (p :
        (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) :
          Type)) ↦
    Subtype.mk (p := fun (x : ℤ[X]) ↦ x ∈ boxPoly n B₁ B₂)
      ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) sorry)
  fun (p : (↑(boxPoly n B₁ B₂) : Type)) ↦
  Subtype.mk (p := fun (x : Fin (n + 1) → ℤ) ↦
    x ∈ (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)))
    ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X])) sorry
Tactic: refine Set.ncard_congr' ⟨fun p ↦ ⟨toFn (n + 1) p, ?_⟩, fun p ↦ ⟨ofFn (n + 1) p, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
refine_1 :
  ∀ (p : (↑(boxPoly n B₁ B₂) : Type)),
    Membership.mem (α := Fin (n + 1) → ℤ)
      (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ))
      ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X]) : Fin (n + 1) → ℤ)
refine_2 :
  ∀
    (p :
      (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) :
        Type)),
    Membership.mem (α := ℤ[X]) (boxPoly n B₁ B₂)
      ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ) : ℤ[X])
refine_3 :
  Function.LeftInverse
    (fun
        (p :
          (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) :
            Type)) ↦
      Subtype.mk (p := fun (x : ℤ[X]) ↦ x ∈ boxPoly n B₁ B₂)
        ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) ⋯)
    fun (p : (↑(boxPoly n B₁ B₂) : Type)) ↦
    Subtype.mk (p := fun (x : Fin (n + 1) → ℤ) ↦
      x ∈ (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)))
      ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X])) ⋯
⊢ (boxPoly n B₁ B₂).ncard =
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard
have refine_4 : Function.RightInverse
  (fun
      (p :
        (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) :
          Type)) ↦
    Subtype.mk (p := fun (x : ℤ[X]) ↦ x ∈ boxPoly n B₁ B₂)
      ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) sorry)
  fun (p : (↑(boxPoly n B₁ B₂) : Type)) ↦
  Subtype.mk (p := fun (x : Fin (n + 1) → ℤ) ↦
    x ∈ (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)))
    ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X])) sorry
Tactic: refine Set.ncard_congr' ⟨fun p ↦ ⟨toFn (n + 1) p, ?_⟩, fun p ↦ ⟨ofFn (n + 1) p, ?_⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : (↑(boxPoly n B₁ B₂) : Type)
⊢ Membership.mem (α := Fin (n + 1) → ℤ)
    (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ))
    ((toFn (n + 1) : (a : ℤ[X]) → Fin (n + 1) → ℤ) (↑p : ℤ[X]) : Fin (n + 1) → ℤ)
have prop : ∀ (i : Fin (n + 1)), B₁ i ≤ (↑((↑p : ℤ[X]).coeff (↑i : ℕ)) : ℝ) ∧ (↑((↑p : ℤ[X]).coeff (↑i : ℕ)) : ℝ) ≤ B₂ i
Tactic: have prop := p.property.2
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) : Type)
⊢ Membership.mem (α := ℤ[X]) (boxPoly n B₁ B₂)
    ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ) : ℤ[X])
have refine_2 : ∀ (i : Fin (n + 1)),
  B₁ i ≤ (↑(coeff ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) (↑i : ℕ)) : ℝ) ∧
    (↑(coeff ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) (↑i : ℕ)) : ℝ) ≤ B₂ i
Tactic: refine ⟨Nat.le_of_lt_succ <| ofFn_natDegree_lt (Nat.le_add_left 1 n) p.val, fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) : Type)
i : Fin (n + 1)
⊢ B₁ i ≤ (↑(coeff ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) (↑i : ℕ)) : ℝ) ∧
    (↑(coeff ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) (↑i : ℕ)) : ℝ) ≤ B₂ i
have prop : (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) ≤ (↑p : Fin (n + 1) → ℤ) ∧ (↑p : Fin (n + 1) → ℤ) ≤ fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋
Tactic: have prop := Finset.mem_Icc.mp p.property
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : (↑(↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)) : Type)
i : Fin (n + 1)
prop :
  (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) ≤ (↑p : Fin (n + 1) → ℤ) ∧ (↑p : Fin (n + 1) → ℤ) ≤ fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋
⊢ B₁ i ≤ (↑(coeff ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) (↑i : ℕ)) : ℝ) ∧
    (↑(coeff ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ)) (↑i : ℕ)) : ℝ) ≤ B₂ i
have refine_2 : B₁ i ≤ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), sorry⟩) : ℝ) ∧ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), sorry⟩) : ℝ) ≤ B₂ i
Tactic: rw [ofFn_coeff_eq_val_of_lt _ i.2]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (↑(Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) : Set (Fin (n + 1) → ℤ)).ncard =
    ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
have norm_cast : Finset.card (α := Fin (n + 1) → ℤ) (Finset.Icc (fun (x : Fin (n + 1)) ↦ ⌈B₁ x⌉) fun (x : Fin (n + 1)) ↦ ⌊B₂ x⌋) =
  ∏ x : Fin (n + 1), (⌊B₂ x⌋ - ⌈B₁ x⌉ + 1).toNat
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
⊢ 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)
have simp_rw : Set.ncard (α := ℤ[X])
    {p : ℤ[X] |
      p.natDegree ≤ n ∧
        ∀ (i : Fin (n + 1)),
          -((↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)) ≤ (↑(p.coeff (↑i : ℕ)) : ℝ) ∧
            (↑(p.coeff (↑i : ℕ)) : ℝ) ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} =
  ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)
Tactic: simp_rw [norm_eq_abs, abs_le]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
⊢ Set.ncard (α := ℤ[X])
      {p : ℤ[X] |
        p.natDegree ≤ n ∧
          ∀ (i : Fin (n + 1)),
            -((↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)) ≤ (↑(p.coeff (↑i : ℕ)) : ℝ) ∧
              (↑(p.coeff (↑i : ℕ)) : ℝ) ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} =
    ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)
have rw : Eq (α := ℕ)
  (∏ i : Fin (n + 1), (⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ - ⌈-((↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ))⌉ + 1).toNat)
  (∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1))
Tactic: rw [← boxPoly, ncard_boxPoly]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
⊢ Eq (α := ℕ)
    (∏ i : Fin (n + 1),
      (⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ - ⌈-((↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ))⌉ + 1).toNat)
    (∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1))
have simp : Eq (α := ℕ) (∏ x : Fin (n + 1), (2 * ⌊(↑(n.choose (↑x : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat)
  (∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1))
Tactic: simp only [ceil_neg, sub_neg_eq_add, ← two_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
⊢ Eq (α := ℕ) (∏ x : Fin (n + 1), (2 * ⌊(↑(n.choose (↑x : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat)
    (∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1))
have apply : ∀ (i : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
    (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat = 2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1
Tactic: apply Finset.prod_congr rfl fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat = 2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1
have zify : (↑(2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat : ℤ) =
  HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ (↑(2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1
have rw : HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋₊ : ℤ) + 1 =
  HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1
Tactic: rw [toNat_of_nonneg (by positivity), ← natCast_floor_eq_floor (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋₊ : ℤ) + 1 =
    HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1
have norm_cast : 2 * ⌊(↑((↑(n.choose (↑i : ℕ)) : ℝ≥0) * B) : ℝ)⌋₊ + 1 = 2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
n : ℕ
B : ℝ≥0
⊢ 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 : ℝ)} ≤
      ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)
have 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)
Tactic: have h_card :
      Set.ncard {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ i : Fin (n + 1), ‖p.coeff i‖ ≤ n.choose i * B} =
      ∏ i : Fin (n + 1), (2 * ⌊n.choose i * B⌋₊ + 1) := by
    simp_rw [norm_eq_abs, abs_le]
    rw [← boxPoly, ncard_boxPoly]
    simp only [ceil_neg, sub_neg_eq_add, ← two_mul]
    apply Finset.prod_congr rfl fun i _ ↦ ?_
    zify
    rw [toNat_of_nonneg (by positivity), ← natCast_floor_eq_floor (by positivity)]
    norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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)
⊢ 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 : ℝ)} ≤
      ∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1)
have rw : 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: rw [← h_card]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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)
⊢ 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 : ℝ)}
have a : ∀ (p : ℤ[X]) (hp : p.natDegree ≤ n),
  (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ) →
    ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)
Tactic: gcongr with p hp
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ ‖p.coeff (↑d : ℕ)‖ ≤ (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
have a : ‖(map (castRingHom ℂ) p).coeff (↑d : ℕ)‖ ≤ (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
Tactic: rw [show ‖p.coeff d‖ = ‖(p.map (castRingHom ℂ)).coeff d‖ by aesop]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ ‖(map (castRingHom ℂ) p).coeff (↑d : ℕ)‖ ≤ (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
have a : (↑((map (castRingHom ℂ) p).natDegree.choose (↑d : ℕ)) : ℝ) * (map (castRingHom ℂ) p).mahlerMeasure ≤
  (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
Tactic: apply le_trans <| (p.map (castRingHom ℂ)).norm_coeff_le_choose_mul_mahlerMeasure d
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ (↑((map (castRingHom ℂ) p).natDegree.choose (↑d : ℕ)) : ℝ) * (map (castRingHom ℂ) p).mahlerMeasure ≤
    (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
have a : 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
a : 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure
⊢ (↑((map (castRingHom ℂ) p).natDegree.choose (↑d : ℕ)) : ℝ) * (map (castRingHom ℂ) p).mahlerMeasure ≤
    (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
have a₁ : (map (castRingHom ℂ) p).natDegree ≤ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
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)
⊢ 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 : ℝ)}
have 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 : ℝ)}
Tactic: have h_subset :
      {p : ℤ[X] | p.natDegree ≤ n ∧ (p.map (Int.castRingHom ℂ)).mahlerMeasure ≤ B} ⊆
      {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ i : Fin (n + 1), ‖p.coeff i‖ ≤ n.choose i * B} := by
    gcongr with p hp
    intro hB d
    rw [show ‖p.coeff d‖ = ‖(p.map (castRingHom ℂ)).coeff d‖ by aesop]
    apply le_trans <| (p.map (castRingHom ℂ)).norm_coeff_le_choose_mul_mahlerMeasure d
    gcongr
    · exact mahlerMeasure_nonneg _
    · grind [Polynomial.natDegree_map_le]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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 : ℝ)}
⊢ Set.Finite (α := ℤ[X])
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}
have hs : Set.ncard (α := ℤ[X])
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} ≠
  0
Tactic: apply Set.finite_of_ncard_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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 : ℝ)}
⊢ Set.ncard (α := ℤ[X])
      {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} ≠
    0
have hs : ∀ (a : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ a → 2 * ⌊(↑(n.choose (↑a : ℕ)) : ℝ≥0) * B⌋₊ + 1 ≠ 0
Tactic: rw [h_card, Finset.prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
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 : ℝ)}
⊢ 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 : ℝ)}
have h_finite : Set.Finite (α := ℤ[X])
  {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}
Tactic: have h_finite : {p : ℤ[X]| p.natDegree ≤ n ∧
      ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.Finite := by
    apply Set.finite_of_ncard_ne_zero
    rw [h_card, Finset.prod_ne_zero_iff]
    grind
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
have inl : ∀ (hn : n = 0), (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
have inr : ∀ (hn : n ≠ 0), (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
have this : NeZero n
Tactic: have : NeZero n := ⟨hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
have inr : Eq (α := ℝ) (∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ Eq (α := ℝ) (∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖) 1
have inr : ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1
Tactic: suffices ∀ x ∈ primitiveRoots n ℂ, ‖x‖ ≤ 1 from Multiset.prod_eq_one (by simpa)
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
have inl : p = 0 → ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
Tactic: rcases eq_or_ne p 0 with _ | hp
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
inl : p = 0 → ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
have inr : ∀ (hp : p ≠ 0), ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
Tactic: rcases eq_or_ne p 0 with _ | hp
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
have h_ineq : ‖(map (castRingHom ℂ) p).leadingCoeff‖ ≤ 1
Tactic: have h_ineq := h ▸ (leadingCoeff_le_mahlerMeasure <| p.map (castRingHom ℂ))
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : ‖(map (castRingHom ℂ) p).leadingCoeff‖ ≤ 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
have inr : ∀ (h_ineq : norm (E := ℂ) (↑p.leadingCoeff : ℂ) ≤ 1), norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1
Tactic: rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast] at ⊢ h_ineq
Cleared hypotheses: h_ineq
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : norm (E := ℂ) (↑p.leadingCoeff : ℂ) ≤ 1
⊢ norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1
have inr : ∀ (h_ineq : |p.leadingCoeff| ≤ 1), |p.leadingCoeff| = 1
Tactic: norm_cast at ⊢ h_ineq
Cleared hypotheses: h_ineq
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
⊢ |p.leadingCoeff| = 1
have this : ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
Tactic: have := norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one h