n : ℕ
x r : ℝ
⊢ x * x ^ n * ((↑(Nat.factorial n))⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑(Nat.factorial n))⁻¹ * (x * (↑n + 1)⁻¹ * r)
n : ℕ
x r : ℝ
⊢ expNear (n + 1) x r = expNear n x (1 + x / (↑n + 1) * r)
simp [expNear, range_succ, mul_add, add_left_comm, add_assoc, pow_succ, div_eq_mul_inv,
    mul_inv]
no goals
n : ℕ
x r : ℝ
⊢ x * x ^ n * ((↑(Nat.factorial n))⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑(Nat.factorial n))⁻¹ * (x * (↑n + 1)⁻¹ * r)
ac_rfl