rc2

Author: wwylele

Poncelet/Euclidean.lean

@@ -328,7 +328,6 @@ theorem inner_yDir_center_o : ⟪cf.o.center -ᵥ cf.i.center, cf.yDir -ᵥ cf.i
   use 1
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 noncomputable
 def toConfig : Config ℝ where
   u := dist cf.o.center cf.i.center / cf.i.radius
@@ -349,7 +348,6 @@ def toConfig : Config ℝ where
     apply le_of_lt
     exact radius_lt_of_inside cf.i cf.o cf.i_pos cf.inside
 
-set_option backward.isDefEq.respectTransparency false in
 theorem u_add_r_sq : (cf.toConfig.u + cf.toConfig.r) ^ 2 ≠ 1 := by
   apply ne_of_gt
   unfold toConfig
@@ -362,7 +360,6 @@ theorem u_add_r_sq : (cf.toConfig.u + cf.toConfig.r) ^ 2 ≠ 1 := by
   rw [abs_of_nonneg (by simpa using cf.o_pos.le)]
   exact radius_lt_of_inside cf.i cf.o cf.i_pos cf.inside
 
-set_option backward.isDefEq.respectTransparency false in
 theorem u_sub_r_sq : (cf.toConfig.u - cf.toConfig.r) ^ 2 ≠ 1 := by
   apply ne_of_gt
   unfold toConfig
@@ -459,7 +456,7 @@ theorem dirVec_ne_zero' {p : AffineSubspace ℝ P} (hp : Module.finrank ℝ p.di
 set_option backward.isDefEq.respectTransparency false in
 theorem eq_span_dirVec {p : AffineSubspace ℝ P} (hp : Module.finrank ℝ p.direction = 1) :
     p.direction = Submodule.span ℝ {(dirVec hp).val} := by
-  rw [finrank_eq_one_iff_of_nonzero _ (dirVec_ne_zero hp)] at hp
+  rw [finrank_eq_one_iff_of_nonzero (dirVec hp) (dirVec_ne_zero hp) (K := ℝ)] at hp
   rw [← Submodule.map_subtype_span_singleton, hp]
   simp
 

Poncelet/Transfer.lean

@@ -365,7 +365,7 @@ theorem fChord_w [DecidableEq K] [CharZero K] :
   grind
 
 @[simp]
-theorem fPoint_w [DecidableEq K] [CharZero K] : fPoint cf (w cf) =
+theorem fPoint_w [CharZero K] : fPoint cf (w cf) =
     P2.mk ![(cf.u - cf.r) * (cf.u + cf.r) ^ 2 + 2 * cf.r, -2 * cf.k * cf.r, (cf.u + cf.r) ^ 2]
     (by
       by_cases h : cf.u + cf.r = 0
@@ -435,7 +435,7 @@ theorem fChord_neg_w [DecidableEq K] [CharZero K] :
   · ring
 
 @[simp]
-theorem fPoint_neg_w [DecidableEq K] [CharZero K] : fPoint cf (-w cf) =
+theorem fPoint_neg_w [CharZero K] : fPoint cf (-w cf) =
     P2.mk ![(cf.u - cf.r) * (cf.u + cf.r) ^ 2 + 2 * cf.r, 2 * cf.k * cf.r, (cf.u + cf.r) ^ 2]
     (by
       by_cases h : cf.u + cf.r = 0

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "13ecfbb8be8bbea477028cd3dcf5eae0c92e47b1",
+   "rev": "f178e492e7f345d7be5a57d2178e95f7a3cc070b",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,12 +25,22 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1aca177ec824a36582f55fb0396d8f83be20da77",
+   "rev": "2d6247196524215d9beb18820e09d6bd5537bf8e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/david-christiansen/leansqlite",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "739abe6c8ae0602d6ce56461d33f3e49837c9b70",
+   "name": "leansqlite",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
@@ -74,8 +84,8 @@
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "a8191ec244102f576a8cd93399cdd8cc489e47cd",
+   "scope": "",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7ccd5e026eb2b3581915ff3f0d1cd918e18c2ab9",
+   "rev": "17d5e44a634099607fae899127736377c3517f95",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,17 +115,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "06c949a3f4a3b2eb0bd8601e31269b9f4f820aa6",
+   "rev": "b5e00ab2b8adfc9dfc9335ca3dadca7caec37629",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.88",
+   "inputRev": "v0.0.89",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb165126bfb2988738792c9ae37e09d58e2fec83",
+   "rev": "de5caa559acfd0a1577b3bc49c33887a91c4792e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -125,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "90217e10b2db6c6c445d30faae7fea453d9782c0",
+   "rev": "db277098a6c4ae41e0aa9938382a98f14af9da38",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -135,7 +145,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "965500ff9171556698ec2714b936739d5da438c2",
+   "rev": "07be181c4f3c157e385eaa0259ac248bc3eb3626",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc1
+leanprover/lean4:v4.29.0-rc2