awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • cosPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤
    n + 2
have refine_1 : (cosPoly (n + 1)).natDegree ≤ n + 2
Tactic: refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
refine_1 : (cosPoly (n + 1)).natDegree ≤ n + 2
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • cosPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤
    n + 2
have refine_2 : ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * cosPoly n).natDegree ≤ n + 2
Tactic: refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
⊢ 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))
have 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))
Tactic: rw [recursion]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
⊢ 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 θ)
have 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 θ)
Tactic: simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) =
    (↑(n + 2)! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)
have calc : I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 * θ ^ (2 * n + 3)
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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
calc : I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 * θ ^ (2 * n + 3)
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) =
    (↑(n + 2)! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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))
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) =
    (↑(n + 2)! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)
have 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 θ)
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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)
have inl : ∃ (z : ℤ), eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)
Tactic: rcases eq_or_ne b 0 with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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 : ℝ)
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)
have inr : ∀ (hb : b ≠ 0),
  ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k = (↑z : ℝ)
Tactic: rcases eq_or_ne b 0 with rfl | hb
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)
have inl : ∀ (hp : p.natDegree ≤ 0),
  ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 0 =
      (↑z : ℝ)
Tactic: rcases k.eq_zero_or_pos with rfl | hk
Cleared hypotheses: k, hp
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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 : ℝ)
⊢ ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)
have inl₁ : ∀ (hk : k > 0),
  ∃ (z : ℤ),
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑0 : ℝ)) p * HPow.hPow (α := ℝ) (↑0 : ℝ) k = (↑z : ℝ)
Tactic: rcases k.eq_zero_or_pos with rfl | hk
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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 : ℝ)
have inr : eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
  (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)
Tactic: refine ⟨∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)
have lhs : eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k
Tactic: lhs
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k
have rw : eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
    (p.sum fun (n : ℕ) (a : ℤ) ↦ (monomial n : (a : ℤ) → ℤ[X]) a) *
  HPow.hPow (α := ℝ) (↑b : ℝ) k
Tactic: rw [← sum_monomial_eq p]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
| eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)
have rw : eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
    (p.sum fun (n : ℕ) (a : ℤ) ↦ (monomial n : (a : ℤ) → ℤ[X]) a) *
  HPow.hPow (α := ℝ) (↑b : ℝ) k
Tactic: lhs; rw [← sum_monomial_eq p]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) p * HPow.hPow (α := ℝ) (↑b : ℝ) k =
    (↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i)) : ℝ)
have 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)) : ℝ)
Tactic: conv => lhs; rw [← sum_monomial_eq p]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ 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)) : ℝ)
have 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)) : ℝ))
Tactic: rw [eval₂_sum, sum, Finset.sum_mul, Int.cast_sum]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ 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)) : ℝ))
have 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))
Tactic: simp only [eval₂_monomial, eq_intCast, div_pow, Int.cast_mul, Int.cast_pow]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
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)
have ik : i ≤ k
Tactic: have ik := (le_natDegree_of_mem_supp i hi).trans hp
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ (↑(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)
have inr : b ^ i ∣ b ^ (k - i) * b ^ 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ 0 < I n (π / 2)
have refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x → 0 ≤ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))
Tactic: refine integral_pos (by simp) (by fun_prop) ?_ ⟨0, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x → 0 ≤ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))
have refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x), 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
Tactic: refine fun x hx => mul_nonneg (pow_nonneg ?_ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x), 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x → 0 ≤ (1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x), 0 ≤ cos (x * (π / 2))
Tactic: refine fun x hx => mul_nonneg (pow_nonneg ?_ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
have refine_1 : -1 ≤ x ∧ x ≤ 1
Tactic: rw [sub_nonneg, sq_le_one_iff_abs_le_one, abs_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ 0 ≤ cos (x * (π / 2))
have refine_2 : -(π / 2) ≤ x * (π / 2)
Tactic: refine cos_nonneg_of_neg_pi_div_two_le_of_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
refine_2 : -(π / 2) ≤ x * (π / 2)
⊢ 0 ≤ cos (x * (π / 2))
have refine_2₁ : x * (π / 2) ≤ π / 2
Tactic: refine cos_nonneg_of_neg_pi_div_two_le_of_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ -(π / 2) ≤ x * (π / 2)
have nlinarith : x * (π / 2) < -(π / 2) → 2 / 2 = 1
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : x * (π / 2) < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ x * (π / 2)
have nlinarith₁ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : x * (π / 2) < -(π / 2) → 2 / 2 = 1
nlinarith₁ nlinarith₂ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₃ : x * (π / 2) < -(π / 2) → 2 / 2 = 1
nlinarith₄ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) ≤ x * (π / 2)
have nlinarith₅ : x * (π / 2) < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : x * (π / 2) < -(π / 2) → 2 / 2 = 1
nlinarith₁ nlinarith₂ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₃ : x * (π / 2) < -(π / 2) → 2 / 2 = 1
nlinarith₄ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : x * (π / 2) < -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) ≤ x * (π / 2)
have nlinarith₆ : x * (π / 2) < -(π / 2) → 1 * x * (1 * π) - -(1 * π) + (0 - (-1 - x) * (0 - π)) = 0
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ x * (π / 2) ≤ π / 2
have nlinarith : π / 2 < x * (π / 2) → 2 / 2 = 1
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : π / 2 < x * (π / 2) → 2 / 2 = 1
⊢ x * (π / 2) ≤ π / 2
have nlinarith₁ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : π / 2 < x * (π / 2) → 2 / 2 = 1
nlinarith₁ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : π / 2 < x * (π / 2) → 2 / 2 = 1
nlinarith₃ nlinarith₄ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ x * (π / 2) ≤ π / 2
have nlinarith₅ : π / 2 < x * (π / 2) → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : π / 2 < x * (π / 2) → 2 / 2 = 1
nlinarith₁ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : π / 2 < x * (π / 2) → 2 / 2 = 1
nlinarith₃ nlinarith₄ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : π / 2 < x * (π / 2) → GT.gt (α := ℝ) 2 0
⊢ x * (π / 2) ≤ π / 2
have nlinarith₆ : π / 2 < x * (π / 2) → 1 * π - 1 * x * (1 * π) + (0 - (x - 1) * (0 - π)) = 0
Tactic: nlinarith [hx.1, hx.2, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ I n (π / 2) ≤ 2
have rw : ‖I n (π / 2)‖ ≤ 2
Tactic: rw [← norm_of_nonneg I_pos.le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ ‖I n (π / 2)‖ ≤ 2
have refine : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (uIoc (-1) 1) x → ‖(1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))‖ ≤ 1
Tactic: refine (norm_integral_le_of_norm_le_const ?_).trans (show (1 : ℝ) * _ ≤ _ by norm_num)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (uIoc (-1) 1) x
⊢ ‖(1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))‖ ≤ 1
have hx₁ : -1 < x ∧ x ≤ 1
Tactic: simp only [uIoc_of_le, neg_le_self_iff, zero_le_one, mem_Ioc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ ‖(1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))‖ ≤ 1
have rw : |1 - HPow.hPow (β := ℕ) x 2| ^ n * |cos (x * (π / 2))| ≤ 1
Tactic: rw [norm_eq_abs, abs_mul, abs_pow]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - HPow.hPow (β := ℕ) x 2| ^ n * |cos (x * (π / 2))| ≤ 1
have refine : |1 - HPow.hPow (β := ℕ) x 2| ≤ 1
Tactic: refine mul_le_one₀ (pow_le_one₀ (abs_nonneg _) ?_) (abs_nonneg _) (abs_cos_le_one _)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - HPow.hPow (β := ℕ) x 2| ≤ 1
have rw : -1 ≤ 1 - HPow.hPow (β := ℕ) x 2 ∧ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
Tactic: rw [abs_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - HPow.hPow (β := ℕ) x 2 ∧ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
have left : -1 ≤ 1 - HPow.hPow (β := ℕ) x 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
left : -1 ≤ 1 - HPow.hPow (β := ℕ) x 2
⊢ -1 ≤ 1 - HPow.hPow (β := ℕ) x 2 ∧ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
have right : 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - HPow.hPow (β := ℕ) x 2
have nlinarith : 1 - HPow.hPow (β := ℕ) x 2 < -1 → -1 + (1 - HPow.hPow (β := ℕ) x 2 - -1) + (0 - (-1 - x) * (x - 1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
have nlinarith : 1 < 1 - HPow.hPow (β := ℕ) x 2 → 0 - HPow.hPow (β := ℕ) x 2 + (1 - (1 - HPow.hPow (β := ℕ) x 2)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
a : ℝ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds 0)
have rw : Tendsto (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds (a * 0))
Tactic: rw [← mul_zero a]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
a : ℝ
⊢ Tendsto (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds (a * 0))
have refine : ∀ (x : ℕ), a * (HPow.hPow (β := ℕ) a 2 ^ x / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
Tactic: refine ((FloorSemiring.tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
a : ℝ
x : ℕ
⊢ a * (HPow.hPow (β := ℕ) a 2 ^ x / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
have rw : a * (a ^ (2 * x) / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
Tactic: rw [← pow_mul, mul_div_assoc', _root_.pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
a : ℝ
x : ℕ
rw : a * (a ^ (2 * x) / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
⊢ a * (HPow.hPow (β := ℕ) a 2 ^ x / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
have rw₁ : a * a ^ (2 * x) / (↑x ! : ℝ) = a ^ (2 * x + 1) / (↑x ! : ℝ)
Tactic: rw [← pow_mul, mul_div_assoc', _root_.pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
a : ℝ
x : ℕ
rw : a * (a ^ (2 * x) / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
rw₁ : a * a ^ (2 * x) / (↑x ! : ℝ) = a ^ (2 * x + 1) / (↑x ! : ℝ)
⊢ a * (HPow.hPow (β := ℕ) a 2 ^ x / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
have rw₂ : a * a ^ (2 * x) / (↑x ! : ℝ) = a * a ^ (2 * x) / (↑x ! : ℝ)
Tactic: rw [← pow_mul, mul_div_assoc', _root_.pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
x : ℝ
⊢ ¬Irrational x → ∃ (a : ℤ) (b : ℕ), 0 < b ∧ x = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
have rw : (∃ (y : ℚ), (↑y : ℝ) = x) → ∃ (a : ℤ) (b : ℕ), 0 < b ∧ x = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
Tactic: rw [Irrational, not_not, mem_range]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
⊢ Irrational π
have apply : Irrational (π / (↑2 : ℝ))
Tactic: apply Irrational.of_div_natCast 2