Changed the name of right angle from IsRight to IsRt

And add definitions and basic properties of right triangles and obtuse triangles

EuclideanGeometry/Example/ShanZun/Ex1c'.lean

@@ -31,7 +31,7 @@ structure Setting (Plane : Type*) [EuclideanPlane Plane] where
     -- This is because vertices $B, C$ of a nondegenerate triangle are distinct.
     (ne_of_not_collinear not_collinear_ABC).2.2
   --Let $D$ be the midpoint of $AB$
-  hrt: (ANG A C B C_ne_A.symm B_ne_C).IsRightAngle
+  hrt: (ANG A C B C_ne_A.symm B_ne_C).IsRtAngle
   D : Plane
   hD : D = (SEG A B).midpoint
 

EuclideanGeometry/Example/ShanZun/Ex1c.lean

@@ -20,7 +20,7 @@ lemma B_ne_a : B ≠ A := (ne_of_not_collinear hnd).2.2
 lemma c_ne_a : C ≠ A := (ne_of_not_collinear hnd).2.1.symm
 lemma B_ne_C : B ≠ C := (ne_of_not_collinear hnd).1.symm
 --∠ A C B = π/2
-variable {hrt : (ANG A C B c_ne_a.symm B_ne_C).IsRightAngle}
+variable {hrt : (ANG A C B c_ne_a.symm B_ne_C).IsRtAngle}
 -- D is the midpoint of segment AB
 variable {D : P} {hd : D = (SEG A B).midpoint}
 lemma d_ne_a: D ≠ A := by

EuclideanGeometry/Foundation/Axiom/Basic/Class.lean

@@ -126,21 +126,21 @@ instance (α : Type*) [HasCongr α] : IsEquiv α HasCongr.congr where
   trans _ _ _ := HasCongr.trans
   symm _ _ := HasCongr.symm
 
-scoped infix : 50 " ≅ " => HasCongr.congr
-
 scoped infix : 50 " IsCongrTo " => HasCongr.congr
 
+scoped infix : 50 " ≅ " => HasCongr.congr
+
 class HasACongr (α : Type*) where
   acongr : α → α → Prop
   symm : ∀ {a b : α}, acongr a b → acongr b a
 
 instance (α : Type*) [HasACongr α] : IsSymm α HasACongr.acongr where
   symm _ _ := HasACongr.symm
 
-scoped infix : 50 " ≅ₐ " => HasACongr.acongr
-
 scoped infix : 50 " IsACongrTo " => HasACongr.acongr
 
+scoped infix : 50 " ≅ₐ " => HasACongr.acongr
+
 class HasSim (α : Type*) where
   sim : α → α → Prop
   refl : ∀ (a : α), sim a a
@@ -152,23 +152,23 @@ instance (α : Type*) [HasSim α] : IsEquiv α HasSim.sim where
   trans _ _ _ := HasSim.trans
   symm _ _ := HasSim.symm
 
-/-- The similarity relation is denoted by infix $\sim$.-/
-scoped infix : 50 " ∼ " => HasSim.sim
-
 /-- The similarity relation is denoted by infix "IsSimTo".-/
 scoped infix : 50 " IsSimTo " => HasSim.sim
 
+/-- The similarity relation is denoted by infix $\sim$.-/
+scoped infix : 50 " ∼ " => HasSim.sim
+
 class HasASim (α : Type*) where
   asim : α → α → Prop
   symm : ∀ {a b : α}, asim a b → asim b a
 
 instance (α : Type*) [HasACongr α] : IsSymm α HasACongr.acongr where
   symm _ _ := HasACongr.symm
 
-/-- The anti-similarity relation is denoted by infix $\sim_a$.-/
-scoped infix : 50 " ∼ₐ " => HasASim.asim
-
 /-- The anti-similarity relation is denoted by infix "IsASimTo".-/
 scoped infix : 50 " IsASimTo " => HasASim.asim
 
+/-- The anti-similarity relation is denoted by infix $\sim_a$.-/
+scoped infix : 50 " ∼ₐ " => HasASim.asim
+
 end EuclidGeom

EuclideanGeometry/Foundation/Axiom/Position/Angle.lean

@@ -99,7 +99,7 @@ abbrev IsAcu : Prop := ang.value.IsAcu
 abbrev IsObt : Prop := ang.value.IsObt
 
 @[pp_dot]
-abbrev IsRight : Prop := ang.value.IsRight
+abbrev IsRt : Prop := ang.value.IsRt
 
 end Angle
 
@@ -687,11 +687,11 @@ theorem dir_perp_iff_dvalue_eq_pi_div_two : ang.dir₁ ⟂ ang.dir₂ ↔ ang.dv
 theorem line_pt_pt_perp_iff_dvalue_eq_pi_div_two : LIN O A ⟂ LIN O B ↔ (ANG A O B).dvalue = ∡[π / 2] :=
   (ANG A O B).dir_perp_iff_dvalue_eq_pi_div_two
 
-theorem dir_perp_iff_isRight : ang.dir₁ ⟂ ang.dir₂ ↔ ang.IsRight :=
-  dir_perp_iff_dvalue_eq_pi_div_two.trans isRight_iff_coe.symm
+theorem dir_perp_iff_isRt : ang.dir₁ ⟂ ang.dir₂ ↔ ang.IsRt :=
+  dir_perp_iff_dvalue_eq_pi_div_two.trans isRt_iff_coe.symm
 
-theorem line_pt_pt_perp_iff_isRight : LIN O A ⟂ LIN O B ↔ (ANG A O B).IsRight :=
-  (ANG A O B).dir_perp_iff_isRight
+theorem line_pt_pt_perp_iff_isRt : LIN O A ⟂ LIN O B ↔ (ANG A O B).IsRt :=
+  (ANG A O B).dir_perp_iff_isRt
 
 theorem value_eq_pi_of_lies_int_seg_nd {A B C : P} [PtNe C A] (h : B LiesInt (SEG_nd A C)) : ∠ A B C h.2.symm h.3.symm = π :=
   value_eq_pi_of_eq_neg_dir ((SEG_nd A C).toDir_eq_neg_toDir_of_lies_int h)
@@ -737,11 +737,11 @@ theorem cos_pos_iff_isAcu : 0 < cos ang.value ↔ ang.IsAcu :=
 theorem cos_neg_iff_isObt : cos ang.value < 0 ↔ ang.IsObt :=
   isObt_iff_cos_neg.symm
 
-theorem cos_ne_zero_iff_not_isRight : cos ang.value ≠ 0 ↔ ¬ ang.IsRight :=
-  not_isRight_iff_cos_ne_zero.symm
+theorem cos_ne_zero_iff_not_isRt : cos ang.value ≠ 0 ↔ ¬ ang.IsRt :=
+  not_isRt_iff_cos_ne_zero.symm
 
-theorem cos_eq_zero_iff_isRight : cos ang.value = 0 ↔ ang.IsRight :=
-  isRight_iff_cos_eq_zero.symm
+theorem cos_eq_zero_iff_isRt : cos ang.value = 0 ↔ ang.IsRt :=
+  isRt_iff_cos_eq_zero.symm
 
 end sin_cos
 
@@ -760,9 +760,9 @@ theorem inner_pos_iff_isAcu : 0 < @inner ℝ _ _ (VEC O A) (VEC O B) ↔ (∠ A
   exact (mul_pos_iff_of_pos_left (Real.mul_pos (SEG_nd O A).length_pos (SEG_nd O B).length_pos)).trans
     ((∠ A O B).isAcu_iff_cos_pos).symm
 
-theorem inner_eq_zero_iff_isRight : @inner ℝ _ _ (VEC O A) (VEC O B) = 0 ↔ (∠ A O B).IsRight := by
+theorem inner_eq_zero_iff_isRt : @inner ℝ _ _ (VEC O A) (VEC O B) = 0 ↔ (∠ A O B).IsRt := by
   rw [inner_eq_dist_mul_cos A O B]
-  refine' Iff.trans _ ((∠ A O B).isRight_iff_cos_eq_zero).symm
+  refine' Iff.trans _ ((∠ A O B).isRt_iff_cos_eq_zero).symm
   exact smul_eq_zero_iff_right (ne_of_gt (Real.mul_pos (SEG_nd O A).length_pos (SEG_nd O B).length_pos))
 
 theorem inner_neg_iff_isObt : @inner ℝ _ _ (VEC O A) (VEC O B) < 0 ↔ (∠ A O B).IsObt :=by

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean

@@ -73,8 +73,8 @@ theorem oppo_isObt_iff_isObt : ang.oppo.IsObt ↔ ang.IsObt :=
   iff_of_eq (congrArg AngValue.IsObt ang.oppo_value_eq_value)
 
 @[simp]
-theorem oppo_isRight_iff_isRight : ang.oppo.IsRight ↔ ang.IsRight :=
-  iff_of_eq (congrArg AngValue.IsRight ang.oppo_value_eq_value)
+theorem oppo_isRt_iff_isRt : ang.oppo.IsRt ↔ ang.IsRt :=
+  iff_of_eq (congrArg AngValue.IsRt ang.oppo_value_eq_value)
 
 theorem oppo_start_ray : ang.oppo.start_ray = ang.start_ray.reverse := rfl
 
@@ -170,8 +170,8 @@ 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 :=
-  isRight_iff_isRight_of_add_eq_pi ang.suppl_value_add_value_eq_pi
+theorem suppl_isRt_iff_isRt : ang.suppl.IsRt ↔ ang.IsRt :=
+  isRt_iff_isRt_of_add_eq_pi ang.suppl_value_add_value_eq_pi
 
 theorem suppl_start_ray : ang.suppl.start_ray = ang.end_ray := rfl
 
@@ -276,10 +276,10 @@ theorem rev_isObt_iff_isObt : ang.reverse.IsObt ↔ ang.IsObt := by
   exact neg_isObt_iff_isObt
 
 @[simp]
-theorem rev_isRight_iff_isRight : ang.reverse.IsRight ↔ ang.IsRight := by
-  unfold IsRight
+theorem rev_isRt_iff_isRt : ang.reverse.IsRt ↔ ang.IsRt := by
+  unfold IsRt
   rw [rev_value_eq_neg_value]
-  exact neg_isRight_iff_isRight
+  exact neg_isRt_iff_isRt
 
 theorem rev_start_ray : ang.reverse.start_ray = ang.end_ray := rfl
 

EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean

@@ -167,10 +167,10 @@ theorem perp_foot_lies_int_start_ray_iff_isAcu {A O B : P} [PtNe A O] [PtNe B O]
   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
+theorem perp_foot_eq_source_iff_isRt {A O B : P} [PtNe A O] [PtNe B O] : (perp_foot B (LIN O A)) = O ↔ (ANG A O B).IsRt := 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))
+      (Iff.trans _ (inner_eq_zero_iff_isRt 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))

EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean

@@ -158,6 +158,7 @@ variable {P : Type*} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P)
 
 namespace Triangle
 
+@[pp_dot]
 def perm_vertices : (Triangle P) where
   point₁ := tr.point₂
   point₂ := tr.point₃
@@ -169,7 +170,7 @@ def perm_vertices : (Triangle P) where
 theorem eq_self_of_perm_vertices_three_times : tr.perm_vertices.perm_vertices.perm_vertices = tr := rfl
 
 -- flip vertices for triangles means to flip the second and the third vertices.
-
+@[pp_dot]
 def flip_vertices : (Triangle P) where
   point₁ := tr.point₁
   point₂ := tr.point₃

EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean

@@ -4,13 +4,44 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex
 namespace EuclidGeom
 open AngValue
 
-variable {P : Type*} [EuclideanPlane P]
+variable {P : Type*} [EuclideanPlane P] {tr_nd : TriangleND P}
 
-structure TriangleND.IsAcute (tr_nd : TriangleND P) : Prop where
+namespace TriangleND
+
+theorem value_abs_add_value_abs_lt_pi : tr_nd.angle₁.value.abs + tr_nd.angle₂.value.abs < π := sorry
+
+@[pp_dot]
+structure IsAcu (tr_nd : TriangleND P) : Prop where
   angle₁ : tr_nd.angle₁.IsAcu
   angle₂ : tr_nd.angle₂.IsAcu
   angle₃ : tr_nd.angle₃.IsAcu
 
+theorem perm_isAcu_iff_isAcu : tr_nd.perm_vertices.IsAcu ↔ tr_nd.IsAcu := sorry
+
+theorem flip_isAcu_iff_isAcu : tr_nd.flip_vertices.IsAcu ↔ tr_nd.IsAcu := sorry
+
+@[pp_dot]
+def IsRt (tr_nd : TriangleND P) : Prop :=
+  tr_nd.angle₁.IsRt
+
+theorem flip_isRt_iff_isRt : tr_nd.flip_vertices.IsAcu ↔ tr_nd.IsAcu := sorry
+
+theorem angle₂_isAcu_of_isRt (h : tr_nd.IsRt) : tr_nd.angle₂.IsAcu := sorry
+
+theorem angle₃_isAcu_of_isRt (h : tr_nd.IsRt) : tr_nd.angle₃.IsAcu := sorry
+
+@[pp_dot]
+def IsObt (tr_nd : TriangleND P) : Prop :=
+  tr_nd.angle₁.IsObt
+
+theorem flip_isObt_iff_isObt : tr_nd.flip_vertices.IsAcu ↔ tr_nd.IsAcu := sorry
+
+theorem angle₂_isAcu_of_isObt (h : tr_nd.IsObt) : tr_nd.angle₂.IsAcu := sorry
+
+theorem angle₃_isAcu_of_isObt (h : tr_nd.IsObt) : tr_nd.angle₃.IsAcu := sorry
+
+end TriangleND
+
 variable {tr_nd₁ tr_nd₂ : TriangleND P}
 
 theorem edge_toLine_not_para_of_not_collinear {A B C : P} (h : ¬ Collinear A B C) : ¬ (SEG_nd A B (ne_of_not_collinear h).2.2) ∥ SEG_nd B C (ne_of_not_collinear h).1 ∧ ¬  (SEG_nd B C (ne_of_not_collinear h).1) ∥ SEG_nd C A (ne_of_not_collinear h).2.1 ∧ ¬  (SEG_nd C A (ne_of_not_collinear h).2.1) ∥ SEG_nd A B (ne_of_not_collinear h).2.2 := by

EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean

@@ -143,6 +143,9 @@ theorem perm_asim (h : IsASim tr₁ tr₂) : IsASim (perm_vertices tr₁) (perm_
   angle₂ := h.3
   angle₃ := h.1
 
+theorem asim_iff_perm_asim : IsASim tr₁ tr₂ ↔ IsASim (perm_vertices tr₁) (perm_vertices tr₂) :=
+  ⟨fun h ↦ h.perm_asim, fun h ↦ h.perm_asim.perm_asim⟩
+
 theorem ratio₁ : h.ratio = tr₁.edge₁.length / tr₂.edge₁.length := rfl
 
 theorem ratio₂ : h.ratio = tr₁.edge₂.length / tr₂.edge₂.length := by

EuclideanGeometry/Foundation/Axiom/Triangle/Similarity_trash.lean

@@ -0,0 +1,25 @@
+import EuclideanGeometry.Foundation.Axiom.Triangle.Similarity
+
+noncomputable section
+
+namespace EuclidGeom
+
+variable {P : Type*} [EuclideanPlane P]
+
+open TriangleND AngValue
+
+theorem sim_of_AA' (tr₁ tr₂ : TriangleND P) (h₂ : tr₁.angle₂.dvalue = tr₂.angle₂.dvalue) (h₃ : tr₁.angle₃.value = tr₂.angle₃.value) : tr₁ ∼ tr₂ := sorry
+
+theorem sim_of_AA_of_isRt (tr₁ tr₂ : TriangleND P) (h₁ : tr₁.IsRt) (h₂ : tr₂.IsRt) (h : tr₁.angle₂.dvalue = tr₂.angle₂.dvalue) : tr₁ ∼ tr₂ := by
+  refine' IsSim.sim_iff_perm_sim.mpr (IsSim.sim_iff_perm_sim.mpr (sim_of_AA' _ _ _ _))
+  · exact (isRt_iff_coe.mp h₁).trans (isRt_iff_coe.mp h₂).symm
+  · exact eq_of_isAcu_of_coe_eq (angle₂_isAcu_of_isRt h₁) (angle₂_isAcu_of_isRt h₂) h
+
+theorem asim_of_AA' (tr₁ tr₂ : TriangleND P) (h₂ : tr₁.angle₂.dvalue = - tr₂.angle₂.dvalue) (h₃ : tr₁.angle₃.value = - tr₂.angle₃.value) : tr₁ ∼ₐ tr₂ := sorry
+
+theorem asim_of_AA_of_isRt (tr₁ tr₂ : TriangleND P) (h₁ : tr₁.IsRt) (h₂ : tr₂.IsRt) (h : tr₁.angle₂.dvalue = - tr₂.angle₂.dvalue) : tr₁ ∼ₐ tr₂ := by
+  refine' IsASim.asim_iff_perm_asim.mpr (IsASim.asim_iff_perm_asim.mpr (asim_of_AA' _ _ _ _))
+  · sorry
+  · sorry
+
+end EuclidGeom