diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean index 93e93d40..b4d54173 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean @@ -1,6 +1,7 @@ import Mathlib.Analysis.InnerProductSpace.Basic import Mathlib.Analysis.SpecialFunctions.Complex.Arg import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex +import Mathlib.Analysis.Complex.Arg import Mathlib.Data.Real.Sign /-! # Standard Vector Space @@ -72,6 +73,13 @@ theorem Vec.norm_smul_eq_mul_norm {x : ℝ} (x_nonneg : 0 ≤ x) (u : Vec) : Vec simp only [Complex.real_smul, map_mul, Complex.abs_ofReal, mul_eq_mul_right_iff, abs_eq_self, map_eq_zero] tauto +@[simp] +theorem neg_Vec_norm_eq_Vec_norm (z : Vec) : Vec.norm (-z) = Vec.norm z := by + have h : Complex.abs (-z) = Complex.abs (z) := by + simp only [map_neg_eq_map] + unfold Vec.norm + rw [h] + -- norm is nonnegetive theorem Vec.norm_nonnegative (u : Vec) : 0 ≤ Vec.norm u := Real.sqrt_nonneg _ @@ -102,6 +110,10 @@ theorem fst_of_mul_eq_fst_mul_fst (z w : Vec_nd) : (z * w).1 = z.1 * w.1 := by r @[simp] theorem norm_of_Vec_nd_eq_norm_of_Vec_nd_fst (z : Vec_nd) : Vec_nd.norm z = Vec.norm z := rfl +@[simp] +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 toVec : Vec @@ -454,6 +466,27 @@ theorem mk_angle_neg_pi_div_two_eq_neg_I' : mk_angle ((-π) / 2) = -I := by end Make_angle_theorems +-- Here is a small section which would not be used later. We just compare our definitions to the standard sameRay definitions. +section sameRay_theorems + +theorem sameRay_iff_eq (a b : Dir) : SameRay ℝ a.1 b.1 ↔ a = b := by + rw [Complex.sameRay_iff] + constructor + · simp only [tovec_ne_zero, false_or] + intro h + let g := congrArg (fun z => mk_angle z) h + simp only [mk_angle_arg_toComplex_of_Dir_eq_self] at g + exact g + · tauto + +theorem sameRay_Vec_nd_toDir (z : Vec_nd) : SameRay ℝ z.1 z.toDir.1 := by + rw [Complex.sameRay_iff_arg_div_eq_zero, Vec_nd.self_eq_norm_smul_todir z, Complex.real_smul, ← mul_div, div_self (tovec_ne_zero (Vec_nd.toDir z)), mul_one, norm_of_Vec_nd_eq_norm_of_Vec_nd_fst] + exact Complex.arg_ofReal_of_nonneg (Vec.norm_nonnegative z) + +theorem toDir_eq_toDir_of_sameRay (z₁ z₂ : Vec_nd) : SameRay ℝ z₁.1 z₂.1 → z₁.toDir = z₂.toDir := fun h => (sameRay_iff_eq z₁.toDir z₂.toDir).1 (SameRay.symm (SameRay.trans (SameRay.symm (SameRay.trans h (sameRay_Vec_nd_toDir z₂) (by simp only [ne_eq, ne_zero_of_Vec_nd, false_or, IsEmpty.forall_iff]))) (sameRay_Vec_nd_toDir z₁) (by simp only [ne_eq, ne_zero_of_Vec_nd, false_or, IsEmpty.forall_iff]))) + +end sameRay_theorems + instance : SMul Dir Vec where smul := fun d v => d.1 * v @@ -863,7 +896,12 @@ theorem det_eq_zero_iff_eq_smul (u v : Vec) (hu : u ≠ 0) : det u v = 0 ↔ ( rcases e ring -theorem det_eq_zero_of_toProj_eq (u v : Vec_nd) (toprojeq : Vec_nd.toProj u = v.toProj) : det u v = 0 := ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).2) (smul_of_eq_toproj u v toprojeq) +-- det theorems for Vec_nd +theorem det_eq_zero_of_toProj_eq (u v : Vec_nd) (toprojeq : u.toProj = v.toProj) : det u v = 0 := ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).2) (smul_of_eq_toproj u v toprojeq) + +theorem toProj_eq_of_det_eq_zero (u v : Vec_nd) (det_eq_zero : det u v = 0) : u.toProj = v.toProj := (Vec_nd.eq_toproj_iff u v).mpr ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).1 det_eq_zero) + +theorem det_eq_zero_iff_toProj_eq (u v : Vec_nd) : det u v = 0 ↔ u.toProj = v.toProj := ⟨fun z => ((Vec_nd.eq_toproj_iff u v).mpr ((det_eq_zero_iff_eq_smul u.1 v.1 u.2).1 z)), fun z => (((det_eq_zero_iff_eq_smul u.1 v.1 u.2).2) (smul_of_eq_toproj u v z))⟩ theorem det'_ne_zero_of_not_colinear {u v : Vec} (hu : u ≠ 0) (h' : ¬(∃ (t : ℝ), v = t • u)) : det' u v ≠ 0 := by unfold det' diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean index e873a279..e8d34e8b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean @@ -5,6 +5,14 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] -theorem Seg_nd.not_para_rev_of_not_para (seg_nd seg_nd' : Seg_nd P) : (¬ seg_nd ∥ seg_nd') → (¬ seg_nd ∥ seg_nd'.reverse) := sorry +-- Later we need a version of this theorem in class DirFig +theorem Seg_nd.para_self_rev (seg_nd : Seg_nd P) : seg_nd ∥ seg_nd.reverse := Eq.symm (toproj_of_rev_eq_toproj) +-- The followings are corollaries: + +theorem Seg_nd.para_rev_of_para (seg_nd seg_nd' : Seg_nd P) : (seg_nd ∥ seg_nd') ↔ (seg_nd ∥ seg_nd'.reverse) := ⟨fun z => Eq.trans z (Seg_nd.para_self_rev seg_nd'), fun z => Eq.trans z (Eq.symm (Seg_nd.para_self_rev seg_nd'))⟩ + +theorem Seg_nd.not_para_rev_of_not_para (seg_nd seg_nd' : Seg_nd P) : (¬ seg_nd ∥ seg_nd') → (¬ seg_nd ∥ seg_nd'.reverse) := by + let g := (Seg_nd.para_rev_of_para seg_nd seg_nd').2 + tauto end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean index 36ff6920..efd7479c 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean @@ -98,7 +98,13 @@ instance : IntFig Angle where end Angle -theorem eq_end_ray_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := sorry +theorem eq_end_ray_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := by + ext : 1 + rw [← ang₁.source_eq_source, ← ang₂.source_eq_source, (congrArg (fun z => z.source)) h] + let g := (congrArg (fun z => Dir.mk_angle z)) v + unfold Angle.value Dir.angle at g + simp only [Dir.mk_angle_arg_toComplex_of_Dir_eq_self, (congrArg (fun z => z.toDir)) h, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_self, mul_one] at g + exact g theorem eq_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁ = ang₂ := Angle.ext ang₁ ang₂ h (eq_end_ray_of_eq_value_eq_start_ray h v) diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean index 85cb35e6..f51e23d1 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean @@ -20,41 +20,24 @@ def wedge (A B C : P) : ℝ := det (VEC A B) (VEC A C) def oarea (A B C : P) : ℝ := wedge A B C / 2 theorem wedge213 (A B C : P) : wedge B A C = - wedge A B C := by - dsimp only [wedge] - have h1 : VEC B A = (-1 : ℝ) • VEC A B := by - dsimp only [Vec.mk_pt_pt] - rw[Complex.real_smul] - field_simp - rw [h1, det_smul_left_eq_mul_det, det_eq_neg_det, det_eq_neg_det (VEC A B) _] - field_simp - have h2 : VEC B C = VEC A C - VEC A B := by - dsimp only [Vec.mk_pt_pt] - exact Eq.symm (vsub_sub_vsub_cancel_right C B A) - rw [h2, det_sub_eq_det] + unfold wedge + rw [← neg_vec A B, ← neg_one_smul ℝ, det_smul_left_eq_mul_det, det_eq_neg_det, det_eq_neg_det (VEC A B) _, neg_one_mul, neg_neg, neg_neg, ← vec_sub_vec A B C, det_sub_eq_det] theorem wedge132 (A B C : P) : wedge A C B = - wedge A B C := by - dsimp only [wedge] apply det_symm theorem wedge312 (A B C : P) : wedge C A B = wedge A B C := by - rw [wedge213, wedge132] - ring + rw [wedge213, wedge132, neg_neg] theorem wedge231 (A B C : P) : wedge B C A = wedge A B C := by rw [wedge312, wedge312] theorem wedge321 (A B C : P) : wedge C B A = - wedge A B C := by rw [wedge213, wedge231] -theorem wedge_eq_sine_mul_length_mul_length (A B C : P) (aneb : B ≠ A) (anec : C ≠ A) : wedge A B C = (Real.sin (Angle.mk_pt_pt_pt B A C aneb anec).value * (SEG A B).length *(SEG A C).length) := by - dsimp only [wedge] - have vecabnd : VEC A B ≠ 0 := by - exact (ne_iff_vec_ne_zero A B).mp aneb - have vecacnd : VEC A C ≠ 0 := by - exact (ne_iff_vec_ne_zero A C).mp anec - have h0 : (Angle.mk_pt_pt_pt B A C aneb anec).value = Vec_nd.angle ⟨VEC A B , vecabnd⟩ ⟨VEC A C, vecacnd⟩ := by - dsimp only [Angle.mk_pt_pt_pt,Vec_nd.angle,angle_value_eq_dir_angle] - rfl +theorem wedge_eq_sine_mul_length_mul_length (A B C : P) (bnea : B ≠ A) (cnea : C ≠ A) : wedge A B C = (Real.sin (Angle.mk_pt_pt_pt B A C bnea cnea).value * (SEG A B).length *(SEG A C).length) := by + unfold wedge + have h0 : (Angle.mk_pt_pt_pt B A C bnea cnea).value = Vec_nd.angle (VEC_nd A B bnea) (VEC_nd A C cnea) := rfl rw [h0] - apply det_eq_sin_mul_norm_mul_norm ⟨VEC A B , vecabnd⟩ ⟨VEC A C, vecacnd⟩ + apply det_eq_sin_mul_norm_mul_norm (VEC_nd A B bnea) (VEC_nd A C cnea) theorem colinear_iff_wedge_eq_zero (A B C : P) : (colinear A B C) ↔ (wedge A B C = 0) := by dsimp only [wedge] @@ -129,15 +112,13 @@ theorem odist'_eq_sine_mul_length (A : P) (ray : Ray P) (h : A ≠ ray.source) : rw [mul_comm] rfl -theorem wedge_eq_odist'_mul_length (A B C : P) (aneb : B ≠ A) : (wedge A B C) = ((odist' C (RAY A B aneb)) * (SEG A B).length) := by +theorem wedge_eq_odist'_mul_length (A B C : P) (bnea : B ≠ A) : (wedge A B C) = ((odist' C (RAY A B bnea)) * (SEG A B).length) := by by_cases p : C ≠ A - rw [wedge_eq_sine_mul_length_mul_length A B C aneb p,odist'_eq_sine_mul_length C (RAY A B aneb),mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B aneb) C p).value)) ((SEG (RAY A B aneb).source C).length) ((SEG A B).length),mul_comm ((SEG (RAY A B aneb).source C).length) ((SEG A B).length),←mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B aneb) C p).value)) ((SEG A B).length) ((SEG (RAY A B aneb).source C).length)] + rw [wedge_eq_sine_mul_length_mul_length A B C bnea p,odist'_eq_sine_mul_length C (RAY A B bnea),mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B bnea) C p).value)) ((SEG (RAY A B bnea).source C).length) ((SEG A B).length),mul_comm ((SEG (RAY A B bnea).source C).length) ((SEG A B).length),←mul_assoc (Real.sin ((Angle.mk_ray_pt (RAY A B bnea) C p).value)) ((SEG A B).length) ((SEG (RAY A B bnea).source C).length)] congr - simp at p - have vecac0 : VEC A C = 0 := (eq_iff_vec_eq_zero A C).mp p - have vecrayc0 : VEC (RAY A B aneb).source C = 0 := (eq_iff_vec_eq_zero A C).mp p - dsimp only [wedge,odist',det] - field_simp [vecac0,vecrayc0] + have vecrayc0 : VEC (RAY A B bnea).source C = 0 := (eq_iff_vec_eq_zero A C).mp (not_not.1 p) + dsimp only [wedge, odist', det] + field_simp [(eq_iff_vec_eq_zero A C).mp (not_not.1 p), vecrayc0] theorem odist'_eq_odist'_of_to_dirline_eq_to_dirline (A : P) (ray ray' : Ray P) (h : same_dir_line ray ray') : odist' A ray = odist' A ray' := by have h₁ : ray.2.1 =ray'.2.1 := by @@ -224,11 +205,11 @@ end point_toray section oriented_area -theorem oarea_eq_length_mul_odist_div_2 (A B C : P) (aneb : B ≠ A) : (oarea A B C) = ((odist C (Seg_nd.mk A B aneb)) * (SEG A B).length) / 2:= sorry +theorem oarea_eq_length_mul_odist_div_2 (A B C : P) (bnea : B ≠ A) : (oarea A B C) = ((odist C (Seg_nd.mk A B bnea)) * (SEG A B).length) / 2:= sorry theorem oarea_eq_oarea_iff_odist_eq_odist_of_ne (A B C D : P) (bnea : B ≠ A) : (odist C (Seg_nd.mk A B bnea) = odist D (Seg_nd.mk A B bnea)) ↔ oarea A B C = oarea A B D := sorry -theorem oarea_eq_sine_mul_length_mul_length_div_2 (A B C : P) (aneb : B ≠ A) (anec : C ≠ A) : oarea A B C = (Real.sin (Angle.mk_pt_pt_pt B A C aneb anec).value * (SEG A B).length *(SEG A C).length) / 2 := sorry +theorem oarea_eq_sine_mul_length_mul_length_div_2 (A B C : P) (bnea : B ≠ A) (cnea : C ≠ A) : oarea A B C = (Real.sin (Angle.mk_pt_pt_pt B A C bnea cnea).value * (SEG A B).length *(SEG A C).length) / 2 := sorry theorem oarea_eq_zero_of_colinear (A B C : P) : oarea A B C = 0 ↔ colinear A B C := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean index 22a36727..6b47df75 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean @@ -81,8 +81,10 @@ variable {P : Type u} [EuclideanPlane P] namespace Triangle +-- When we have DirFig, rewrite this definition. protected def IsInt (A : P) (tr : Triangle P) : Prop := by by_cases colinear tr.1 tr.2 tr.3 + -- why not using ¬ tr.is_nd? · exact False · let tr_nd : Triangle_nd P := ⟨tr, h⟩ exact (if tr_nd.is_cclock then A LiesOnLeft Seg_nd.toRay ⟨tr.edge₁, tr_nd.nontriv₁⟩ ∧ A LiesOnLeft Seg_nd.toRay ⟨tr.edge₂, tr_nd.nontriv₂⟩ ∧ A LiesOnLeft Seg_nd.toRay ⟨tr.edge₃, tr_nd.nontriv₃⟩ else A LiesOnRight Seg_nd.toRay ⟨tr.edge₁, tr_nd.nontriv₁⟩ ∧ A LiesOnRight Seg_nd.toRay ⟨tr.edge₂, tr_nd.nontriv₂⟩ ∧ A LiesOnRight Seg_nd.toRay ⟨tr.edge₃, tr_nd.nontriv₃⟩) @@ -182,13 +184,48 @@ theorem angle_sum_eq_pi_of_cclock (cclock : tr_nd.is_cclock): tr_nd.angle₁.val theorem angle_sum_eq_neg_pi_of_clock (clock : ¬ tr_nd.is_cclock): tr_nd.angle₁.value + tr_nd.angle₂.value + tr_nd.angle₃.value = - π := sorry -/ -theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.length := sorry - -theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := sorry - -theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd := sorry - -theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd := sorry -- should this theorem stated as ≠, or as > ??? +theorem triangle_ineq : tr.edge₁.length + tr.edge₂.length ≥ tr.edge₃.length := by + have l₃ : tr.edge₃.length = norm (VEC tr.point₁ tr.point₂) := rfl + rw [l₃, ← neg_vec point₂ _, norm_neg, ← vec_add_vec point₂ point₃ point₁] + exact norm_add_le _ _ + +theorem trivial_of_edge_sum_eq_edge : tr.edge₁.length + tr.edge₂.length = tr.edge₃.length → ¬ tr.is_nd := by + let A := tr.point₁ + let B := tr.point₂ + let C := tr.point₃ + have l₃ : tr.edge₃.length = norm (VEC A B) := rfl + rw [l₃, ← neg_vec B _, norm_neg, ← vec_add_vec B C A] + intro eq + unfold is_nd + let g := Complex.sameRay_iff.2 ((Complex.abs_add_eq_iff).1 eq.symm) + by_cases h₁ : VEC B C = 0 + · simp only [(eq_iff_vec_eq_zero B C).2 h₁, not_not] + apply flip_colinear_fst_trd + exact triv_colinear _ _ + · by_cases h₂ : VEC C A = 0 + · simp only [(eq_iff_vec_eq_zero C A).2 h₂, not_not] + apply flip_colinear_snd_trd + exact triv_colinear _ _ + · rcases SameRay.exists_pos g h₁ h₂ with ⟨_, ⟨_, ⟨_, ⟨_, g⟩⟩⟩⟩ + rw [← neg_vec C B, ← neg_one_smul ℝ, ← mul_smul, mul_neg_one, ← eq_inv_smul_iff₀ (by linarith), ← mul_smul] at g + exact not_not.2 (perm_colinear_snd_trd_fst (colinear_of_vec_eq_smul_vec g)) + +theorem triangle_ineq' (nontriv : tr.is_nd) : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length := by + have ne : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length := by + by_contra h + let g := trivial_of_edge_sum_eq_edge tr h + tauto + by_contra h + let g := eq_of_le_of_not_lt (triangle_ineq tr) h + tauto + +/- The following two theorems are totally wrong: + +theorem nontrivial_of_edge_sum_ne_edge : tr.edge₁.length + tr.edge₂.length ≠ tr.edge₃.length → tr.is_nd := by + +theorem nontrivial_of_edge_sum_gt_edge : tr.edge₁.length + tr.edge₂.length > tr.edge₃.length → tr.is_nd := sorry + +So funny. Can you get it? -/ theorem edge_sum_eq_edge_iff_colinear : colinear tr.1 tr.2 tr.3 ↔ (tr.edge₁.length + tr.edge₂.length = tr.edge₃.length) ∨ (tr.edge₂.length + tr.edge₃.length = tr.edge₁.length) ∨ (tr.edge₃.length + tr.edge₁.length = tr.edge₂.length) := sorry /- area ≥ 0, nontrivial → >0, =0 → trivial -/ diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean index 28bc97f8..2dcf5306 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean @@ -15,7 +15,7 @@ def perm_vertices : (Triangle P) where -- We decide not to define reverse permutation of triangles, just do composition twice. -- Permuting three times returns to the original triangle. -theorem eq_self_of_perm_vertices_three_times : tr.perm_vertices.perm_vertices.perm_vertices = tr := by sorry +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. @@ -24,14 +24,16 @@ def flip_vertices : (Triangle P) where point₂ := tr.point₃ point₃ := tr.point₂ -theorem eq_self_of_flip_vertices_twice : tr.flip_vertices.flip_vertices = tr := by sorry +theorem eq_self_of_flip_vertices_twice : tr.flip_vertices.flip_vertices = tr := rfl -- Not sure this is the best theorem to p -theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr.flip_vertices.perm_vertices.perm_vertices = tr.perm_vertices.flip_vertices := by sorry +theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr.flip_vertices.perm_vertices.perm_vertices = tr.perm_vertices.flip_vertices := rfl -theorem is_inside_of_is_inside_perm_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.perm_vertices := by sorry +theorem is_inside_of_is_inside_perm_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.perm_vertices := by + sorry -theorem is_inside_of_is_inside_flip_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.flip_vertices := by sorry +theorem is_inside_of_is_inside_flip_vertices (tr : Triangle P) (p : P) (inside : p LiesInt tr) : p LiesInt tr.flip_vertices := by + sorry end Triangle @@ -41,12 +43,12 @@ def perm_vertices : (Triangle_nd P) := ⟨tr_nd.1.perm_vertices, flip_colinear_s def flip_vertices : (Triangle_nd P) := ⟨tr_nd.1.flip_vertices, flip_colinear_snd_trd.mt tr_nd.2⟩ -theorem eq_self_of_perm_vertices_three_times : tr_nd.perm_vertices.perm_vertices.perm_vertices = tr_nd := by sorry +theorem eq_self_of_perm_vertices_three_times : tr_nd.perm_vertices.perm_vertices.perm_vertices = tr_nd := rfl --exact tr_nd.1.eq_self_of_perm_vertices_three_times -theorem eq_self_of_flip_vertices_twice : tr_nd.flip_vertices.flip_vertices = tr_nd := by sorry +theorem eq_self_of_flip_vertices_twice : tr_nd.flip_vertices.flip_vertices = tr_nd := rfl -theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr_nd.flip_vertices.perm_vertices.perm_vertices = tr_nd.perm_vertices.flip_vertices := by sorry +theorem eq_flip_of_perm_twice_of_perm_flip_vertices : tr_nd.flip_vertices.perm_vertices.perm_vertices = tr_nd.perm_vertices.flip_vertices := rfl -- compatibility of permutation/flip of vertices with orientation of the triangle diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean index c4a9c007..3b773534 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Trigonometric.lean @@ -17,43 +17,18 @@ theorem cosine_rule (tr_nd : Triangle_nd P) : 2 * (tr_nd.edge₃.length * tr_nd. let A := tr_nd.1.point₁ let B := tr_nd.1.point₂ let C := tr_nd.1.point₃ - dsimp only [Seg.length] - simp - have h : ¬colinear A B C := (tr_nd).2 - have h0 : B ≠ A := by - intro k - rw [←k] at h - exact h (triv_colinear B C) - have h1 : C ≠ A := by - intro k - rw [←k] at h - have p : ¬colinear C C B := by - intro k - exact h (flip_colinear_snd_trd k) - exact p (triv_colinear C B) - have h2 : A ≠ C := Ne.symm h1 - have h3 : 2 * (Vec.norm (⟨VEC A B,(ne_iff_vec_ne_zero A B).mp h0⟩ : Vec_nd) * Vec.norm (⟨VEC A C,(ne_iff_vec_ne_zero A C).mp h1⟩ : Vec_nd) * Real.cos (Vec_nd.angle ⟨VEC A B,(ne_iff_vec_ne_zero A B).mp h0⟩ ⟨VEC A C,(ne_iff_vec_ne_zero A C).mp h1⟩)) = Seg.length (SEG A B) ^ 2 + Seg.length (SEG A C) ^ 2 - Seg.length (SEG B C) ^ 2 := cosine_rule' A B C h0 h1 - have h4 : Vec.norm (⟨VEC A C,(ne_iff_vec_ne_zero A C).mp h1⟩ : Vec_nd) = Vec.norm (⟨VEC C A,(ne_iff_vec_ne_zero C A).mp h2⟩ : Vec_nd) := by - unfold Vec.norm; simp; unfold Vec.mk_pt_pt - have l0 : A -ᵥ C = -1 * (C -ᵥ A) := by - rw [neg_one_mul] - simp - rw [l0,map_mul Complex.abs (-1) (C -ᵥ A)] - have l1: Complex.abs (-1)=1 := by simp - rw [l1,one_mul] - have h5 : Seg.length (SEG A C)=Seg.length (SEG C A) := by - unfold Seg.length - simp; unfold Vec.mk_pt_pt - have l0 : A -ᵥ C = -1 * (C -ᵥ A) := by - rw [neg_one_mul] - simp - rw [l0,map_mul Complex.abs (-1) (C -ᵥ A)] - have l1 : Complex.abs (-1) = 1 := by simp - rw [l1,one_mul] - rw [h4] at h3 - unfold Vec.norm at h3; - rw [h5] at h3; unfold Seg.length at h3; simp at h3 - exact h3 + let h₃ := cosine_rule' A B C (tr_nd.nontriv₃) (Ne.symm tr_nd.nontriv₂) + have h₄ : Vec.norm (⟨VEC A C, (ne_iff_vec_ne_zero A C).mp (Ne.symm tr_nd.nontriv₂)⟩ : Vec_nd) = Vec.norm (⟨VEC C A, (ne_iff_vec_ne_zero C A).mp (tr_nd.nontriv₂)⟩ : Vec_nd) := by + simp only [ne_eq] + rw [← neg_vec A C] + simp only [neg_Vec_norm_eq_Vec_norm] + have h₅ : Seg.length (SEG A C) = Seg.length (SEG C A) := by + unfold Seg.length Seg.toVec + rw [← neg_vec (SEG A C).target (SEG A C).source] + simp only [norm_neg, Complex.norm_eq_abs] + rw [h₄, h₅] at h₃ + simp only [ne_eq, Nat.cast_ofNat] at h₃ + exact h₃ theorem cosine_rule'' (tr_nd : Triangle_nd P) : tr_nd.edge₁.length = (tr_nd.edge₃.length ^ 2 + tr_nd.edge₂.length ^ 2 - 2 * (tr_nd.edge₃.length * tr_nd.edge₂.length * Real.cos tr_nd.angle₁.value)) ^ (1/2) := by sorry