Merge branch 'master' into angvalue

EuclideanGeometry/Example/ShanZun/Ex1c.lean

@@ -57,7 +57,6 @@ lemma aec_colinear : colinear A E C := by
 
 lemma midpt_half_length : (SEG A D).length = (SEG A B).length/2:=by
   rw[length_eq_length_add_length (seg:= SEG A B) (A := D),← dist_target_eq_dist_source_of_eq_midpt,half_add_self]
-  simp only [Seg.source]
   exact hd
   rw[hd]
   exact Seg.midpt_lies_on
@@ -122,15 +121,17 @@ lemma hnd'' : ¬ colinear C D E := by
     exact hd
   apply hnd this
 lemma ade_sim_abc: TRI_nd A D E (@hnd' P _ A B C hnd D hd E he) ∼ TRI_nd A B C hnd := by
+  let tri_nd_ADE := TRI_nd A D E (@hnd' P _ A B C hnd D hd E he)
+  let tri_nd_ABC := TRI_nd A B C hnd
   apply sim_of_SAS
   simp only [Triangle_nd.edge₂,Triangle_nd.edge₃, Triangle.edge₂,Triangle.edge₃]
-  have tr13: (TRI A D E).point₃=E:= rfl
-  have tr23: (TRI A B C).point₃ =C:= rfl
-  have tr11: (TRI A D E).point₁=A:= rfl
-  have tr21: (TRI A B C).point₁ =A:= rfl
-  have tr12: (TRI A D E).point₂=D:= rfl
-  have tr22: (TRI A B C).point₂ =B := rfl
-  rw[tr13, tr12, tr11, tr23, tr22, tr21, ← Seg.length_of_rev_eq_length, ← (SEG C A).length_of_rev_eq_length]
+  have tr13: tri_nd_ADE.1.point₃=E:= rfl
+  have tr23: tri_nd_ABC.1.point₃ =C:= rfl
+  have tr11: tri_nd_ADE.1.point₁=A:= rfl
+  have tr21: tri_nd_ABC.1.point₁ =A:= rfl
+  have tr12: tri_nd_ADE.1.point₂=D:= rfl
+  have tr22: tri_nd_ABC.1.point₂ =B := rfl
+  rw [tr13, tr12, tr11, tr23, tr22, tr21, ← Seg.length_of_rev_eq_length, ← (SEG C A).length_of_rev_eq_length]
   simp only [Seg.reverse]
   rw[ae_ratio,ad_ratio]
   use C

EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean

@@ -116,7 +116,7 @@ theorem neg_Vec_nd_norm_eq_Vec_nd_norm (x : Vec_nd) : (-x).norm = x.norm := by
   simp only [ne_eq, fst_neg_Vec_nd_is_neg_fst_Vec_nd, norm_of_Vec_nd_eq_norm_of_Vec_nd_fst, neg_Vec_norm_eq_Vec_norm]
 
 @[ext]
-class Dir where
+structure Dir where
   toVec : Vec
   unit : @inner ℝ _ _ toVec toVec = 1
 
@@ -209,12 +209,10 @@ instance : Monoid Dir where
     ext : 1
     unfold toVec HMul.hMul instHMul Mul.mul Semigroup.toMul instSemigroupDir instMulDir
     simp only [Dir.one_eq_one_toComplex, one_mul]
-    rfl
   mul_one := fun _ => by
     ext : 1
     unfold toVec HMul.hMul instHMul Mul.mul Semigroup.toMul instSemigroupDir instMulDir
     simp only [Dir.one_eq_one_toComplex, mul_one]
-    rfl
 
 instance : CommGroup Dir where
   inv := fun x => {

EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean

@@ -6,7 +6,7 @@ namespace EuclidGeom
 
 /- Class of Circles-/
 @[ext]
-class Circle (P : Type _) [EuclideanPlane P] where
+structure Circle (P : Type _) [EuclideanPlane P] where
   center : P
   radius : ℝ
   rad_pos : 0 < radius

EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean

@@ -161,7 +161,7 @@ theorem CC_inscribe_point_lieson_circles {ω₁ : Circle P} {ω₂ : Circle P} (
         congr
         unfold Dir.toVec Vec_nd.toDir Vec_nd.mk_pt_pt
         simp
-        nth_rw 4 [← neg_vec]
+        nth_rw 5 [← neg_vec]
         rw [mul_neg, mul_neg, neg_vec_norm_eq]; rfl
       _ = Vec.norm ((Vec_nd.norm (VEC_nd ω₁.center ω₂.center h.2.symm) + ω₁.radius) • (VEC_nd ω₁.center ω₂.center h.2.symm).toDir.1) := by
         rw [add_smul, Vec_nd.self_eq_norm_smul_todir]
@@ -190,8 +190,9 @@ theorem CC_inscribe_point_centers_colinear {ω₁ : Circle P} {ω₂ : Circle P}
         congr
         unfold Dir.toVec Vec_nd.toDir Vec_nd.mk_pt_pt
         simp
-        nth_rw 2 [← neg_vec]
+        nth_rw 3 [← neg_vec]
         rw [← mul_neg, neg_vec_norm_eq]
+        simp only [neg_neg]
       _ = - ω₁.radius • (VEC_nd ω₁.center ω₂.center h.2.symm).toDir.1 := by
         rw [smul_neg, neg_smul]
       _ = (- ω₁.radius) • ((Vec.norm (VEC ω₁.center ω₂.center))⁻¹ • (VEC ω₁.center ω₂.center)) := rfl

EuclideanGeometry/Foundation/Axiom/Linear/Line.lean

@@ -152,20 +152,28 @@ end make
 
 section coercion
 
+@[pp_dot]
 def DirLine.toDir (l : DirLine P) : Dir := Quotient.lift (s := same_dir_line.setoid) (fun ray => ray.toDir) (fun _ _ h => h.left) l
 
+@[pp_dot]
 def DirLine.toProj (l : DirLine P) : Proj := l.toDir.toProj
 
+@[pp_dot]
 def DirLine.toLine (l : DirLine P) : Line P := Quotient.lift (⟦·⟧) (fun _ _ h => Quotient.sound $ same_dir_line_le_same_extn_line h) l
 
+@[pp_dot]
 def Ray.toDirLine (ray : Ray P) : DirLine P := ⟦ray⟧
 
+@[pp_dot]
 def Seg_nd.toDirLine (seg_nd : Seg_nd P) : DirLine P := seg_nd.toRay.toDirLine
 
+@[pp_dot]
 def Line.toProj (l : Line P) : Proj := Quotient.lift (s := same_extn_line.setoid) (fun ray : Ray P => ray.toProj) (fun _ _ h => h.left) l
 
+@[pp_dot]
 def Ray.toLine (ray : Ray P) : Line P := ⟦ray⟧
 
+@[pp_dot]
 def Seg_nd.toLine (seg_nd : Seg_nd P) : Line P := ⟦seg_nd.toRay⟧
 
 end coercion
@@ -187,40 +195,6 @@ instance : Coe (Ray P) (Line P) where
 
 end coercion_compatibility
 
-/-
-section ClassDirFig
-
-variable (P : Type _) [EuclideanPlane P]
-
-class DirFig (α : Type*) where
-  toDirLine : α → DirLine P
-
-instance DirLine.instDirFig : DirFig P (DirLine P) where
-  toDirLine l := l
-
-instance Ray.instDirFig : DirFig P (Ray P) where
-  toDirLine := Quotient.mk (@same_dir_line.setoid P _)
-
-instance Seg_nd.instDirFig : DirFig P (Seg_nd P) where
-  toDirLine s := Quotient.mk (@same_dir_line.setoid P _) s.toRay
-
-section DirFig
-
-variable {P : Type _} [EuclideanPlane P] {α : Type _} [DirFig P α] (l : α)
-
-def toDir : Dir := (@DirFig.toDirLine P _ _ _ l).toDir
-
-def toProj : Proj := (@DirFig.toDirLine P _ _ _ l).toDir.toProj
-
-def toLine : Line P := (@DirFig.toDirLine P _ _ _ l).toLine
-
--- And other definitions, such as IsLeft, IsRight, OnLine, odist, sign, and so on.
-
-end DirFig
-
-end ClassDirFig
--/
-
 open Classical
 
 section carrier
@@ -310,6 +284,7 @@ end dirline_toray
 
 section reverse
 
+@[pp_dot]
 def DirLine.reverse (l : DirLine P) : DirLine P := by
   refine' Quotient.lift (⟦·.reverse⟧) (fun a b h ↦ _) l
   exact (@Quotient.eq _ same_dir_line.setoid _ _).mpr ⟨neg_inj.mpr h.left, Ray.lies_on_rev_or_lies_on_iff.mp h.2⟩
@@ -583,8 +558,8 @@ theorem Line.nontriv (l : Line P) : ∃ (A B : P), A LiesOn l ∧ B LiesOn l ∧
 theorem Ray.lies_on_ray_or_lies_on_ray_rev_iff : A LiesOn r ∧ A ≠ r.source ∨ A LiesOn r.reverse ∧ A ≠ r.source ∨ A = r.source ↔ A LiesOn r ∨ A LiesOn r.reverse := ⟨
   fun | .inl h => .inl h.1
       | .inr h => .casesOn h (fun h => .inr h.1) (fun h => .inr (by rw[h]; exact source_lies_on)),
-  fun | .inl h => if g : A = source then .inr (.inr g) else .inl ⟨h, g⟩
-      | .inr h => if g : A = source then .inr (.inr g) else .inr (.inl ⟨h, g⟩)⟩
+  fun | .inl h => if g : A = r.source then .inr (.inr g) else .inl ⟨h, g⟩
+      | .inr h => if g : A = r.source then .inr (.inr g) else .inr (.inl ⟨h, g⟩)⟩
 
 theorem Ray.lies_on_toline_iff_lies_int_or_lies_int_rev_or_eq_source {r : Ray P} : (A LiesOn r.toLine) ↔ (A LiesInt r) ∨ (A LiesInt r.reverse) ∨ (A = r.source) := by
   rw [lies_int_def, lies_int_def, source_of_rev_eq_source, lies_on_ray_or_lies_on_ray_rev_iff, lies_on_toline_iff_lies_on_or_lies_on_rev]
@@ -747,7 +722,7 @@ theorem linear {l : Line P} {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l)
           exact a
         have b' : B ∈ ray'.carrier := lies_on_pt_todir_of_pt_lies_on_rev b a'
         have c' : C ∈ ray'.carrier := lies_on_pt_todir_of_pt_lies_on_rev c a'
-        exact Ray.colinear_of_lies_on (Ray.source_lies_on) b' c'
+        exact Ray.colinear_of_lies_on (ray'.source_lies_on) b' c'
   | inr a =>
     cases b with
     | inl b =>
@@ -756,7 +731,7 @@ theorem linear {l : Line P} {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l)
         let ray' := Ray.mk A ray.toDir
         have b' : B ∈ ray'.carrier := lies_on_pt_todir_of_pt_lies_on_rev b a
         have c' : C ∈ ray'.carrier := lies_on_pt_todir_of_pt_lies_on_rev c a
-        exact Ray.colinear_of_lies_on (Ray.source_lies_on) b' c'
+        exact Ray.colinear_of_lies_on (ray'.source_lies_on) b' c'
       | inr c =>
         let ray' := Ray.mk B ray.reverse.toDir
         have b' : B LiesOn ray.reverse.reverse := by

EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean

@@ -56,15 +56,15 @@ section definition
 
 /-- A \emph{ray} consists of a pair of a point $P$ and a direction; it is the ray that starts at the point and extends in the given direction. -/
 @[ext]
-class Ray (P : Type _) [EuclideanPlane P] where
+structure Ray (P : Type _) [EuclideanPlane P] where
   /-- returns the source of the ray. -/
   source : P
   /-- returns the direction of the ray. -/
   toDir : Dir
 
 /-- A \emph{Segment} consists of a pair of points: the source and the target; it is the segment from the source to the target. (We allow the source and the target to be the same.) -/
 @[ext]
-class Seg (P : Type _) [EuclideanPlane P] where
+structure Seg (P : Type _) [EuclideanPlane P] where
   /-- returns the source of the segment. -/
   source : P
   /-- returns the target of the segment. -/
@@ -171,25 +171,29 @@ instance : Coe (Seg_nd P) (Seg P) where
   coe := fun x => x.1
 
 /-- Given a nondegenerate segment, this function returns the source of the segment. -/
-@[simp]
+@[simp, pp_dot]
 def source (seg_nd : Seg_nd P) : P := seg_nd.1.source
 
 /-- Given a nondegenerate segment, this function returns the target of the segment. -/
-@[simp]
+@[simp, pp_dot]
 def target (seg_nd : Seg_nd P) : P := seg_nd.1.target
 
 /-- Given a nondegenerate segment $AB$, this function returns the nondegenerate vector $\overrightarrow{AB}$. -/
+@[pp_dot]
 def toVec_nd (seg_nd : Seg_nd P) : Vec_nd := ⟨VEC seg_nd.source seg_nd.target, (ne_iff_vec_ne_zero _ _).mp seg_nd.2⟩
 
 /-- Given a nondegenerate segment $AB$, this function returns the direction associated to the segment, defined by normalizing the nondegenerate vector $\overrightarrow{AB}$. -/
+@[pp_dot]
 def toDir (seg_nd : Seg_nd P) : Dir := Vec_nd.toDir seg_nd.toVec_nd
 
 /-- Given a nondegenerate segment $AB$, this function returns the ray $AB$, whose source is $A$ in the direction of $B$. -/
+@[pp_dot]
 def toRay (seg_nd : Seg_nd P) : Ray P where
   source := seg_nd.1.source
   toDir := seg_nd.toDir
 
 /-- Given a nondegenerate segment $AB$, this function returns the projective direction  of $AB$, defined as the projective direction of the nondegenerate vector $\overrightarrow{AB}$.  -/
+@[pp_dot]
 def toProj (seg_nd : Seg_nd P) : Proj := (seg_nd.toVec_nd.toProj : Proj)
 
 /-- Given a point $A$ and a nondegenerate segment $seg_nd$, this function returns whether $A$ lies on $seg_nd$, namely, whether it lies on the corresponding segment.-/
@@ -654,11 +658,13 @@ end lieson_compatibility
 section reverse
 
 /-- Given a ray, this function returns the ray with the same source but with reversed direction. -/
+@[pp_dot]
 def Ray.reverse (ray : Ray P): Ray P where
   source := ray.source
   toDir := - ray.toDir
 
 /-- Given a segment $AB$, this function returns its reverse, i.e. the segment $BA$. -/
+@[pp_dot]
 def Seg.reverse (seg : Seg P): Seg P where
   source := seg.target
   target := seg.source
@@ -880,7 +886,7 @@ theorem Ray.not_lies_on_of_lies_int_rev {A : P} {ray : Ray P} (liesint : A LiesI
 theorem Ray.not_lies_int_of_lies_on_rev {A : P} {ray : Ray P} (liesint : A LiesOn ray.reverse) : ¬ A LiesInt ray := by
   by_contra h
   rw [← Ray.rev_rev_eq_self (ray:=ray)] at h
-  have:¬A LiesOn ray.reverse:=by
+  have : ¬ (A LiesOn ray.reverse) := by
     apply not_lies_on_of_lies_int_rev
     exact h
   trivial
@@ -920,7 +926,8 @@ theorem lies_on_iff_lies_on_toray_and_rev_toray {X : P} {seg_nd : Seg_nd P} : X
   simp only[inv_nonneg]
   linarith
   linarith
-  rw[h, mul_smul, this, ← Vec_nd.norm_smul_todir_eq_self seg_nd.toVec_nd, smul_smul, smul_smul, mul_assoc, ← norm_of_Vec_nd_eq_norm_of_Vec_nd_fst,inv_mul_cancel (Vec_nd.norm_ne_zero seg_nd.toVec_nd),mul_one]
+  rw [h, mul_smul, this, ← Vec_nd.norm_smul_todir_eq_self seg_nd.toVec_nd, smul_smul, smul_smul, mul_assoc, ← norm_of_Vec_nd_eq_norm_of_Vec_nd_fst,inv_mul_cancel (Vec_nd.norm_ne_zero seg_nd.toVec_nd),mul_one]
+  rfl
 
 -- `This theorem really concerns about the total order on a line`
 /-- Let $ray$ be a ray, and let $A$ be a point on $ray$, and $B$ a point on the reverse of $ray$. Then $A$ lies on the ray starting at $B$ in the same direction of $\ray$. -/
@@ -932,18 +939,23 @@ theorem lies_on_pt_todir_of_pt_lies_on_rev {A B : P} {ray : Ray P} (hA : A LiesO
   constructor
   linarith
   simp only
-  rw [add_smul, ← vec_sub_vec ray.source, ha, hb, sub_neg_eq_add]
+  rw [add_smul, ← vec_sub_vec ray.source, ha, hb]
+  simp only [Complex.real_smul, Dir.tovec_neg_eq_neg_tovec, smul_neg, sub_neg_eq_add]
 
 /-- Given two rays $ray_1$ and $ray_2$ in same direction, the source of $ray_1$ lies on $ray_2$ if and only if the source of $ray_2$ lies on the reverse of $ray_1$. -/
 theorem lies_on_iff_lies_on_rev_of_same_todir {ray₁ ray₂ : Ray P} (h : ray₁.toDir = ray₂.toDir) : ray₁.source LiesOn ray₂ ↔ ray₂.source LiesOn ray₁.reverse := by
   constructor
   · intro ⟨t, ht, eq⟩
     refine' ⟨t, ht, _⟩
-    rw [Dir.tovec_neg_eq_neg_tovec, smul_neg, h, ← eq]
+    simp only [Ray.source_of_rev_eq_source, Ray.todir_of_rev_eq_neg_todir,
+      Dir.tovec_neg_eq_neg_tovec, smul_neg, h]
+    rw [← eq]
     exact (neg_vec ray₂.source ray₁.source).symm
   · intro ⟨t, ht, eq⟩
     refine' ⟨t, ht, _⟩
-    rw [Dir.tovec_neg_eq_neg_tovec, smul_neg, ← neg_vec, h] at eq
+    simp only [Ray.source_of_rev_eq_source, Ray.todir_of_rev_eq_neg_todir,
+      Dir.tovec_neg_eq_neg_tovec, smul_neg] at eq
+    rw [← neg_vec, h] at eq
     exact neg_inj.mp eq
 
 /-- Given two rays $ray_1$ and $ray_2$ in same direction, the source of $ray_1$ lies in the interior of $ray_2$ if and only if the source of $ray_2$ lies in the interior of the reverse of $ray_1$. -/
@@ -987,7 +999,9 @@ theorem lies_on_or_rev_iff_exist_real_vec_eq_smul {A : P} {ray : Ray P} : (A Lie
     rcases h with ⟨t, _, eq⟩ | ⟨t, _, eq⟩
     · use t, eq
     · use - t
-      rw [Dir.tovec_neg_eq_neg_tovec, smul_neg, ← neg_smul] at eq
+      simp only [Ray.source_of_rev_eq_source, Ray.todir_of_rev_eq_neg_todir,
+        Dir.tovec_neg_eq_neg_tovec, smul_neg] at eq
+      rw [← neg_smul] at eq
       exact eq
   · intro h
     choose t ht using h
@@ -1019,6 +1033,7 @@ end reverse
 section extension
 
 /-- Define the extension ray of a nondegenerate segment to be the ray whose origin is the target of the segment whose direction is the same as that of the segment. -/
+@[pp_dot]
 def Seg_nd.extension (seg_nd : Seg_nd P) : Ray P where
   source := seg_nd.target
   toDir := seg_nd.toDir
@@ -1116,7 +1131,10 @@ theorem lies_on_seg_nd_or_extension_of_lies_on_toray {seg_nd : Seg_nd P} {A : P}
   let v : Vec_nd := ⟨VEC seg_nd.1.1 seg_nd.1.2, (ne_iff_vec_ne_zero _ _).mp seg_nd.2⟩
   by_cases h : t > ‖v.1‖
   · refine' Or.inr ⟨t - ‖v.1‖, sub_nonneg.mpr (le_of_lt h), _⟩
-    rw [sub_smul, ← eq]
+    simp only [Seg_nd.toray_todir_eq_todir] at eq
+    rw [sub_smul]
+    simp only [Seg_nd.extn_todir]
+    rw [← eq]
     refine' eq_sub_of_add_eq (add_eq_of_eq_sub' _)
     rw [vec_sub_vec']
     exact v.norm_smul_todir_eq_self
@@ -1131,9 +1149,11 @@ end extension
 section length
 
 /-- This function gives the length of a given segment, which is the norm of the vector associated to the segment. -/
+@[pp_dot]
 def Seg.length (seg : Seg P) : ℝ := norm (seg.toVec)
 
 /-- This function defines the length of a nondegenerate segment, which is just the length of the segment. -/
+@[pp_dot]
 def Seg_nd.length (seg_nd : Seg_nd P) : ℝ := seg_nd.1.length
 
 /-- Every segment has nonnegative length. -/
@@ -1194,8 +1214,10 @@ end length
 section midpoint
 
 /-- Given a segment $AB$, this function returns the midpoint of $AB$, defined as moving from $A$ by the vector $\overrightarrow{AB}/2$. -/
+@[pp_dot]
 def Seg.midpoint (seg : Seg P): P := (1 / 2 : ℝ) • seg.toVec +ᵥ seg.source
 
+@[pp_dot]
 def Seg_nd.midpoint (seg_nd : Seg_nd P): P := seg_nd.1.midpoint
 
 theorem Seg.vec_source_midpt {seg : Seg P} : VEC seg.1 seg.midpoint = 1 / 2 * VEC seg.1 seg.2 := by
@@ -1346,7 +1368,7 @@ theorem Seg_nd.exist_pt_beyond_pt (l : Seg_nd P) : (∃ q : P, l.target LiesInt
     If a segment contains an interior point, then it is nondegenerate-/
 theorem Seg.nd_of_exist_int_pt {X : P} {seg : Seg P} (h : X LiesInt seg) : seg.is_nd := by
   rcases h with ⟨⟨_, ⟨_, _, e⟩⟩, ⟨p_ne_s, _⟩⟩
-  have t : VEC Seg.source X ≠ 0 := (ne_iff_vec_ne_zero Seg.source X).mp p_ne_s
+  have t : VEC seg.source X ≠ 0 := (ne_iff_vec_ne_zero seg.source X).mp p_ne_s
   rw [e] at t
   exact Iff.mp vsub_ne_zero (right_ne_zero_of_smul t)
 

EuclideanGeometry/Foundation/Axiom/Position/Angle.lean

@@ -6,7 +6,7 @@ namespace EuclidGeom
 /- Define values of oriented angles, in (-π, π], modulo 2 π. -/
 /- Define oriented angles, ONLY taking in two rays starting at one point!  And define ways to construct oriented angles, by given three points on the plane, and etc.  -/
 @[ext]
-class Angle (P : Type _) [EuclideanPlane P] where
+structure Angle (P : Type _) [EuclideanPlane P] where
   start_ray : Ray P
   end_ray : Ray P
   source_eq_source : start_ray.source = end_ray.source