awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
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
⊢ 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))
have succ₁ : HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * (n + 1))! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) ≠ 0
Tactic: refine (div_eq_div_iff ?_ ?_).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
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
⊢ 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))
have 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)))
Tactic: refine (div_eq_div_iff ?_ ?_).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
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 (α := ℝ) (β := ℕ) (↑((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)))
have 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)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
n : ℕ
⊢ W n =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
have 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))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
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))
⊢ W n =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
have 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))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ (π / 2)⁻¹ * W k = HDiv.hDiv (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
have 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))
Tactic: rw [integral_sin_pow_even, integral_sin_pow_odd, mul_div_mul_comm, ← prod_div_distrib, inv_div]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ 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))
have 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))
Tactic: simp_rw [div_div_div_comm, div_div_eq_mul_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ W k ≤ π / 2
have rw : (π / 2)⁻¹ * W k ≤ 1
Tactic: rw [← div_le_one pi_div_two_pos, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ (π / 2)⁻¹ * W k ≤ 1
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
Tactic: rw [W_eq_integral_sin_pow_div_integral_sin_pow, div_le_one (integral_sin_pow_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * (π / 2) ≤ W k
have rw : (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) _]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ≤ (π / 2)⁻¹ * W k
have rw : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
Tactic: rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀ (integral_sin_pow_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
have h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1 + 1)
Tactic: convert! integral_sin_pow_succ_le (2 * k + 1)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
k : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1 + 1)
have h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
  (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 +
    HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Tactic: rw [integral_sin_pow (2 * k)]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
⊢ Tendsto W atTop (𝓝 (π / 2))
have refine : Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
  (𝓝 (π / 2))
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds le_W W_le
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
⊢ 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
have rw : 𝓝 (π / 2) = 𝓝 (1 * (π / 2))
Tactic: rw [sub_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
rw : 𝓝 (π / 2) = 𝓝 (1 * (π / 2))
⊢ 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
have rw₁ : 𝓝 (π / 2) = 𝓝 (π / 2)
Tactic: rw [sub_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (hypothesis)
Goal:
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (π / 2))
have this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
Tactic: have : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2)) := by rw [sub_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (π / 2))
have rw : Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
  (𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) * (π / 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2)))
have refine : Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop
  (𝓝 (HSub.hSub (α := ℝ) 1 0))
Tactic: refine Tendsto.mul ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
n : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
    1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
have rw : (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1) / (HMul.hMul (α := ℝ) 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
n : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
have e_a : HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1 = HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2 - 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (hypothesis)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0))
have h : ∀ (n : ℕ),
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
    1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop
    (𝓝 (HSub.hSub (α := ℝ) 1 0))
have simp_rw : Tendsto (fun (i : ℕ) ↦ 1 - 1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop (𝓝 (HSub.hSub (α := ℝ) 1 0))
Tactic: simp_rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (fun (i : ℕ) ↦ 1 - 1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)) atTop (𝓝 (HSub.hSub (α := ℝ) 1 0))
have refine : Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) atTop atTop
Tactic: refine (tendsto_const_nhds.div_atTop ?_).const_sub _
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Wallis (goal)
Goal:
this : 𝓝 (π / 2) = 𝓝 (HSub.hSub (α := ℝ) 1 0 * (π / 2))
h :
  ∀ (n : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) =
      1 - 1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) atTop atTop
have refine : Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ)) atTop atTop
Tactic: refine Tendsto.atTop_add ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.Real.Spectrum (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have refine_1 : ∀ (h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) (x : ℝ)
  (hx : x ∈ spectrum ℝ a), 0 ≤ x
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Spectrum (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
refine_1 :
  ∀ (h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)) (x : ℝ)
    (hx : x ∈ spectrum ℝ a), 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have refine_2 : ∀ (h : ∀ x ∈ spectrum ℝ a, 0 ≤ x), SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Spectrum (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
a : A
h : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ 0 ≤ x
have refine_1 : ∀ (x : ℝ≥0) (hx : Membership.mem (α := ℝ) (spectrum ℝ a) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)),
  LE.le (α := ℝ) (0 : ℝ) ((algebraMap ℝ≥0 ℝ : (a : ℝ≥0) → ℝ) x : ℝ)
Tactic: obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Spectrum (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
a : A
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x
have rw : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
  ∀ x ∈ σₙ ℝ a, 0 ≤ x
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Spectrum (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
a : A
rw :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ∀ x ∈ σₙ ℝ a, 0 ≤ x
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x
have rw₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
    (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
  ∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Spectrum (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℝ A
inst_2 : IsScalarTower ℝ A A
inst_3 : SMulCommClass ℝ A A
a : A
rw :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ∀ x ∈ σₙ ℝ a, 0 ≤ x
rw₁ :
  SpectrumRestricts (R := ℝ≥0) (S := ℝ) (A := Unitization ℝ A) (↑a : Unitization ℝ A)
      (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x
⊢ QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x
have rw₂ : (∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x) ↔
  ∀ x ∈ spectrum ℝ (A := Unitization ℝ A) (↑a : Unitization ℝ A), 0 ≤ x
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
⊢ f 0 = 0
have rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E) 0 0) = 0
Tactic: rw [← zero_smul 𝕜 (0 : E), smul, norm_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E) 0 0) = 0
⊢ f 0 = 0
have rw₁ : norm.{u_3} (E := 𝕜) 0 * f 0 = 0
Tactic: rw [← zero_smul 𝕜 (0 : E), smul, norm_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E) 0 0) = 0
rw₁ : norm.{u_3} (E := 𝕜) 0 * f 0 = 0
⊢ f 0 = 0
have rw₂ : 0 * f 0 = 0
Tactic: rw [← zero_smul 𝕜 (0 : E), smul, norm_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (β := E) 0 0) = 0
rw₁ : norm.{u_3} (E := 𝕜) 0 * f 0 = 0
rw₂ : 0 * f 0 = 0
⊢ f 0 = 0
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [← zero_smul 𝕜 (0 : E), smul, norm_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
⊢ f (-x) = f x
have rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (-1) x) = f x
Tactic: rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Seminorm (goal)
Goal:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
rw : f (HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜) (-1) x) = f x
⊢ f (-x) = f x
have rw₁ : norm.{u_3} (E := 𝕜) (-1) * f x = f x
Tactic: rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]