sin_deg_thirtytheoremProved here from basic factspropext, Classical.choice, Quot.sound
sin_deg_thirtyLean 4Proved here from basic factsFormally verified
/-- `sin 30° = 1/2`. First `30° = π/6` radians (arithmetic), then Mathlib's exact value`Real.sin_pi_div_six`. Note that `sin 30`, *without* the conversion, is the sine of 30 radians,about `-0.988`. -/theorem sin_deg_thirty : sin (deg 30) = 1 / 2 := by have h : deg 30 = π / 6 := by unfold deg; ring rw [h, sin_pi_div_six]
addition_formulastheoremProved here from basic factspropext, Classical.choice, Quot.sound
addition_formulasLean 4Proved here from basic factsFormally verified
/-- **The addition formulas**`sin (α + β) = sin α cos β + cos α sin β` and `cos (α + β) = cos α cos β − sin α sin β`.This is the lesson's rotation proof in the language of complex numbers: multiplying by`e^{iθ} = cos θ + i sin θ` rotates the plane by `θ`, and rotating by `β` and then by `α` isrotating by `α + β`: `e^{i(α+β)} = e^{iα} e^{iβ}` (Mathlib's `Complex.exp_add`). Expanding theproduct and comparing imaginary and real parts gives the two formulas. -/theorem addition_formulas (α β : ℝ) : sin (α + β) = sin α * cos β + cos α * sin β ∧ cos (α + β) = cos α * cos β - sin α * sin β := by have key : Complex.exp (((α + β : ℝ) : ℂ) * Complex.I) = Complex.exp ((α : ℂ) * Complex.I) * Complex.exp ((β : ℂ) * Complex.I) := by rw [← Complex.exp_add] congr 1 push_cast ring rw [Complex.exp_mul_I, Complex.exp_mul_I, Complex.exp_mul_I, ← Complex.ofReal_cos, ← Complex.ofReal_sin, ← Complex.ofReal_cos, ← Complex.ofReal_sin, ← Complex.ofReal_cos, ← Complex.ofReal_sin] at key have him := congrArg Complex.im key have hre := congrArg Complex.re key simp only [Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im] at him hre constructor <;> linarith
sin_add_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
sin_add_libraryLean 4Applies a library theoremFormally verified
/-- The sine addition formula, straight from Mathlib (`Real.sin_add`). Compare`addition_formulas`, which derives it from the exponential rule. -/theorem sin_add_library (α β : ℝ) : sin (α + β) = sin α * cos β + cos α * sin β := Real.sin_add α β
sin_add_ne_addtheoremProved here from basic factspropext, Classical.choice, Quot.sound
sin_add_ne_addLean 4Proved here from basic factsFormally verified
/-- **Sine does not distribute over addition.** "`sin (α + β) = sin α + sin β` for all `α, β`"is false: with `α = β = π/2` the left side is `sin π = 0` and the right side is `1 + 1 = 2`. -/theorem sin_add_ne_add : ¬ ∀ α β : ℝ, sin (α + β) = sin α + sin β := by intro h have h1 := h (π / 2) (π / 2) rw [add_halves, sin_pi, sin_pi_div_two] at h1 norm_num at h1
sin_right_triangletheoremApplies a library theorempropext, Classical.choice, Quot.sound
sin_right_triangleLean 4Applies a library theoremFormally verified
/-- **The power-series sine agrees with "opposite over hypotenuse".** In a right triangle withthe right angle at `B`, the sine of the angle at `C`, times the hypotenuse `AC`, is the side`AB` opposite that angle. Applies Mathlib's`EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two`. -/theorem sin_right_triangle {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {A B C : P} (h : ∠ A B C = π / 2) : sin (∠ B C A) * dist A C = dist A B := EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two h
law_of_cosines_coordtheoremProved here from basic factspropext, Classical.choice, Quot.sound
law_of_cosines_coordLean 4Proved here from basic factsFormally verified
/-- **The law of cosines, the coordinate computation.** Put the vertex `C` of the triangle atthe origin and `B = (a, 0)` on the positive x-axis. By the unit-circle definition of sine andcosine, the vertex `A` at distance `b` from `C` and at angle `γ` is `A = (b cos γ, b sin γ)`.By the distance formula, `c² = AB² = (b cos γ − a)² + (b sin γ)²`, and this simplifies to`a² + b² − 2ab cos γ` using `sin² γ + cos² γ = 1`. -/theorem law_of_cosines_coord (a b γ : ℝ) : (b * cos γ - a) ^ 2 + (b * sin γ) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b * cos γ := by have h := Real.sin_sq_add_cos_sq γ calc (b * cos γ - a) ^ 2 + (b * sin γ) ^ 2 = b ^ 2 * (sin γ ^ 2 + cos γ ^ 2) + a ^ 2 - 2 * a * b * cos γ := by ring _ = a ^ 2 + b ^ 2 - 2 * a * b * cos γ := by rw [h]; ring
law_costheoremApplies a library theorempropext, Classical.choice, Quot.sound
law_cosLean 4Applies a library theoremFormally verified
/-- **The law of cosines** for any three points of a Euclidean space (a plane, or space):`AC² = AB² + CB² − 2 · AB · CB · cos ∠ABC`. Applies Mathlib's `EuclideanGeometry.law_cos`,which is proved with vectors and the inner product. -/theorem law_cos {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (A B C : P) : dist A C * dist A C = dist A B * dist A B + dist C B * dist C B - 2 * dist A B * dist C B * cos (∠ A B C) := EuclideanGeometry.law_cos A B C
law_sintheoremApplies a library theorempropext, Classical.choice, Quot.sound
law_sinLean 4Applies a library theoremFormally verified
/-- **The law of sines** in the form `sin ∠ABC · BC = sin ∠CAB · CA`, that is,`CA / sin B = BC / sin A` when the sines are non-zero. Applies Mathlib's`EuclideanGeometry.law_sin`. -/theorem law_sin {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (A B C : P) : sin (∠ A B C) * dist B C = sin (∠ C A B) * dist C A := EuclideanGeometry.law_sin A B C
/-- The coordinate computation behind the law of cosines. With `C` at the origin, `B = (a, 0)`and `A = (b cos γ, b sin γ)`, the squared distance `AB²` is `a² + b² − 2ab cos γ`.Hint: rewrite the left side as `b² (sin² γ + cos² γ) + a² − 2ab cos γ` with `ring`, then use`Real.sin_sq_add_cos_sq`. -/theorem law_of_cosines_coord (a b γ : ℝ) : (b * cos γ - a) ^ 2 + (b * sin γ) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b * cos γ := by sorry
Show the compiled solution
law_of_cosines_coordLean 4Proved here from basic factsFormally verified
/-- **The law of cosines, the coordinate computation.** Put the vertex `C` of the triangle atthe origin and `B = (a, 0)` on the positive x-axis. By the unit-circle definition of sine andcosine, the vertex `A` at distance `b` from `C` and at angle `γ` is `A = (b cos γ, b sin γ)`.By the distance formula, `c² = AB² = (b cos γ − a)² + (b sin γ)²`, and this simplifies to`a² + b² − 2ab cos γ` using `sin² γ + cos² γ = 1`. -/theorem law_of_cosines_coord (a b γ : ℝ) : (b * cos γ - a) ^ 2 + (b * sin γ) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b * cos γ := by have h := Real.sin_sq_add_cos_sq γ calc (b * cos γ - a) ^ 2 + (b * sin γ) ^ 2 = b ^ 2 * (sin γ ^ 2 + cos γ ^ 2) + a ^ 2 - 2 * a * b * cos γ := by ring _ = a ^ 2 + b ^ 2 - 2 * a * b * cos γ := by rw [h]; ring
/-- Show that `sin (α + β) = sin α + sin β` is not an identity.Hint: try `α = β = π / 2`, and use `add_halves`, `sin_pi` and `sin_pi_div_two`. -/theorem sin_add_ne_add : ¬ ∀ α β : ℝ, sin (α + β) = sin α + sin β := by sorry
Show the compiled solution
sin_add_ne_addLean 4Proved here from basic factsFormally verified
/-- **Sine does not distribute over addition.** "`sin (α + β) = sin α + sin β` for all `α, β`"is false: with `α = β = π/2` the left side is `sin π = 0` and the right side is `1 + 1 = 2`. -/theorem sin_add_ne_add : ¬ ∀ α β : ℝ, sin (α + β) = sin α + sin β := by intro h have h1 := h (π / 2) (π / 2) rw [add_halves, sin_pi, sin_pi_div_two] at h1 norm_num at h1