-- actually it's analytical trigonometry
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.LibrarySearch

axiom sin : Real → Real 
axiom csc : Real → Real 

axiom sin_eq_reciprocal_of_csc : ∀x, sin x = 1 / (csc x)
axiom csc_eq_reciprocal_of_sin : ∀x, csc x = 1 / (sin x)

axiom cos : Real → Real 
axiom sec : Real → Real 

axiom cos_eq_reciprocal_of_sec : ∀x, cos x = (sec x)⁻¹ 
axiom sec_eq_reciprocal_of_cos : ∀x, sec x = (cos x)⁻¹

@[simp]
noncomputable def tan (x : Real) : Real := sin x / cos x
theorem tan_def : ∀x, tan x = sin x / cos x := by simp
@[simp]
noncomputable def cot (x : Real) : Real := cos x / sin x

theorem tan_eq_sin_div_cos : ∀x, tan x = sin x / cos x := by simp
theorem cot_eq_cos_div_sin : ∀x, cot x = cos x / sin x := by simp

theorem tan_eq_reciprocal_of_cot : ∀x, tan x = 1 / (cot x) := by simp
theorem cot_eq_reciprocal_of_tan : ∀x, cot x = 1 / (tan x) := by simp

noncomputable def sin2 (x : Real) : Real := sin x * sin x
noncomputable def cos2 (x : Real) : Real := cos x * cos x
noncomputable def tan2 (x : Real) : Real := tan x * tan x
theorem tan2_def : ∀x, tan2 x = sin2 x / cos2 x := by 
  intro x
  simp [tan2, sin2, cos2]
  exact div_mul_div_comm (sin x) (cos x) (sin x) (cos x)

noncomputable def csc2 (x : Real) : Real := csc x * csc x
noncomputable def sec2 (x : Real) : Real := sec x * sec x
theorem sec2_eq_reciprocal_of_cos2 : ∀x, sec2 x = (cos2 x)⁻¹ := by 
  intro x
  rw [sec2, cos2]
  simp
  rw [sec_eq_reciprocal_of_cos]

noncomputable def cot2 (x : Real) : Real := cot x * cot x

noncomputable def sin3 (x : Real) : Real := sin2 x * sin x
noncomputable def cos3 (x : Real) : Real := cos2 x * cos x
noncomputable def tan3 (x : Real) : Real := tan2 x * tan x

noncomputable def csc3 (x : Real) : Real := csc2 x * csc x
noncomputable def sec3 (x : Real) : Real := sec2 x * sec x
noncomputable def cot3 (x : Real) : Real := cot2 x * cot x

@[simp]
axiom pyth_id : ∀x, sin2 x + cos2 x = 1

theorem sin_squared_eq {x : Real} : sin2 x = 1 - cos2 x := by 
  rw [← add_left_inj (cos2 x)]
  rw [sub_add_cancel]
  exact pyth_id x

theorem cos_squared_eq {x : Real} : cos2 x = 1 - sin2 x := by 
  rw [← add_left_inj (sin2 x)]
  rw [sub_add_cancel]
  rw [add_comm]
  exact pyth_id x

theorem bleh {a b c : Real} (d : Real) : a + b = c → a / d + b / d = c / d := by
  intro h
  rw [← add_div, h]

def tan_pyth_id : ∀x, cos2 x ≠ 0 → tan2 x + 1 = sec2 x := by 
  intro x
  intro hnz
  have h := pyth_id x
  have h : sin2 x / cos2 x + cos2 x / cos2 x = 1 / cos2 x :=
    bleh (cos2 x) h

  rw [← tan2_def] at h
  simp at h
  rw [← sec2_eq_reciprocal_of_cos2, div_self] at h
  exact h
  exact hnz

example (x : Real) : 2 * (1 / (csc x)) = 2 * (sin x) := by
  rw [sin_eq_reciprocal_of_csc]

--todo evens and odds and the sin/cos (a ± b) ones