Limit_of_Sine_X_over_X_v2
Provedlim_{x→0} sin(x)/x = 1.
Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.Tactic
Formal statement
theorem Limit_of_Sine_X_over_X_v2 : Filter.Tendsto (fun x => Real.sin x / x) (nhdsWithin 0 {0}ᶜ) (nhds 1) := by sorry