import Omega.Geometry
import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

namespace Omega
noncomputable section
open Complex InnerProductGeometry
open scoped RealInnerProductSpace

theorem mark_dot (a z w : ℝ) :
    ⟪mark a z,mark a w⟫=a^2*(c^2+z*w) := by
  change ((mark a w)*star (mark a z)).re=_
  simp [mark]
  ring

theorem mark_radius (a z : ℝ) (ha : 0 < a) :
    ‖mark a z‖=a*Real.sqrt (c^2+z^2) := by
  apply (sq_eq_sq₀ (norm_nonneg _) (mul_nonneg ha.le (Real.sqrt_nonneg _))).mp
  rw [← Complex.normSq_eq_norm_sq,Complex.normSq_apply,mark_re,mark_im,mul_pow,
    Real.sq_sqrt (add_nonneg (sq_nonneg c) (sq_nonneg z))]
  ring

theorem mark_angle_cosine (a z w : ℝ) (ha : 0 < a) :
    Real.cos (angle (mark a z) (mark a w))=
      (c^2+z*w)/(Real.sqrt (c^2+z^2)*Real.sqrt (c^2+w^2)) := by
  rw [cos_angle,mark_dot,mark_radius a z ha,mark_radius a w ha]
  have hc := c_pos
  have hz : Real.sqrt (c^2+z^2)≠0 := by positivity
  have hw : Real.sqrt (c^2+w^2)≠0 := by positivity
  field_simp
  <;> ring

theorem seed_angle (a : ℝ) (ha : 0 < a) :
    angle (mark a s) (mark a (-s))=epsilon := by
  apply Real.injOn_cos
    ⟨angle_nonneg _ _,angle_le_pi _ _⟩
    ⟨by unfold epsilon; positivity, by unfold epsilon; linarith [Real.pi_pos]⟩
  rw [mark_angle_cosine a _ _ ha]
  have hcs : c^2+s^2=1 := by linarith [sc_identity]
  simp only [neg_sq,hcs,Real.sqrt_one,one_mul,div_one,mul_neg]
  have ht := Real.cos_two_mul delta
  have he : epsilon=2*delta := by unfold delta; ring
  rw [he]
  dsimp [c,s]
  nlinarith [Real.sin_sq_add_cos_sq delta]

/-- Euclidean triangle area in the canonical orthonormal plane, using half
the absolute determinant. -/
def triangleArea (a z w : ℝ) : ℝ :=
  |(mark a z).re*(mark a w).im-(mark a z).im*(mark a w).re|/2

theorem triangle_area (a z w : ℝ) :
    triangleArea a z w=a^2*c/2*|z-w| := by
  unfold triangleArea
  rw [mark_re,mark_re,mark_im,mark_im]
  have he : a*c*(a*w)-(a*z)*(a*c)=a^2*c*(w-z) := by ring
  rw [he,abs_mul,abs_of_nonneg (mul_nonneg (sq_nonneg a) c_pos.le),abs_sub_comm]
  ring

end
end Omega