Complete the part of Position/Angle

EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean

@@ -16,8 +16,6 @@ In this file, we define suitable coversion function between `ℝ⧸2π`,`ℝ⧸
 
 noncomputable section
 
-attribute [ext] Complex.ext
-
 namespace EuclidGeom
 
 open AngValue Classical Real
@@ -1208,24 +1206,6 @@ end AngDValue
 
 
 
-lemma _root_.Real.div_nat_le_self_of_nonnneg {a : ℝ} (n : ℕ) (h : 0 ≤ a) : a / n ≤ a := by
-  show a * (↑n)⁻¹ ≤ a
-  refine' mul_le_of_le_one_right h _
-  by_cases h : n = 0
-  · simp only [h, CharP.cast_eq_zero, inv_zero, zero_le_one]
-  exact inv_le_one (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h))
-
-lemma _root_.Real.div_nat_le_self_of_pos {a : ℝ} (n : ℕ) (h : 0 < a) : a / n ≤ a :=
-  a.div_nat_le_self_of_nonnneg n (le_of_lt h)
-
-lemma _root_.Real.div_nat_lt_self_of_pos_of_two_le {a : ℝ} {n : ℕ} (h : 0 < a) (hn : 2 ≤ n) : a / n < a :=
-  mul_lt_of_lt_one_right h (inv_lt_one (Nat.one_lt_cast.mpr hn))
-
-lemma _root_.Real.pi_div_nat_nonneg (n : ℕ) : 0 ≤ π / n :=
-  div_nonneg (le_of_lt pi_pos) (Nat.cast_nonneg n)
-
-
-
 namespace AngValue
 
 section abs

EuclideanGeometry/Foundation/Axiom/Basic/Angle/AddToMathlib.lean

@@ -958,3 +958,29 @@ end contruction
 end AddTorsor
 
 end Mathlib.Algebra.AddTorsor
+
+
+
+/-!
+### More theorems about real numbers divided by nature numbers
+-/
+
+section Mathlib.Data.Real.Basic
+
+theorem Real.div_nat_le_self_of_nonnneg {a : ℝ} (n : ℕ) (h : 0 ≤ a) : a / n ≤ a := by
+  show a * (↑n)⁻¹ ≤ a
+  refine' mul_le_of_le_one_right h _
+  by_cases h : n = 0
+  · simp only [h, CharP.cast_eq_zero, inv_zero, zero_le_one]
+  · exact inv_le_one (Nat.one_le_cast.mpr (Nat.one_le_iff_ne_zero.mpr h))
+
+theorem Real.div_nat_le_self_of_pos {a : ℝ} (n : ℕ) (h : 0 < a) : a / n ≤ a :=
+  a.div_nat_le_self_of_nonnneg n (le_of_lt h)
+
+theorem Real.div_nat_lt_self_of_pos_of_two_le {a : ℝ} {n : ℕ} (h : 0 < a) (hn : 2 ≤ n) : a / n < a :=
+  mul_lt_of_lt_one_right h (inv_lt_one (Nat.one_lt_cast.mpr hn))
+
+theorem pi_div_nat_nonneg (n : ℕ) : 0 ≤ π / n :=
+  div_nonneg (le_of_lt pi_pos) (Nat.cast_nonneg n)
+
+end Mathlib.Data.Real.Basic

EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean

@@ -60,6 +60,9 @@ theorem neg_vec_norm_eq (A B : P) : ‖- VEC A B‖ = ‖VEC A B‖ := by
 theorem vec_norm_eq_rev (A B : P) : ‖VEC A B‖ = ‖VEC B A‖ := by
   rw [← neg_vec, neg_vec_norm_eq]
 
+theorem vec_norm_eq_dist (A B : P) : ‖VEC A B‖ = dist A B :=
+  (vec_norm_eq_rev A B).trans (NormedAddTorsor.dist_eq_norm' A B).symm
+
 theorem eq_iff_vec_eq_zero {A B : P} : B = A ↔ VEC A B = 0 := vsub_eq_zero_iff_eq.symm
 
 theorem ne_iff_vec_ne_zero {A B : P} : B ≠ A ↔ VEC A B ≠ 0 := eq_iff_vec_eq_zero.not
@@ -118,7 +121,7 @@ def delabVecNDMkPtPt : Delab := do
 lemma VecND.coe_mkPtPt (A B : P) [_h : Fact (B ≠ A)] : VEC_nd A B = VEC A B := rfl
 
 @[simp low]
-theorem VecND.neg_vecND (A B : P) [_h : Fact (B ≠ A)] : (- VEC_nd A B)= VEC_nd B A _h.1.symm := by
+theorem VecND.neg_vecND (A B : P) [_h : Fact (B ≠ A)] : - VEC_nd A B = VEC_nd B A _h.1.symm := by
   haveI : Fact (A ≠ B) := ⟨_h.1.symm⟩
   ext
   simp only [ne_eq, RayVector.coe_neg, coe_mkPtPt, neg_vec]

EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean

@@ -172,22 +172,22 @@ end Perpendicular_inner_product
 
 section vec
 
-variable {A B : P} {l : DirLine P}
+variable (A B : P) {l : DirLine P}
 -- Feel free to change the order of the following theorems for ease of proof.
 
 lemma inner_vec_pt_pt_vec_pt_perp_foot_eq_inner_vec_pt_perp_foot (ha : A LiesOn l) : @inner ℝ _ _ (VEC A B) (VEC A (perp_foot B l)) = inner (VEC A (perp_foot B l)) (VEC A (perp_foot B l)) := sorry
 
 lemma inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_pt_perp_foot (ha : A LiesOn l) : @inner ℝ _ _ (VEC A B) l.toDir.unitVec = inner (VEC A (perp_foot B l)) l.toDir.unitVec := sorry
 
 theorem inner_eq_ddist_pt_perp_foot (ha : A LiesOn l) : inner (VEC A B) l.toDir.unitVec = l.ddist ha (perp_foot_lies_on_line B l) :=
-  inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_pt_perp_foot ha
+  inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_pt_perp_foot A B ha
 
 theorem perp_foot_eq_inner_smul_toDir_unitVec_vadd (ha : A LiesOn l) : perp_foot B l = (@inner ℝ _ _ (VEC A B) l.toDir.unitVec) • l.toDir.unitVec +ᵥ A := by
-  rw [inner_eq_ddist_pt_perp_foot ha]
+  rw [inner_eq_ddist_pt_perp_foot A B ha]
   exact l.pt_eq_ddist_smul_toDir_unitVec_vadd ha (perp_foot_lies_on_line B l)
 
-theorem vec_eq_ddist_smul_toDir_unitVec (ha : A LiesOn l) : VEC A (perp_foot B l) = (@inner ℝ _ _ (VEC A B) l.toDir.unitVec) • l.toDir.unitVec := by
-  rw [inner_eq_ddist_pt_perp_foot ha]
+theorem vec_pt_perp_foot_eq_ddist_smul_toDir_unitVec (ha : A LiesOn l) : VEC A (perp_foot B l) = (@inner ℝ _ _ (VEC A B) l.toDir.unitVec) • l.toDir.unitVec := by
+  rw [inner_eq_ddist_pt_perp_foot A B ha]
   exact l.vec_eq_ddist_smul_toDir_unitVec ha (perp_foot_lies_on_line B l)
 
 theorem inner_vec_pt_pt_vec_pt_perp_foot_eq_dist_sq (ha : A LiesOn l) : inner (VEC A B) (VEC A (perp_foot B l)) = dist A (perp_foot B l) ^ 2 := sorry
@@ -197,7 +197,15 @@ lemma inner_vec_pt_pt_vec_perp_foot_perp_foot_eq_inner_vec_perp_foot_perp_foot :
 lemma inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_perp_foot_perp_foot : @inner ℝ _ _ (VEC A B) l.toDir.unitVec = inner (VEC (perp_foot A l) (perp_foot B l)) l.toDir.unitVec := sorry
 
 theorem inner_eq_ddist_perp_foot_perp_foot : inner (VEC A B) l.toDir.unitVec = l.ddist (perp_foot_lies_on_line A l) (perp_foot_lies_on_line B l) :=
-  inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_perp_foot_perp_foot
+  inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_perp_foot_perp_foot A B
+
+theorem perp_foot_eq_inner_smul_toDir_unitVec_vadd_perp_foot : perp_foot B l = (@inner ℝ _ _ (VEC A B) l.toDir.unitVec) • l.toDir.unitVec +ᵥ perp_foot A l := by
+  rw [inner_eq_ddist_perp_foot_perp_foot]
+  exact l.pt_eq_ddist_smul_toDir_unitVec_vadd (perp_foot_lies_on_line A l) (perp_foot_lies_on_line B l)
+
+theorem vec_perp_foot_perp_foot_eq_ddist_smul_toDir_unitVec : VEC (perp_foot A l) (perp_foot B l) = (@inner ℝ _ _ (VEC A B) l.toDir.unitVec) • l.toDir.unitVec := by
+  rw [inner_eq_ddist_perp_foot_perp_foot]
+  exact l.vec_eq_ddist_smul_toDir_unitVec (perp_foot_lies_on_line A l) (perp_foot_lies_on_line B l)
 
 theorem inner_vec_pt_pt_vec_perp_foot_perp_foot_eq_dist_sq : inner (VEC A B) (VEC (perp_foot A l) (perp_foot B l)) = dist (perp_foot A l) (perp_foot B l) ^ 2 := sorry
 

EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean

@@ -795,6 +795,10 @@ theorem SegND.source_pt_toDir_eq_toDir_of_lies_int {seg_nd : SegND P} {A : P} (h
     exact lies_int_toRay_of_lies_int h
   exact Ray.pt_pt_eq_ray this
 
+theorem Ray.lies_int_iff_pos_of_vec_eq_smul_toDir {ray : Ray P} {A : P} {t : ℝ} (h : VEC ray.source A = t • ray.toDir.unitVec) : A LiesInt ray ↔ 0 < t := sorry
+
+theorem Ray.eq_source_iff_eq_zero_of_vec_eq_smul_toDir {ray : Ray P} {A : P} {t : ℝ} (h : VEC ray.source A = t • ray.toDir.unitVec) : A = ray.source ↔ t = 0 := sorry
+
 end lieson_compatibility
 
 
@@ -959,7 +963,7 @@ theorem pt_lies_on_ray_rev_iff_vec_opposite_dir {A : P} {ray : Ray P} : A LiesOn
     simp [hu, h]
 
 /-- A point $A$ lies on the lines determined by a ray $ray$ (i.e. lies on the ray or its reverse) if and only if the vector from the source of ray to $A$ is a real multiple of the direction vector of $ray$. -/
-theorem pt_lies_on_line_from_ray_iff_vec_parallel {A : P} {ray : Ray P} : (A LiesOn ray ∨ A LiesOn ray.reverse) ↔ ∃t : ℝ, VEC ray.source A = t • ray.toDir.unitVec := by
+theorem pt_lies_on_line_from_ray_iff_vec_parallel {A : P} {ray : Ray P} : (A LiesOn ray ∨ A LiesOn ray.reverse) ↔ ∃ t : ℝ, VEC ray.source A = t • ray.toDir.unitVec := by
   constructor
   · rintro (⟨t, _, ha⟩ | ⟨t, _, ha⟩)
     · use t
@@ -1172,6 +1176,8 @@ theorem SegND.toDir_eq_neg_toDir_of_lies_int {A : P} {seg_nd : SegND P} (h : A L
   exact neg_inj.mpr <|
     (source_pt_toDir_eq_toDir_of_lies_int h).trans (pt_target_toDir_eq_toDir_of_lies_int h).symm
 
+theorem Ray.lies_int_rev_iff_neg_of_vec_eq_smul_toDir {ray : Ray P} {A : P} {t : ℝ} (h : VEC ray.source A = t • ray.toDir.unitVec) : A LiesInt ray.reverse ↔ t < 0 := sorry
+
 end reverse
 
 section extension
@@ -1220,58 +1226,37 @@ theorem eq_target_iff_lies_on_lies_on_extn {A : P} {seg_nd : SegND P} : (A LiesO
 theorem target_lies_int_seg_source_pt_of_pt_lies_int_extn {X : P} {seg_nd : SegND P}
 (liesint : X LiesInt seg_nd.extension) : seg_nd.target LiesInt SEG seg_nd.source X  := by
   rcases liesint with ⟨⟨a, anonneg, ha⟩, nonsource⟩
-  have raysourcesegtarget:seg_nd.1.target = seg_nd.extension.1 := by
-    rfl
-  have sourcetargetA : VEC seg_nd.1.source seg_nd.1.target + VEC seg_nd.1.target X =
-  VEC seg_nd.1.source X := by
+  have raysourcesegtarget :seg_nd.1.target = seg_nd.extension.1 := rfl
+  have sourcetargetA : VEC seg_nd.1.source seg_nd.1.target + VEC seg_nd.1.target X = VEC seg_nd.1.source X := by
     rw [vec_add_vec]
-  have vec_ndtoVec : VEC seg_nd.1.source seg_nd.1.target = seg_nd.toVecND.1 := by
-    rfl
-  have apos:0 < a := by
-    contrapose! nonsource
-    have : a = 0 := by
-      linarith
-    rw [this] at ha
-    simp only [smul_neg, zero_smul, neg_zero] at ha
-    apply eq_iff_vec_eq_zero.mpr
-    exact ha
-  have raysourcesource : seg_nd.extension.source = seg_nd.1.target := by
-    rfl
+  have vec_ndtoVec : VEC seg_nd.1.source seg_nd.1.target = seg_nd.toVecND.1 := rfl
   have seg_pos : 0 < norm (SegND.toVecND seg_nd) := by
     simp only [VecND.norm_pos]
-  have seg_nonzero : norm (SegND.toVecND seg_nd) ≠ 0 := by linarith
-  have aseg_pos : 0 <norm (SegND.toVecND seg_nd) + a:=by
-    linarith
-  have aseg_nonzero : norm (SegND.toVecND seg_nd) + a ≠ 0:=by
-    linarith
+  have aseg_nonzero : norm (SegND.toVecND seg_nd) + a ≠ 0:= by linarith
   constructor
   use (norm (SegND.toVecND seg_nd)) * (norm (seg_nd.toVecND) + a)⁻¹
   constructor
   apply mul_nonneg
-  linarith[seg_pos]
+  linarith [seg_pos]
   norm_num
   linarith
   constructor
-  rw [←mul_inv_cancel aseg_nonzero]
+  rw [← mul_inv_cancel aseg_nonzero]
   apply mul_le_mul
   linarith
   linarith
   norm_num
   linarith
   linarith
   simp only [Seg.target]
-  rw [←raysourcesegtarget] at ha
-  rw [←sourcetargetA, ha, vec_ndtoVec]
-  have raydir : seg_nd.extension.toDir.unitVec = seg_nd.toVecND.toDir.unitVec := by
-    exact rfl
-  rw [raydir, ←VecND.norm_smul_toDir_unitVec (seg_nd.toVecND), ←add_smul,
-  ← mul_smul,mul_assoc,inv_mul_cancel,mul_one]
+  rw [← raysourcesegtarget] at ha
+  rw [← sourcetargetA, ha, vec_ndtoVec]
+  have raydir : seg_nd.extension.toDir.unitVec = seg_nd.toVecND.toDir.unitVec := rfl
+  rw [raydir, ← VecND.norm_smul_toDir_unitVec (seg_nd.toVecND), ← add_smul,
+    ← mul_smul,mul_assoc,inv_mul_cancel,mul_one]
   linarith
   exact seg_nd.2
-  rw [←raysourcesegtarget] at nonsource
-  symm
-  exact nonsource
-
+  exact nonsource.symm
 
 /-- If a point lies on the ray associated to a segment, then either it lies on the segment or it lies on the extension ray of the segment. -/
 theorem lies_on_seg_nd_or_extension_of_lies_on_toRay {seg_nd : SegND P} {A : P} (h : A LiesOn seg_nd.toRay) : A LiesOn seg_nd ∨ A LiesOn seg_nd.extension := by
@@ -1287,8 +1272,8 @@ theorem lies_on_seg_nd_or_extension_of_lies_on_toRay {seg_nd : SegND P} {A : P}
   · have eq : VEC seg_nd.1.1 A = t • v.toDir.unitVecND := eq
     exact Or.inl ⟨t * ‖v.1‖⁻¹, mul_nonneg tpos (inv_nonneg.mpr (norm_nonneg v.1)),
       (mul_inv_le_iff (norm_pos_iff.2 v.2)).mpr (by rw [mul_one]; exact not_lt.mp h), by
-      simp [eq, mul_smul]
-      rfl⟩
+        simp only [eq, ne_eq, Dir.coe_unitVecND, VecND.norm_coe, Seg.mk_source_target, mul_smul]
+        rfl⟩
 
 /--If a point lies on the extension ray associated to a nondegenerate segment, then it lies on the
 interior of the ray associated to the segment-/
@@ -1396,7 +1381,6 @@ theorem Seg.length_nonneg {seg : Seg P} : 0 ≤ seg.length := dist_nonneg
 /-- A segment has positive length if and only if it is nondegenerate. -/
 theorem Seg.length_pos_iff_nd {seg : Seg P} : 0 < seg.length ↔ seg.IsND :=
   dist_pos.trans ne_comm
---norm_pos_iff.trans toVec_eq_zero_of_deg.symm.not
 
 /-- The length of a given segment is nonzero if and only if the segment is nondegenerate. -/
 theorem Seg.length_ne_zero_iff_nd {seg : Seg P} : 0 ≠ seg.length ↔ seg.IsND :=
@@ -1623,8 +1607,6 @@ theorem Seg.reverse_midpt_eq_midpt {seg : Seg P} : seg.reverse.midpoint = seg.mi
   show (SEG seg.reverse.target m).length = (SEG m seg.reverse.source).length
   rw [length_of_rev_eq_length', ←H2, length_of_rev_eq_length']
 
-
-
 theorem SegND.reverse_midpt_eq_midpt {seg_nd : SegND P} : seg_nd.reverse.midpoint = seg_nd.midpoint :=
   seg_nd.1.reverse_midpt_eq_midpt
 
@@ -1680,14 +1662,15 @@ theorem Seg.nd_iff_exist_int_pt {seg : Seg P} : (∃ (X : P), X LiesInt seg) ↔
   ⟨fun ⟨_, b⟩ ↦ nd_of_exist_int_pt b, fun h ↦ ⟨seg.midpoint, SegND.midpt_lies_int (seg_nd :=⟨seg, h⟩)⟩⟩
 
 /-- If a segment is nondegenerate, it contains an interior point. -/
-theorem SegND.exist_int_pt {seg_nd : SegND P} : ∃ (X : P), X LiesInt seg_nd := ⟨seg_nd.midpoint, midpt_lies_int⟩
+theorem SegND.exist_int_pt {seg_nd : SegND P} : ∃ (X : P), X LiesInt seg_nd :=
+  ⟨seg_nd.midpoint, midpt_lies_int⟩
 
 /-- A segment contains an interior point if and only if its length is positive. -/
 theorem Seg.length_pos_iff_exist_int_pt {seg : Seg P} : 0 < seg.length ↔ (∃ (X : P), X LiesInt seg) :=
   length_pos_iff_nd.trans nd_iff_exist_int_pt.symm
 
-theorem SegND.length_pos_iff_exist_int_pt {seg_nd : SegND P} : 0 < seg_nd.length ↔ (∃ (X : P), X LiesInt seg_nd) := by
-  exact Seg.length_pos_iff_exist_int_pt
+theorem SegND.length_pos_iff_exist_int_pt {seg_nd : SegND P} : 0 < seg_nd.length ↔ (∃ (X : P), X LiesInt seg_nd) :=
+  Seg.length_pos_iff_exist_int_pt
 
 /-- A ray contains two distinct points. -/
 theorem Ray.nontriv (ray : Ray P) : ∃ (A B : P), (A ∈ ray.carrier) ∧ (B ∈ ray.carrier) ∧ (B ≠ A) :=

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean

@@ -162,13 +162,16 @@ theorem suppl_isND_iff_isND : ang.suppl.IsND ↔ ang.IsND :=
   isND_iff_isND_of_add_eq_pi ang.suppl_value_add_value_eq_pi
 
 @[simp]
-theorem suppl_isAcu_iff_isObt : ang.suppl.IsAcu ↔ ang.IsObt := sorry
+theorem suppl_isAcu_iff_isObt : ang.suppl.IsAcu ↔ ang.IsObt :=
+  isAcu_iff_isObt_of_add_eq_pi ang.suppl_value_add_value_eq_pi
 
 @[simp]
-theorem suppl_isObt_iff_isAcu : ang.suppl.IsObt ↔ ang.IsAcu := sorry
+theorem suppl_isObt_iff_isAcu : ang.suppl.IsObt ↔ ang.IsAcu :=
+  isObt_iff_isAcu_of_add_eq_pi ang.suppl_value_add_value_eq_pi
 
 @[simp]
-theorem suppl_isRight_iff_isRight : ang.suppl.IsRight ↔ ang.IsRight := sorry
+theorem suppl_isRight_iff_isRight : ang.suppl.IsRight ↔ ang.IsRight :=
+  isRight_iff_isRight_of_add_eq_pi ang.suppl_value_add_value_eq_pi
 
 theorem suppl_start_ray : ang.suppl.start_ray = ang.end_ray := rfl
 
@@ -361,20 +364,23 @@ theorem IsAlternateIntAng.symm {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng
     rw [h.2]
     exact (ang₂.end_dirLine.rev_rev_eq_self).symm⟩
 
-theorem value_eq_of_isCorrespondingAng {ang₁ ang₂ : Angle P} (h : IsCorrespondingAng ang₁ ang₂) : ang₁.value = ang₂.value := by
-  apply value_eq_of_dir_eq
-  exact h.1
-  sorry
+theorem value_eq_of_isCorrespondingAng {ang₁ ang₂ : Angle P} (h : IsCorrespondingAng ang₁ ang₂) : ang₁.value = ang₂.value :=
+  value_eq_of_dir_eq h.1 (congrArg DirLine.toDir h.2)
 
-theorem dvalue_eq_of_isCorrespondingAng {ang₁ ang₂ : Angle P} (h : IsCorrespondingAng ang₁ ang₂) : ang₁.dvalue = ang₂.dvalue := sorry
+theorem dvalue_eq_of_isCorrespondingAng {ang₁ ang₂ : Angle P} (h : IsCorrespondingAng ang₁ ang₂) : ang₁.dvalue = ang₂.dvalue :=
+  dvalue_eq_of_dir_eq h.1 (congrArg DirLine.toDir h.2)
 
-theorem value_eq_value_add_pi_of_isConsecutiveIntAng {ang₁ ang₂ : Angle P} (h : IsConsecutiveIntAng ang₁ ang₂) : ang₁.value = ang₂.value + π := sorry --`first mod 2π, then discuss +-? `
+theorem value_eq_value_add_pi_of_isConsecutiveIntAng {ang₁ ang₂ : Angle P} (h : IsConsecutiveIntAng ang₁ ang₂) : ang₁.value = ang₂.value + π :=
+  value_eq_value_add_pi_of_dir_eq_neg_dir_of_dir_eq h.1 (congrArg DirLine.toDir h.2)
 
-theorem dvalue_eq_of_isConsecutiveIntAng {ang₁ ang₂ : Angle P} (h : IsConsecutiveIntAng ang₁ ang₂) : ang₁.dvalue = ang₂.dvalue := sorry --`first mod 2π, then discuss +-? `
+theorem dvalue_eq_of_isConsecutiveIntAng {ang₁ ang₂ : Angle P} (h : IsConsecutiveIntAng ang₁ ang₂) : ang₁.dvalue = ang₂.dvalue :=
+  dvalue_eq_dvalue_of_dir_eq_neg_dir_of_dir_eq h.1 (congrArg DirLine.toDir h.2)
 
-theorem value_eq_of_isAlternateIntAng {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry
+theorem value_eq_of_isAlternateIntAng {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng ang₁ ang₂) : ang₁.value = ang₂.value :=
+  value_eq_of_dir_eq_neg_dir h.1 (congrArg DirLine.toDir h.2)
 
-theorem dvalue_eq_of_isAlternateIntAng {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng ang₁ ang₂) : ang₁.dvalue = ang₂.dvalue := sorry
+theorem dvalue_eq_of_isAlternateIntAng {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng ang₁ ang₂) : ang₁.dvalue = ang₂.dvalue :=
+  dvalue_eq_of_dir_eq_neg_dir h.1 (congrArg DirLine.toDir h.2)
 
 /-
 -- equivlently, this will be much more lengthy

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean

@@ -159,17 +159,29 @@ theorem dvalue_eq_pi_div_two_at_perp_foot {A B C : P} [_h : PtNe B C] (l : Line
   simp only [hc, Line.eq_line_of_pt_pt_of_ne (perp_foot_lies_on_line A l) hb]
   exact line_of_self_perp_foot_perp_line_of_not_lies_on ha
 
-theorem perp_foot_lies_int_start_ray_iff_isAcu {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) LiesInt (RAY O A) ↔ (ANG A O B).IsAcu := sorry
-
-theorem perp_foot_lies_int_start_ray_iff_isAcu_of_lies_int_end_ray {A : P} (ha : A LiesInt ang.end_ray) : perp_foot A ang.start_ray LiesInt ang.start_ray ↔ ang.IsAcu := sorry
-
-theorem perp_foot_eq_source_iff_isRight {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) = O ↔ (ANG A O B).IsRight := sorry
-
-theorem perp_foot_eq_source_iff_isRight_of_lies_int_end_ray {A : P} (ha : A LiesInt ang.end_ray) : perp_foot A ang.start_ray = ang.source ↔ ang.IsRight := sorry
-
-theorem perp_foot_lies_int_start_ray_reverse_iff_isObt {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) LiesInt (RAY O A).reverse ↔ (ANG A O B).IsObt := sorry
-
-theorem perp_foot_lies_int_start_ray_reverse_iff_isObt_of_lies_int_end_ray {A : P} (ha : A LiesInt ang.end_ray) : perp_foot A ang.start_ray.reverse LiesInt ang.start_ray ↔ ang.IsObt := sorry
+theorem perp_foot_lies_int_start_ray_iff_isAcu {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) LiesInt (RAY O A) ↔ (ANG A O B).IsAcu := by
+  refine' ((RAY O A).lies_int_iff_pos_of_vec_eq_smul_toDir
+    (vec_pt_perp_foot_eq_ddist_smul_toDir_unitVec O B (@DirLine.fst_pt_lies_on_mk_pt_pt P _ O A _))).trans
+      (Iff.trans _ (inner_pos_iff_isAcu A O B))
+  show 0 < inner (VEC O B) (‖VEC O A‖⁻¹ • (VEC O A)) ↔ 0 < inner (VEC O A) (VEC O B)
+  rw [real_inner_smul_right, real_inner_comm]
+  exact mul_pos_iff_of_pos_left (inv_pos.mpr (VEC_nd O A).norm_pos)
+
+theorem perp_foot_eq_source_iff_isRight {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) = O ↔ (ANG A O B).IsRight := by
+  refine' ((RAY O A).eq_source_iff_eq_zero_of_vec_eq_smul_toDir
+    (vec_pt_perp_foot_eq_ddist_smul_toDir_unitVec O B (@DirLine.fst_pt_lies_on_mk_pt_pt P _ O A _))).trans
+      (Iff.trans _ (inner_eq_zero_iff_isRight A O B))
+  show inner (VEC O B) (‖VEC O A‖⁻¹ • (VEC O A)) = 0 ↔ inner (VEC O A) (VEC O B) = 0
+  rw [real_inner_smul_right, real_inner_comm]
+  exact smul_eq_zero_iff_right (ne_of_gt (inv_pos.mpr (VEC_nd O A).norm_pos))
+
+theorem perp_foot_lies_int_start_ray_reverse_iff_isObt {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) LiesInt (RAY O A).reverse ↔ (ANG A O B).IsObt := by
+  refine' ((RAY O A).lies_int_rev_iff_neg_of_vec_eq_smul_toDir
+    (vec_pt_perp_foot_eq_ddist_smul_toDir_unitVec O B (@DirLine.fst_pt_lies_on_mk_pt_pt P _ O A _))).trans
+      (Iff.trans _ (inner_neg_iff_isObt A O B))
+  show inner (VEC O B) (‖VEC O A‖⁻¹ • (VEC O A)) < 0 ↔ inner (VEC O A) (VEC O B) < 0
+  rw [real_inner_smul_right, real_inner_comm]
+  exact smul_neg_iff_of_pos_left (inv_pos.mpr (VEC_nd O A).norm_pos)
 
 end perp_foot