Theorem: centralBinom_ratio (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom (n + 1)) / ↑(centralBinom n) = 4 * ((↑n + 1 / 2) / (↑n + 1))
Tactic:
rw [mul_div_assoc', mul_add, eq_div_iff, ← cast_add_one, div_mul_eq_mul_div, mul_comm, ← cast_mul,
  succ_mul_centralBinom_succ, cast_mul, mul_div_cancel]
State after:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * (2 * n + 1)) = 4 * ↑n + 4 * (1 / 2)

case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom n) ≠ 0

α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑n + 1 ≠ 0

State before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑n + 1 ≠ 0
Tactic:
exact Nat.cast_add_one_ne_zero _
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * (2 * n + 1)) = 4 * ↑n + 4 * (1 / 2)
Tactic:
rw [mul_add_one, ← mul_assoc, cast_add, cast_mul]
State after:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * 2) * ↑n + ↑2 = 4 * ↑n + 4 * (1 / 2)

State before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(2 * 2) * ↑n + ↑2 = 4 * ↑n + 4 * (1 / 2)
Tactic:
norm_num1
State after:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ 4 * ↑n + 2 = 4 * ↑n + 2

State before:
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ 4 * ↑n + 2 = 4 * ↑n + 2
Tactic:
rfl
State after:
no goals

State before:
case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ ↑(centralBinom n) ≠ 0
Tactic:
rw [Nat.cast_ne_zero]
State after:
case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ centralBinom n ≠ 0

State before:
case h
α : Type u_1
inst✝¹ : Field α
inst✝ : CharZero α
n : ℕ
⊢ centralBinom n ≠ 0
Tactic:
exact centralBinom_ne_zero _
State after:
no goals