awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
right :
  Eq (α := ℝ)
    (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) * HPow.hPow (β := ℕ) y 2 ^ x * y)
    (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
⊢ ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘ fun (x : ℝ) ↦
          HPow.hPow (β := ℕ) x 2)
        y *
      y =
    arctan y

Tactic:
rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]

Premises used: tsum_mul_right, HasSum.tsum_eq, Function.comp_apply, Real.hasSum_arctan
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
right :
  Eq (α := ℝ) (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x * y ^ (2 * x + 1) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1))
    (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
⊢ Eq (α := ℝ)
    (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) * HPow.hPow (β := ℕ) y 2 ^ x * y)
    (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))

Tactic:
simp_rw [mul_assoc, ← pow_mul, ← pow_succ, div_mul_eq_mul_div]

Premises used: pow_succ, mul_assoc, div_mul_eq_mul_div, pow_mul
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
right right₁ right₂ right₃ :
  Eq (α := ℝ) (∑' (x : ℕ), (↑(Int.negSucc 0 ^ x) : ℝ) * y ^ (2 * x + 1) / (↑(2 * x + 1) : ℝ))
    (∑' (b : ℕ), (↑(Int.negSucc 0 ^ b) : ℝ) * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))
⊢ Eq (α := ℝ) (∑' (x : ℕ), HPow.hPow (α := ℝ) (-1) x * y ^ (2 * x + 1) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1))
    (∑' (b : ℕ), HPow.hPow (α := ℝ) (-1) b * y ^ (2 * b + 1) / (↑(2 * b + 1) : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel :
  Tendsto
    (fun (x : ℝ) ↦
      ((fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) ∘
            fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2)
          x *
        x)
    (𝓝[<] 1) (𝓝 l)
⊢ Tendsto arctan (𝓝[<] 1) (𝓝 l)

Tactic:
replace abel : Tendsto arctan (𝓝[<] 1) (𝓝 l) := by
    apply abel.congr'
    rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff]
    use 1, zero_lt_one
    intro y hy1 hy2
    rw [dist_eq, abs_sub_lt_iff] at hy1
    rw [Set.mem_Iio] at hy2
    have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith
    rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]
    simp_rw [mul_assoc, ← pow_mul, ← pow_succ, div_mul_eq_mul_div]
    norm_cast
-- Module: Mathlib.Analysis.Real.Pi.Leibniz
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)
rwa :
  ∀
    (h :
      Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
        (𝓝 (arctan 1)))
    (m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1))
    (q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1))
    (abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)),
    Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
      (𝓝 (π / 4))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (h :
      Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
        (𝓝 (π / 4)))
    (m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1))
    (q : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1))
    (abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)),
    Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
      (𝓝 (π / 4))
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))

Tactic:
rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h

Premises used: Continuous.tendsto, Real.arctan_one, Real.continuous_arctan, Filter.Tendsto.mono_left, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
⊢ W (k + 1) =
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))

Tactic:
prod_range_succ _ _

Premises used: Real.Wallis.W, Finset.prod_range_succ
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
⊢ LT.lt (α := ℝ) 0
    (∏ i ∈ range 0,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)))

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
hk : 0 < W k
succ :
  0 <
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))
⊢ 0 < W (k + 1)

Tactic:
rw [W_succ]

Premises used: Real.Wallis.W_succ
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
hk : 0 < W k
⊢ 0 <
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))

Tactic:
mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_))

Premises used: mul_pos, div_pos
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
hk : 0 < W k
succ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2
succ₁ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
succ₂ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2
succ₃ : 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3
⊢ 0 <
    W k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3)))

Tactic:
refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_))

Premises used: mul_pos, div_pos
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
hk : 0 < W k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
hk : 0 < W k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
hk : 0 < W k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
zero : 0 < W 0
succ : ∀ (k : ℕ) (hk : 0 < W k), 0 < W (k + 1)
⊢ 0 < W k

Tactic:
induction k with
  | zero => unfold W; simp
  | succ k hk =>
    rw [W_succ]
    refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_)) <;> positivity

Premises used: Real.Wallis.W, Real.Wallis.W_succ
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
⊢ 1 =
    1 * HPow.hPow (α := ℝ) (β := ℕ) (↑1 : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑1 : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1))

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
succ :
  HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3))) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))
⊢ ∏ i ∈ range (n + 1),
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))

Tactic:
rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]

Premises used: div_mul_div_comm, Finset.prod_range_succ
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3))) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))

Tactic:
(div_eq_div_iff ?_ ?_).mpr ?_

Premises used: Iff.mpr, div_eq_div_iff
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
succ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)) ≠
    0
succ₁ : HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) ≠ 0
succ₂ :
  HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)))
⊢ HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3))) =
    HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))

Tactic:
refine (div_eq_div_iff ?_ ?_).mpr ?_

Premises used: Iff.mpr, div_eq_div_iff
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ 0 <
    HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3))

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
      ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)) ≠
    0

Tactic:
exact ne_of_gt (by positivity)

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) ≠ 0

Tactic:
exact ne_of_gt (by positivity)

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
succ :
  HPow.hPow (α := ℝ) 2 (4 * n) *
          (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 0 * (↑n ! : ℝ) * (↑n ! : ℝ) * (↑n ! : ℝ) * (↑n ! : ℝ)) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) *
      (HPow.hPow (β := ℕ)
              ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 + 1) * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (↑(2 * n)! : ℝ))) 0 *
            ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 + 1) * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (↑(2 * n)! : ℝ))) *
          ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 + 1) * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (↑(2 * n)! : ℝ))) *
        (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * 2 * 2 * 2 * 2 *
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) 0 *
                (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
              (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
            (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 0 * (↑(2 * n)! : ℝ) * (↑(2 * n)! : ℝ) *
          (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)))
⊢ HPow.hPow (α := ℝ) 2 (4 * n) *
          (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 0 * (↑n ! : ℝ) * (↑n ! : ℝ) * (↑n ! : ℝ) * (↑n ! : ℝ)) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) : ℝ) 0 *
            (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) : ℝ) *
          (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) : ℝ) *
        (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * 2 * 2 * 2 * 2 *
        (HPow.hPow (α := ℝ) (β := ℕ) (↑((n + 1) * n !) : ℝ) 0 * (↑((n + 1) * n !) : ℝ) * (↑((n + 1) * n !) : ℝ) *
            (↑((n + 1) * n !) : ℝ) *
          (↑((n + 1) * n !) : ℝ)) *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 0 * (↑(2 * n)! : ℝ) * (↑(2 * n)! : ℝ) *
          (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)))

Tactic:
push_cast
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
IH :
  ∏ i ∈ range n,
      (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (α := ℝ) 2 (4 * n) *
          (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 0 * (↑n ! : ℝ) * (↑n ! : ℝ) * (↑n ! : ℝ) * (↑n ! : ℝ)) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)) *
      (HPow.hPow (β := ℕ)
              ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 + 1) * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (↑(2 * n)! : ℝ))) 0 *
            ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 + 1) * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (↑(2 * n)! : ℝ))) *
          ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 + 1) * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (↑(2 * n)! : ℝ))) *
        (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * 2 * 2 * 2 * 2 *
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) 0 *
                (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
              (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
            (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ)) *
          (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 0 * (↑(2 * n)! : ℝ) * (↑(2 * n)! : ℝ) *
          (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) *
        ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3)))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
n : ℕ
zero :
  W 0 =
    HPow.hPow (α := ℝ) 2 (HMul.hMul (α := ℕ) 4 0) * HPow.hPow (α := ℝ) (β := ℕ) (↑0! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(HMul.hMul (α := ℕ) 2 0)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1))
succ :
  ∀ (n : ℕ)
    (IH :
      W n =
        HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
          (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))),
    W (n + 1) =
      HPow.hPow (α := ℝ) 2 (4 * (n + 1)) * HPow.hPow (α := ℝ) (β := ℕ) (↑(n + 1)! : ℝ) 4 /
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1))
⊢ W n =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))

Tactic:
induction n with
  | zero =>
    simp only [W, prod_range_zero, Nat.factorial_zero, mul_zero, pow_zero]
    norm_num
  | succ n IH =>
    unfold W at IH ⊢
    rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]
    refine (div_eq_div_iff ?_ ?_).mpr ?_
    any_goals exact ne_of_gt (by positivity)
    simp_rw [Nat.mul_succ, Nat.factorial_succ, pow_succ]
    push_cast
    ring_nf

Premises used: Iff.mpr, Nat.mul_succ, Nat.factorial_succ, div_mul_div_comm, pow_succ, ne_of_gt, div_eq_div_iff, pow_zero, MulZeroClass.mul_zero, Real.Wallis.W, Finset.prod_range_zero, Finset.prod_range_succ, Nat.factorial_zero
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
rw :
  2 / π * W k =
    2 / π *
      ∏ x ∈ range k,
        (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 3) /
          ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2))
⊢ (π / 2)⁻¹ * W k = HDiv.hDiv (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))

Tactic:
rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]

Premises used: inv_div, mul_div_mul_comm, integral_sin_pow_odd, Finset.prod_div_distrib, integral_sin_pow_even
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
simp_rw :
  2 / π * W k =
    2 / π *
      ∏ x ∈ range k,
        (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) *
          ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 3))
⊢ 2 / π * W k =
    2 / π *
      ∏ x ∈ range k,
        (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 3) /
          ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2))

Tactic:
simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]

Premises used: mul_div_assoc, div_div_eq_mul_div, div_div_div_comm
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
⊢ 2 / π * W k =
    2 / π *
      ∏ x ∈ range k,
        (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) *
          ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 3))

Tactic:
rfl
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
rw : (π / 2)⁻¹ * W k ≤ 1
⊢ W k ≤ π / 2

Tactic:
rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]

Premises used: Real.pi_div_two_pos, div_le_one, div_eq_inv_mul
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
rw : LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
⊢ (π / 2)⁻¹ * W k ≤ 1

Tactic:
rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]

Premises used: integral_sin_pow_pos, Real.Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))

Tactic:
apply integral_sin_pow_succ_le

Premises used: integral_sin_pow_succ_le
-- Module: Mathlib.Analysis.Real.Pi.Wallis
Goal:
k : ℕ
rw : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ≤ (π / 2)⁻¹ * W k
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * (π / 2) ≤ W k

Tactic:
rw [← le_div_iff₀ pi_div_two_pos, div_eq_inv_mul (W k) _]

Premises used: Real.pi_div_two_pos, Real.Wallis.W, div_eq_inv_mul, le_div_iff₀