-- Mathlib/Data/Real/Pi/Wallis.lean
theorem tendsto_W_nhds_pi_div_two : Tendsto W atTop (𝓝 <| π / 2)

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 1 - 1 / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Tactic:
refine (tendsto_const_nhds.div_atTop ?_).const_sub _

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i + 2) atTop atTop

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i + 2) atTop atTop

Tactic:
refine Tendsto.atTop_add ?_ tendsto_const_nhds

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i) atTop atTop

Proof state:
case e_a
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1

Tactic:
ring

Result:
no goals

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))

Tactic:
rw [this]

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 2 * ↑i) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop two_pos

Result:
no goals

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (2 * ↑n + 2 - 1) / (2 * ↑n + 2)

Tactic:
congr 1

Result:
case e_a
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Tactic:
simp_rw [h]

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => 1 - 1 / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Proof state:
⊢ 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))

Tactic:
rw [sub_zero, one_mul]

Result:
no goals

Proof state:
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))

Tactic:
have : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2)) := by rw [sub_zero, one_mul]

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)

Tactic:
rw [sub_div' (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg
  (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)), one_mul]

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (2 * ↑n + 2 - 1) / (2 * ↑n + 2)

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 ((1 - 0) * (π / 2)))

Tactic:
refine Tendsto.mul ?_ tendsto_const_nhds

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Proof state:
⊢ Tendsto W atTop (𝓝 (π / 2))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds le_W W_le

Result:
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2) * (π / 2)) atTop (𝓝 (π / 2))

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Tactic:
have h : ∀ n : ℕ, ((2 : ℝ) * n + 1) / (2 * n + 2) = 1 - 1 / (2 * n + 2) := by
  intro n
  rw [sub_div' (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg
    (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)), one_mul]
  congr 1; ring

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
h : ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)
⊢ Tendsto (fun i => (2 * ↑i + 1) / (2 * ↑i + 2)) atTop (𝓝 (1 - 0))

Proof state:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
⊢ ∀ (n : ℕ), (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)

Tactic:
intro n

Result:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = 1 - 1 / (2 * ↑n + 2)