awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MahlerMeasure
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])) ⋯
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) → ℤ)) ⋯)
    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

Tactic:
refine Set.ncard_congr' ⟨fun p ↦ ⟨toFn (n + 1) p, ?_⟩, fun p ↦ ⟨ofFn (n + 1) p, ?_⟩, ?_, ?_⟩

Premises used: Equiv.mk, Polynomial.toFn, Subtype.mk, HAdd.hAdd, Set.ncard_congr', OfNat.ofNat, DFunLike.coe, Polynomial.ofFn
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : (↑(boxPoly n B₁ B₂) : Type)
⊢ ∀ (i : Fin (n + 1)), B₁ i ≤ (↑((↑p : ℤ[X]).coeff (↑i : ℕ)) : ℝ) ∧ (↑((↑p : ℤ[X]).coeff (↑i : ℕ)) : ℝ) ≤ B₂ i

Tactic:
have prop := p.property.2
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : (↑(boxPoly n B₁ B₂) : Type)
prop : ∀ (i : Fin (n + 1)), B₁ i ≤ (↑((↑p : ℤ[X]).coeff (↑i : ℕ)) : ℝ) ∧ (↑((↑p : ℤ[X]).coeff (↑i : ℕ)) : ℝ) ≤ B₂ i
⊢ 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) → ℤ)

Tactic:
simpa using ⟨fun i ↦ ceil_le.mpr (prop i).1, fun i ↦ le_floor.mpr (prop i).2⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
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])

Tactic:
⟨Nat.le_of_lt_succ <| ofFn_natDegree_lt (Nat.le_add_left 1 n) p.val, fun i ↦ ?_⟩

Premises used: Set.Mem, setOf, Nat.le_add_left, Nat.le_of_lt_succ, And.intro, OfNat.ofNat, Subtype.val, Polynomial.ofFn_natDegree_lt, Polynomial.boxPoly
-- Module: Mathlib.NumberTheory.MahlerMeasure
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)
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
⊢ Membership.mem (α := ℤ[X]) (boxPoly n B₁ B₂)
    ((ofFn (n + 1) : (a : Fin (n + 1) → ℤ) → ℤ[X]) (↑p : Fin (n + 1) → ℤ) : ℤ[X])

Tactic:
refine ⟨Nat.le_of_lt_succ <| ofFn_natDegree_lt (Nat.le_add_left 1 n) p.val, fun i ↦ ?_⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
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)
⊢ (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
-- Module: Mathlib.NumberTheory.MahlerMeasure
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⌋
refine_2 : B₁ i ≤ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), ⋯⟩) : ℝ) ∧ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), ⋯⟩) : ℝ) ≤ B₂ i
⊢ 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:
rw [ofFn_coeff_eq_val_of_lt _ i.2]

Premises used: Fin.isLt, Polynomial.ofFn_coeff_eq_val_of_lt
-- Module: Mathlib.NumberTheory.MahlerMeasure
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 ≤ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), ⋯⟩) : ℝ) ∧ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), ⋯⟩) : ℝ) ≤ B₂ i

Tactic:
⟨ceil_le.mp (prop.1 i), le_floor.mp (prop.2 i)⟩

Premises used: Int.ceil_le, And.right, And.left, And.intro, Int.le_floor, Iff.mp
-- Module: Mathlib.NumberTheory.MahlerMeasure
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 ≤ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), ⋯⟩) : ℝ) ∧ (↑((↑p : Fin (n + 1) → ℤ) ⟨(↑i : ℕ), ⋯⟩) : ℝ) ≤ B₂ i

Tactic:
exact ⟨ceil_le.mp (prop.1 i), le_floor.mp (prop.2 i)⟩
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ 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])) ⋯

Tactic:
grind [boxPoly, ofFn_comp_toFn_eq_id_of_natDegree_lt]

Premises used: Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt, Polynomial.boxPoly
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ 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) → ℤ)) ⋯)
    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])) ⋯

Tactic:
grind [toFn_comp_ofFn_eq_id]

Premises used: Polynomial.toFn_comp_ofFn_eq_id
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
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
⊢ (↑(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

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ 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:
grind [Pi.card_Icc, card_Icc]

Premises used: Pi.card_Icc, Int.card_Icc
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
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)
⊢ 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:
simp_rw [norm_eq_abs, abs_le]

Premises used: abs_le, Int.norm_eq_abs
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
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))
⊢ 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:
rw [← boxPoly, ncard_boxPoly]

Premises used: Polynomial.ncard_boxPoly, Polynomial.boxPoly
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
simp :
  Eq (α := ℕ) (∏ x : Fin (n + 1), (2 * ⌊(↑(n.choose (↑x : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat)
    (∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1))
⊢ 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:
simp only [ceil_neg, sub_neg_eq_add, ← two_mul]

Premises used: Int.ceil_neg, two_mul, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
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
⊢ Eq (α := ℕ) (∏ x : Fin (n + 1), (2 * ⌊(↑(n.choose (↑x : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat)
    (∏ i : Fin (n + 1), (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1))

Tactic:
apply Finset.prod_congr rfl fun i _ ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
zify :
  (↑(2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1
⊢ (2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat = 2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1

Tactic:
zify
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ 0 ≤ 2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ 0 ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
rw :
  HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋₊ : ℤ) + 1 =
    HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1
⊢ (↑(2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋ + 1).toNat : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1

Tactic:
rw [toNat_of_nonneg (by positivity), ← natCast_floor_eq_floor (by positivity)]

Premises used: Int.toNat_of_nonneg, Int.natCast_floor_eq_floor
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
n : ℕ
B : ℝ≥0
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  2 * ⌊(↑((↑(n.choose (↑i : ℕ)) : ℝ≥0) * B) : ℝ)⌋₊ + 1 = 2 * ⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ + 1
⊢ HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)⌋₊ : ℤ) + 1 =
    HMul.hMul (α := ℤ) 2 (↑⌊(↑(n.choose (↑i : ℕ)) : ℝ≥0) * B⌋₊ : ℤ) + 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.MahlerMeasure
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)

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
-- 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)
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 : ℝ)}
⊢ 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)

Tactic:
rw [← h_card]
-- 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)
a :
  ∀ (p : ℤ[X]) (hp : p.natDegree ≤ n),
    (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ) →
      ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)
⊢ 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:
gcongr with p hp
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ ‖p.coeff (↑d : ℕ)‖ = ‖(map (castRingHom ℂ) p).coeff (↑d : ℕ)‖

Tactic:
aesop
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
a : ‖(map (castRingHom ℂ) p).coeff (↑d : ℕ)‖ ≤ (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
⊢ ‖p.coeff (↑d : ℕ)‖ ≤ (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)

Tactic:
rw [show ‖p.coeff d‖ = ‖(p.map (castRingHom ℂ)).coeff d‖ by aesop]
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
a :
  (↑((map (castRingHom ℂ) p).natDegree.choose (↑d : ℕ)) : ℝ) * (map (castRingHom ℂ) p).mahlerMeasure ≤
    (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)
⊢ ‖(map (castRingHom ℂ) p).coeff (↑d : ℕ)‖ ≤ (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)

Tactic:
apply le_trans <| (p.map (castRingHom ℂ)).norm_coeff_le_choose_mul_mahlerMeasure d

Premises used: Fin.val, Int.castRingHom, Polynomial.map, Complex, Polynomial.norm_coeff_le_choose_mul_mahlerMeasure, le_trans
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
a : 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure
a₁ : (map (castRingHom ℂ) p).natDegree ≤ n
⊢ (↑((map (castRingHom ℂ) p).natDegree.choose (↑d : ℕ)) : ℝ) * (map (castRingHom ℂ) p).mahlerMeasure ≤
    (↑(n.choose (↑d : ℕ)) : ℝ) * (↑B : ℝ)

Tactic:
gcongr
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure

Tactic:
mahlerMeasure_nonneg _

Premises used: Polynomial.mahlerMeasure_nonneg
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ 0 ≤ (map (castRingHom ℂ) p).mahlerMeasure

Tactic:
exact mahlerMeasure_nonneg _

Premises used: Polynomial.mahlerMeasure_nonneg
-- 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)
p : ℤ[X]
hp : p.natDegree ≤ n
hB : (map (castRingHom ℂ) p).mahlerMeasure ≤ (↑B : ℝ)
d : Fin (n + 1)
⊢ (map (castRingHom ℂ) p).natDegree ≤ n

Tactic:
grind [Polynomial.natDegree_map_le]

Premises used: Polynomial.natDegree_map_le
-- 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)
⊢ 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]
-- 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 : ℝ)}
hs :
  Set.ncard (α := ℤ[X])
      {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} ≠
    0
⊢ Set.Finite (α := ℤ[X])
    {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)}

Tactic:
apply Set.finite_of_ncard_ne_zero

Premises used: Set.finite_of_ncard_ne_zero
-- 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 : ℝ)}
hs :
  ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ a → 2 * ⌊(↑(n.choose (↑a : ℕ)) : ℝ≥0) * B⌋₊ + 1 ≠ 0
⊢ Set.ncard (α := ℤ[X])
      {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff (↑i : ℕ)‖ ≤ (↑(n.choose (↑i : ℕ)) : ℝ) * (↑B : ℝ)} ≠
    0

Tactic:
rw [h_card, Finset.prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff
-- 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 : ℝ)}
⊢ ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ a → 2 * ⌊(↑(n.choose (↑a : ℕ)) : ℝ≥0) * B⌋₊ + 1 ≠ 0

Tactic:
grind
-- 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 : ℝ)}
⊢ 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