Merge pull request #110 from alissa-tung/master

chore: bump ver

.gitignore

@@ -1,2 +1,3 @@
 /build
 /lake-packages/*
+*.olean

EuclideanGeometry/Foundation/Axiom/Linear/Line.lean

@@ -9,19 +9,19 @@ section setoid
 
 variable {P : Type _} [EuclideanPlane P]
 
-def same_extn_line : Ray P → Ray P → Prop := fun r₁ r₂ => r₁.toProj = r₂.toProj ∧ (r₂.source LiesOn r₁ ∨ r₂.source LiesOn r₁.reverse) 
+def same_extn_line : Ray P → Ray P → Prop := fun r₁ r₂ => r₁.toProj = r₂.toProj ∧ (r₂.source LiesOn r₁ ∨ r₂.source LiesOn r₁.reverse)
 
 namespace same_extn_line
 
 theorem dir_eq_or_eq_neg {x y : Ray P} (h : same_extn_line x y) : (x.toDir = y.toDir ∨ x.toDir = - y.toDir) := (Dir.eq_toProj_iff _ _).mp h.1
 
-protected theorem refl (x : Ray P) : same_extn_line x x := ⟨rfl, Or.inl (Ray.source_lies_on x)⟩  
+protected theorem refl (x : Ray P) : same_extn_line x x := ⟨rfl, Or.inl (Ray.source_lies_on x)⟩
 
 protected theorem symm {x y : Ray P} (h : same_extn_line x y) : same_extn_line y x := by
   constructor
-  · exact h.1.symm 
+  · exact h.1.symm
   · have g := dir_eq_or_eq_neg h
-    cases g with 
+    cases g with
     | inl h₁ => sorry
     | inr h₂ => sorry
 
@@ -39,21 +39,21 @@ instance : Setoid (Ray P) := same_extn_line.setoid
 
 end same_extn_line
 
-theorem same_extn_line_of_PM (A : P) (x y : Dir) (h : PM x y) : same_extn_line (Ray.mk A x) (Ray.mk A y) := sorry 
+theorem same_extn_line_of_PM (A : P) (x y : Dir) (h : PM x y) : same_extn_line (Ray.mk A x) (Ray.mk A y) := sorry
 
 theorem same_extn_line.eq_carrier_union_rev_carrier (ray ray' : Ray P) (h : same_extn_line ray ray') : ray.carrier ∪ ray.reverse.carrier = ray'.carrier ∪ ray'.reverse.carrier := sorry
 
 end setoid
 
 def Line (P : Type _) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _)
 
-variable  {P : Type _} [EuclideanPlane P] 
+variable  {P : Type _} [EuclideanPlane P]
 
 section make
 
 namespace Line
 
--- define a line from two points 
+-- define a line from two points
 def mk_pt_pt (A B : P) (h : B ≠ A) : Line P := ⟦RAY A B h⟧
 
 -- define a line from a point and a proj
@@ -67,15 +67,15 @@ def mk_pt_vec_nd (A : P) (vec_nd : Vec_nd) : Line P := mk_pt_proj A vec_nd.toPro
 
 end Line
 
-scoped notation "LIN" => Line.mk_pt_pt 
+scoped notation "LIN" => Line.mk_pt_pt
 
 end make
 
 section coercion
 
 def Line.toProj (l : Line P) : Proj := Quotient.lift (fun ray : Ray P => ray.toProj) (fun _ _ h => And.left h) l
 
-def Ray.toLine (ray : Ray P) : Line P := ⟦ray⟧ 
+def Ray.toLine (ray : Ray P) : Line P := ⟦ray⟧
 
 def Seg_nd.toLine (seg_nd : Seg_nd P) : Line P := ⟦seg_nd.toRay⟧
 
@@ -98,19 +98,19 @@ instance : Carrier P (Line P) where
 theorem linear (l : Line P) {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l) (h₃ : C LiesOn l) : colinear A B C := by
   unfold Line at l
   revert l
-  rw [forall_quotient_iff (p := fun k : Line P => A LiesOn k → B LiesOn k → C LiesOn k → colinear A B C)]
+  rw [Quotient.forall (p := fun k : Line P => A LiesOn k → B LiesOn k → C LiesOn k → colinear A B C)]
   unfold lies_on instCarrierLine Carrier.carrier Line.carrier at *
   simp only
   intro ray a b c
   rw [@Quotient.lift_mk _ _ same_extn_line.setoid _ _ _] at *
   cases a with
   | inl a =>
     cases b with
-    | inl b => 
+    | inl b =>
       cases c with
-      | inl c => 
+      | inl c =>
         exact Ray.colinear_of_lies_on a b c
-      | inr c => 
+      | inr c =>
         let ray' := Ray.mk C ray.toDir
         have a' : A ∈ ray'.carrier := lies_on_pt_toDir_of_pt_lies_on_rev a c
         have b' : B ∈ ray'.carrier := lies_on_pt_toDir_of_pt_lies_on_rev b c
@@ -119,9 +119,9 @@ theorem linear (l : Line P) {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l)
       cases c with
       | inl c => sorry
       | inr c => sorry
-  | inr a => 
+  | inr a =>
     cases b with
-    | inl b => 
+    | inl b =>
       cases c with
       | inl c => sorry
       | inr c => sorry

EuclideanGeometry/Foundation/Axiom/Linear/Line_ex.lean

@@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray_ex
 noncomputable section
 namespace EuclidGeom
 
-variable {P : Type _} [EuclideanPlane P] 
+variable {P : Type _} [EuclideanPlane P]
 
 section compatibility
 -- `eq_toProj theorems should be relocate to file parallel using parallel`.
@@ -18,7 +18,7 @@ theorem fst_pt_lies_on_line_of_pt_pt {A B : P} (h : B ≠ A) : A LiesOn LIN A B
 
 theorem snd_pt_lies_on_line_of_pt_pt {A B : P} (h : B ≠ A) : B LiesOn LIN A B h := sorry
 
--- The first point and the second point in Line.mk_pt_pt LiesOn the line it make. 
+-- The first point and the second point in Line.mk_pt_pt LiesOn the line it make.
 
 theorem pt_lies_on_line_of_pt_pt_of_ne {A B : P} (h: B ≠ A) : A LiesOn LIN A B h ∧ B LiesOn LIN A B h := by
   constructor
@@ -30,7 +30,7 @@ theorem pt_lies_on_line_of_pt_pt_of_ne {A B : P} (h: B ≠ A) : A LiesOn LIN A B
 theorem eq_line_of_pt_pt_of_ne {A B : P} {l : Line P} (h : B ≠ A) (ha : A LiesOn l) (hb : B LiesOn l) : LIN A B h = l := by
   revert l
   unfold Line
-  rw [forall_quotient_iff (r := same_extn_line.setoid)]
+  rw [Quotient.forall (s := same_extn_line.setoid)]
   intro ray ha hb
   unfold Line.mk_pt_pt
   rw [Quotient.eq]
@@ -83,9 +83,9 @@ theorem lies_on_iff_lies_on_iff_line_eq_line (l₁ l₂ : Line P) : (∀ A : P,
   · intro hiff
     revert l₁ l₂
     unfold Line
-    rw [forall_quotient_iff (r := same_extn_line.setoid)]
+    rw [Quotient.forall (s := same_extn_line.setoid)]
     intro r₁
-    rw [forall_quotient_iff (r := same_extn_line.setoid)]
+    rw [Quotient.forall (s := same_extn_line.setoid)]
     intro r₂
     intro h
     unfold lies_on Line.instCarrierLine Carrier.carrier Line.carrier at h
@@ -172,12 +172,12 @@ theorem lies_on_of_Seg_nd_toProj_eq_toProj {A B : P} {l : Line P} (ha : A LiesOn
   let g := line_toProj_eq_seg_nd_toProj_of_lies_on ha h.1 h.2
   rw [← hp] at g
   unfold Seg_nd.toProj Seg_nd.toVec_nd at g
-  simp only [ne_eq] at g 
+  simp only [ne_eq] at g
   have c : colinear A X B := by
     rw [← iff_true (colinear A X B), ← eq_iff_iff]
     unfold colinear colinear_of_nd
     simp [g]
-    by_cases (B = X ∨ A = B ∨ X = A) 
+    by_cases (B = X ∨ A = B ∨ X = A)
     · simp only [h, dite_eq_ite]
     · simp only [h, dite_eq_ite]
   exact (lies_on_iff_colinear_of_ne_lies_on_lies_on h.2 ha h.1 B).2 c

lake-manifest.json

@@ -2,13 +2,13 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "rev": "e95989a3696b4c379c07e3a2346d487094b96e17",
     "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.13",
-    "inherited": true}},
+    "name": "mathlib",
+    "inputRev?": null,
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -17,14 +17,6 @@
     "name": "Cli",
     "inputRev?": "nightly",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/mathlib4.git",
-    "subDir?": null,
-    "rev": "7d308680dc444730e84a86c72357ad9a7aea9c4b",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": null,
-    "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
@@ -44,8 +36,16 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
+    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.16",
     "inherited": true}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.1.0-rc1