awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
push_cast :
  -(HMul.hMul (α := ℝ) 2 2 * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (HPow.hPow (α := ℝ) 0 (n + 1) * cos θ))) +
        2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * I (n + 1) θ -
      4 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ
⊢ -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * (HPow.hPow (α := ℝ) 0 (n + 1) * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * (↑(n + 1) : ℝ) * I (n + 1 - 1) θ =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ

Tactic:
push_cast
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
⊢ -(HMul.hMul (α := ℝ) 2 2 * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (HPow.hPow (α := ℝ) 0 (n + 1) * cos θ))) +
        2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * I (n + 1) θ -
      4 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
rw :
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (HPow.hPow (α := ℝ) (β := ℕ) 0 0 * cos θ))) * θ +
        2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1) * (2 * sin θ) -
      4 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (↑0 : ℝ) * I (HSub.hSub (α := ℕ) 0 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ
⊢ I 1 θ * HPow.hPow (β := ℕ) θ 3 = 4 * sin θ - 4 * θ * cos θ

Tactic:
rw [_root_.pow_succ, ← mul_assoc, recursion' 0, sub_mul, add_mul, mul_assoc _ (I 0 θ), I_zero]

Premises used: add_mul, _private.0.recursion', pow_succ, mul_assoc, sub_mul, _private.0.I, _private.0.I_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
⊢ -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (HPow.hPow (α := ℝ) (β := ℕ) 0 0 * cos θ))) * θ +
        2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1) * (2 * sin θ) -
      4 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (↑0 : ℝ) * I (HSub.hSub (α := ℕ) 0 1) θ * θ =
    4 * sin θ - 4 * θ * cos θ

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
⊢ (sinPoly 0).natDegree ≤ 0

Tactic:
simp [sinPoly]

Premises used: _private.0.sinPoly
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
⊢ (sinPoly 1).natDegree ≤ 1

Tactic:
simp only [natDegree_C, zero_le', sinPoly]

Premises used: Polynomial.natDegree_C, zero_le', _private.0.sinPoly
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • sinPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤
    n + 2

Tactic:
natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Premises used: Polynomial.natDegree_add_le_of_degree_le, Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
refine_1 : (sinPoly (n + 1)).natDegree ≤ n + 2
refine_2 : ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤ n + 2
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • sinPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤
    n + 2

Tactic:
refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Premises used: Polynomial.natDegree_add_le_of_degree_le, Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ n + 1 ≤ n + 2

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ (sinPoly (n + 1)).natDegree ≤ n + 2

Tactic:
exact (sinPoly_natDegree_le (n + 1)).trans (by simp)

Premises used: HAdd.hAdd, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
natDegree_mul_le.trans ?_

Premises used: Polynomial.natDegree_mul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
refine_2 : natDegree (R := ℤ) ((monomial 2 : (a : ℤ) → ℤ[X]) (-4)) + (sinPoly n).natDegree ≤ n + 2
⊢ ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_mul_le.trans ?_

Premises used: Polynomial.natDegree_mul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ natDegree (R := ℤ) ((monomial 2 : (a : ℤ) → ℤ[X]) (-4)) + (sinPoly n).natDegree ≤ n + 2

Tactic:
simpa [add_comm 2] using sinPoly_natDegree_le n

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
⊢ (cosPoly 0).natDegree ≤ 0

Tactic:
simp [cosPoly]

Premises used: _private.0.cosPoly
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
⊢ LE.le (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • cosPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤
    n + 2

Tactic:
natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Premises used: Polynomial.natDegree_add_le_of_degree_le, Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
refine_1 : (cosPoly (n + 1)).natDegree ≤ n + 2
refine_2 : ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤ n + 2
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • cosPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤
    n + 2

Tactic:
refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Premises used: Polynomial.natDegree_add_le_of_degree_le, Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ (cosPoly (n + 1)).natDegree ≤ n + 2

Tactic:
exact (cosPoly_natDegree_le (n + 1)).trans (by simp)

Premises used: HAdd.hAdd, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ natDegree (R := ℤ) ((monomial 2 : (a : ℤ) → ℤ[X]) (-4)) + (cosPoly n).natDegree ≤ n + 2

Tactic:
simp [add_comm 2, cosPoly_natDegree_le n]

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤ n + 2

Tactic:
exact natDegree_mul_le.trans (by simp [add_comm 2, cosPoly_natDegree_le n])

Premises used: Polynomial.natDegree_mul_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
⊢ I 0 θ * θ ^ (HMul.hMul (α := ℕ) 2 0 + 1) =
    (↑0! : ℝ) * (eval₂ (Int.castRingHom ℝ) θ (sinPoly 0) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly 0) * cos θ)

Tactic:
simp [sinPoly, cosPoly, I_zero]

Premises used: _private.0.I_zero, _private.0.cosPoly, _private.0.sinPoly
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
⊢ I 1 θ * θ ^ (HMul.hMul (α := ℕ) 2 1 + 1) =
    (↑1! : ℝ) * (eval₂ (Int.castRingHom ℝ) θ (sinPoly 1) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly 1) * cos θ)

Tactic:
simp [I_one, sinPoly, cosPoly, sub_eq_add_neg]

Premises used: sub_eq_add_neg, _private.0.I_one, _private.0.cosPoly, _private.0.sinPoly
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 * θ ^ (2 * n + 3)

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
rw :
  (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
        4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ) *
      θ ^ (2 * n + 3) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        (I n θ * θ ^ (2 * n + 1))
⊢ I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 * θ ^ (2 * n + 3) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        (I n θ * θ ^ (2 * n + 1))

Tactic:
rw [recursion]

Premises used: _private.0.recursion
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
⊢ (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
        4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ) *
      θ ^ (2 * n + 3) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        (I n θ * θ ^ (2 * n + 1))

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
simp :
  2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) *
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ) *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        ((↑n ! : ℝ) *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
      ((2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * HPow.hPow (β := ℕ) θ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * HPow.hPow (β := ℕ) θ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)
⊢ 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        (I n θ * θ ^ (2 * n + 1)) =
    (↑(n + 2)! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)

Tactic:
simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]

Premises used: Nat.factorial_succ, _private.0.cosPoly, _private.0.sinPoly
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
⊢ 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) *
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ) *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        ((↑n ! : ℝ) *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
      ((2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * HPow.hPow (β := ℕ) θ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * HPow.hPow (β := ℕ) θ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
calc : I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 * θ ^ (2 * n + 3)
calc₁ :
  I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 * θ ^ (2 * n + 3) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        (I n θ * θ ^ (2 * n + 1))
calc₂ :
  2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * HPow.hPow (β := ℕ) θ 2 *
        (I n θ * θ ^ (2 * n + 1)) =
    (↑(n + 2)! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) =
    (↑(n + 2)! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)

Tactic:
calc I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3) := by ring
        _ = 2 * (n + 2) * (2 * n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
            4 * (n + 2) * (n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1)) := by rw [recursion]; ring
        _ = _ := by simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]; ring

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, _private.0.I, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
inl :
  ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)
inr :
  ∀ (hb : b ≠ 0),
    ∃ (z : ℤ),
      eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
inl :
  ∀ (hp : p.natDegree ≤ 0),
    ∃ (z : ℤ),
      eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 0 =
        (↑z : ℝ)
inl₁ :
  ∀ (hk : k > 0),
    ∃ (z : ℤ),
      eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 0 =
    (↑(p.coeff 0) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 0 =
      (↑z : ℝ)

Tactic:
exact ⟨p.coeff 0, by simp⟩
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑0 : ℝ)

Tactic:
simp [hk.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)

Tactic:
exact ⟨0, by simp [hk.ne']⟩
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)

Tactic:
⟨∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i), ?_⟩

Premises used: HMul.hMul, HSub.hSub, Polynomial.coeff, HPow.hPow, Exists.intro, Polynomial.support, Finset.sum
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
inr :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)

Tactic:
refine ⟨∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i), ?_⟩
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
lhs : eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k
| eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)

Tactic:
lhs
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
rw :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
      (p.sum fun (n : ℕ) (a : ℤ) ↦ (monomial n : (a : ℤ) → ℤ[X]) a) *
    HPow.hPow (α := ℝ) (↑b : ℝ) k
| eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k

Tactic:
rw [← sum_monomial_eq p]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
rw :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
      (p.sum fun (n : ℕ) (a : ℤ) ↦ (monomial n : (a : ℤ) → ℤ[X]) a) *
    HPow.hPow (α := ℝ) (↑b : ℝ) k
| eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)

Tactic:
lhs; rw [← sum_monomial_eq p]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
inr :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
        (p.sum fun (n : ℕ) (a : ℤ) ↦ (monomial n : (a : ℤ) → ℤ[X]) a) *
      HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)
⊢ eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)

Tactic:
conv => lhs; rw [← sum_monomial_eq p]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
inr :
  Eq (α := ℝ)
    (∑ i ∈ p.support,
      eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ((monomial i : (a : ℤ) → ℤ[X]) (p.coeff i)) *
        HPow.hPow (α := ℝ) (↑b : ℝ) k)
    (∑ x ∈ p.support, (↑(p.coeff x * a ^ x * b ^ (k - x)) : ℝ))
⊢ eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
        (p.sum fun (n : ℕ) (a : ℤ) ↦ (monomial n : (a : ℤ) → ℤ[X]) a) *
      HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)

Tactic:
rw [eval₂_sum, sum, Finset.sum_mul, Int.cast_sum]

Premises used: Polynomial.sum, Polynomial.eval₂_sum, Int.cast_sum, Finset.sum_mul
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
inr :
  Eq (α := ℝ)
    (∑ x ∈ p.support,
      (↑(p.coeff x) : ℝ) * (HPow.hPow (α := ℝ) (↑a : ℝ) x / HPow.hPow (α := ℝ) (↑b : ℝ) x) *
        HPow.hPow (α := ℝ) (↑b : ℝ) k)
    (∑ x ∈ p.support, (↑(p.coeff x) : ℝ) * HPow.hPow (α := ℝ) (↑a : ℝ) x * HPow.hPow (α := ℝ) (↑b : ℝ) (k - x))
⊢ Eq (α := ℝ)
    (∑ i ∈ p.support,
      eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ((monomial i : (a : ℤ) → ℤ[X]) (p.coeff i)) *
        HPow.hPow (α := ℝ) (↑b : ℝ) k)
    (∑ x ∈ p.support, (↑(p.coeff x * a ^ x * b ^ (k - x)) : ℝ))

Tactic:
simp only [eval₂_monomial, eq_intCast, div_pow, Int.cast_mul, Int.cast_pow]

Premises used: Polynomial.eval₂_monomial, Int.cast_pow, eq_intCast, Int.cast_mul, div_pow
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ Eq (α := ℝ)
    (∑ x ∈ p.support,
      (↑(p.coeff x) : ℝ) * (HPow.hPow (α := ℝ) (↑a : ℝ) x / HPow.hPow (α := ℝ) (↑b : ℝ) x) *
        HPow.hPow (α := ℝ) (↑b : ℝ) k)
    (∑ x ∈ p.support, (↑(p.coeff x) : ℝ) * HPow.hPow (α := ℝ) (↑a : ℝ) x * HPow.hPow (α := ℝ) (↑b : ℝ) (k - x))

Tactic:
Finset.sum_congr rfl (fun i hi => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
inr :
  ∀ (i : ℕ) (hi : i ∈ p.support),
    (↑(p.coeff i) : ℝ) * (HPow.hPow (α := ℝ) (↑a : ℝ) i / HPow.hPow (α := ℝ) (↑b : ℝ) i) *
        HPow.hPow (α := ℝ) (↑b : ℝ) k =
      (↑(p.coeff i) : ℝ) * HPow.hPow (α := ℝ) (↑a : ℝ) i * HPow.hPow (α := ℝ) (↑b : ℝ) (k - i)
⊢ Eq (α := ℝ)
    (∑ x ∈ p.support,
      (↑(p.coeff x) : ℝ) * (HPow.hPow (α := ℝ) (↑a : ℝ) x / HPow.hPow (α := ℝ) (↑b : ℝ) x) *
        HPow.hPow (α := ℝ) (↑b : ℝ) k)
    (∑ x ∈ p.support, (↑(p.coeff x) : ℝ) * HPow.hPow (α := ℝ) (↑a : ℝ) x * HPow.hPow (α := ℝ) (↑b : ℝ) (k - x))

Tactic:
refine Finset.sum_congr rfl (fun i hi => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
⊢ i ≤ k

Tactic:
have ik := (le_natDegree_of_mem_supp i hi).trans hp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
inr : b ^ i ∣ b ^ (k - i) * b ^ i
⊢ (↑(p.coeff i) : ℝ) * (HPow.hPow (α := ℝ) (↑a : ℝ) i / HPow.hPow (α := ℝ) (↑b : ℝ) i) * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(p.coeff i) : ℝ) * HPow.hPow (α := ℝ) (↑a : ℝ) i * HPow.hPow (α := ℝ) (↑b : ℝ) (k - i)

Tactic:
rw [mul_assoc, div_mul_comm, ← Int.cast_pow, ← Int.cast_pow, ← Int.cast_pow,
    ← pow_sub_mul_pow b ik, ← Int.cast_div_charZero, Int.mul_ediv_cancel _ (pow_ne_zero _ hb),
    ← mul_assoc, mul_right_comm, ← Int.cast_pow]

Premises used: mul_assoc, Int.cast_pow, Int.mul_ediv_cancel, pow_ne_zero, pow_sub_mul_pow, mul_right_comm, div_mul_comm, Int.cast_div_charZero
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Tactic:
dvd_mul_left _ _

Premises used: dvd_mul_left
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Tactic:
exact dvd_mul_left _ _

Premises used: dvd_mul_left
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ LT.lt (α := ℝ) (-1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))) (Icc (-1) 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) 0 ∧ 0 < (1 - HPow.hPow (α := ℝ) (β := ℕ) 0 2) ^ n * cos (0 * (π / 2))

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
refine :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x → 0 ≤ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))
⊢ 0 < I n (π / 2)

Tactic:
refine integral_pos (by simp) (by fun_prop) ?_ ⟨0, by simp⟩

Premises used: Exists.intro, intervalIntegral.integral_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x → 0 ≤ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))

Tactic:
fun x hx => mul_nonneg (pow_nonneg ?_ _) ?_

Premises used: mul_nonneg, pow_nonneg
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x), 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x), 0 ≤ cos (x * (π / 2))
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x → 0 ≤ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))

Tactic:
refine fun x hx => mul_nonneg (pow_nonneg ?_ _) ?_

Premises used: mul_nonneg, pow_nonneg