Update to lean v4.3.0

main
Joshua Potter 2023-12-14 12:49:31 -07:00
parent cdba12f161
commit 4f8c3383f1
14 changed files with 101 additions and 110 deletions

1
.gitignore vendored
View File

@ -4,6 +4,7 @@ lakefile.olean
lake-packages lake-packages
_target _target
leanpkg.path leanpkg.path
.lake/
# TeX # TeX
*.aux *.aux

View File

@ -50,7 +50,7 @@ theorem exercise_4c (x y : )
: ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by : ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by
have hx : x = Int.floor x + Int.fract x := Eq.symm (add_eq_of_eq_sub' rfl) have hx : x = Int.floor x + Int.fract x := Eq.symm (add_eq_of_eq_sub' rfl)
have hy : y = Int.floor y + Int.fract y := Eq.symm (add_eq_of_eq_sub' rfl) have hy : y = Int.floor y + Int.fract y := Eq.symm (add_eq_of_eq_sub' rfl)
by_cases Int.fract x + Int.fract y < 1 by_cases h : Int.fract x + Int.fract y < 1
· refine Or.inl ?_ · refine Or.inl ?_
rw [Int.floor_eq_iff] rw [Int.floor_eq_iff]
simp only [Int.cast_add] simp only [Int.cast_add]

View File

@ -1,5 +1,5 @@
import Common.Set import Common.Set
import Mathlib.Data.Real.Basic import Mathlib.Data.Real.Archimedean
/-! # Apostol.Chapter_I_03 /-! # Apostol.Chapter_I_03

View File

@ -481,7 +481,7 @@ theorem exercise_1_2_2b_iii {k : } (h : Odd k)
exact absurd hr hk exact absurd hr hk
unfold σ unfold σ
rw [hn₁] rw [hn₁]
simp only [Nat.add_eq, add_zero, not_forall, exists_prop, and_true] simp only [Nat.add_eq, add_zero, imp_false, not_not]
exact exercise_1_2_2b_i False Q hn₂ exact exercise_1_2_2b_i False Q hn₂
end Exercise_1_2_2 end Exercise_1_2_2

View File

@ -616,7 +616,7 @@ lemma right_diff_eq_insert_one_three : A \ (B \ C) = {1, 3} := by
rw [hy] at hz rw [hy] at hz
unfold Membership.mem Set.instMembershipSet Set.Mem at hz unfold Membership.mem Set.instMembershipSet Set.Mem at hz
unfold singleton Set.instSingletonSet Set.singleton setOf at hz unfold singleton Set.instSingletonSet Set.singleton setOf at hz
simp only at hz simp at hz
· intro hy · intro hy
refine ⟨Or.inr (Or.inr hy), ?_⟩ refine ⟨Or.inr (Or.inr hy), ?_⟩
intro hz intro hz

View File

@ -542,7 +542,7 @@ theorem exercise_3_1 {x y z u v w : }
· rw [hx, hy, hz, hu, hv, hw] · rw [hx, hy, hz, hu, hv, hw]
simp simp
· rw [hy, hv] · rw [hy, hv]
simp only simp
/-- ### Exercise 3.2a /-- ### Exercise 3.2a

View File

@ -702,7 +702,7 @@ theorem exercise_4_17 (m n p : )
| zero => calc m ^ (n + 0) | zero => calc m ^ (n + 0)
_ = m ^ n := rfl _ = m ^ n := rfl
_ = m ^ n * 1 := by rw [right_mul_id] _ = m ^ n * 1 := by rw [right_mul_id]
_ = m ^ n * m ^ 0 := rfl _ = m ^ n * m ^ 0 := by rfl
| succ p ih => calc m ^ (n + p.succ) | succ p ih => calc m ^ (n + p.succ)
_ = m ^ (n + p).succ := rfl _ = m ^ (n + p).succ := rfl
_ = m ^ (n + p) * m := rfl _ = m ^ (n + p) * m := rfl

View File

@ -512,7 +512,7 @@ theorem corollary_6d_b
] ]
refine ⟨1, ?_⟩ refine ⟨1, ?_⟩
intro x nx intro x nx
simp only [mul_eq_one, false_and] at nx simp only [mul_eq_one, OfNat.ofNat_ne_one, false_and] at nx
/-- ### Corollary 6E /-- ### Corollary 6E
@ -992,7 +992,7 @@ lemma sdiff_size_aux [DecidableEq α] [Nonempty α]
simp only [Set.diff_empty] simp only [Set.diff_empty]
exact hA exact hA
rw [this] rw [this]
refine ⟨trivial, hB', Set.equinumerous_emptyset_emptyset⟩ refine ⟨by simp, hB', Set.equinumerous_emptyset_emptyset⟩
| succ m ih => | succ m ih =>
/- /-
> #### (ii) > #### (ii)

View File

@ -162,7 +162,7 @@ theorem length_zipWith_self_tail_eq_length_sub_one
rw [length_zipWith] rw [length_zipWith]
simp only [length_cons, ge_iff_le, min_eq_right_iff] simp only [length_cons, ge_iff_le, min_eq_right_iff]
show length as ≤ length as + 1 show length as ≤ length as + 1
simp only [le_add_iff_nonneg_right] simp only [le_add_iff_nonneg_right, zero_le]
/-- /--
The output `List` of a `zipWith` is nonempty **iff** both of its inputs are The output `List` of a `zipWith` is nonempty **iff** both of its inputs are

View File

@ -9,23 +9,4 @@ If `n < m⁺`, then `n < m` or `n = m`.
theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m n = m := theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m n = m :=
lt_or_eq_of_le (lt_succ.mp h) lt_or_eq_of_le (lt_succ.mp h)
/--
The following cancellation law holds for `m`, `n`, and `p` in `ω`:
```
m ⬝ p = n ⬝ p ∧ p ≠ 0 → m = n
```
-/
theorem mul_right_cancel (m n p : ) (hp : 0 < p) : m * p = n * p → m = n := by
intro hmn
match @trichotomous LT.lt _ m n with
| Or.inl h =>
have : m * p < n * p := Nat.mul_lt_mul_of_pos_right h hp
rw [hmn] at this
simp at this
| Or.inr (Or.inl h) => exact h
| Or.inr (Or.inr h) =>
have : n * p < m * p := Nat.mul_lt_mul_of_pos_right h hp
rw [hmn] at this
simp at this
end Nat end Nat

View File

@ -1,6 +1,5 @@
import Mathlib.Algebra.BigOperators.Basic import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic import Mathlib.Data.Real.Archimedean
import Mathlib.Data.Finset.Basic
/-! # Common.Real.Floor /-! # Common.Real.Floor

View File

@ -1,76 +1,86 @@
{"version": 6, {"version": 7,
"packagesDir": "lake-packages", "packagesDir": ".lake/packages",
"packages": "packages":
[{"git": [{"url": "https://github.com/mhuisi/lean4-cli",
{"url": "https://github.com/mhuisi/lean4-cli", "type": "git",
"subDir?": null, "subDir": null,
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
"opts": {},
"name": "Cli", "name": "Cli",
"inputRev?": "nightly", "manifestFile": "lake-manifest.json",
"inherited": false}}, "inputRev": "nightly",
{"git": "inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/xubaiw/CMark.lean", {"url": "https://github.com/xubaiw/CMark.lean",
"subDir?": null, "type": "git",
"subDir": null,
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
"opts": {},
"name": "CMark", "name": "CMark",
"inputRev?": "main", "manifestFile": "lake-manifest.json",
"inherited": false}}, "inputRev": "main",
{"git": "inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/fgdorais/lean4-unicode-basic", {"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null, "type": "git",
"rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71", "subDir": null,
"opts": {}, "rev": "dc62b29a26fcc3da545472ab8ad2c98ef3433634",
"name": "UnicodeBasic", "name": "UnicodeBasic",
"inputRev?": "main", "manifestFile": "lake-manifest.json",
"inherited": false}}, "inputRev": "main",
{"git": "inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/hargonix/LeanInk", {"url": "https://github.com/hargonix/LeanInk",
"subDir?": null, "type": "git",
"subDir": null,
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
"opts": {},
"name": "leanInk", "name": "leanInk",
"inputRev?": "doc-gen", "manifestFile": "lake-manifest.json",
"inherited": false}}, "inputRev": "doc-gen",
{"git": "inherited": false,
{"url": "https://github.com/leanprover-community/mathlib4.git", "configFile": "lakefile.lean"},
"subDir?": null,
"rev": "c97b9b00802c2ed343d9ac73e59be287428dbcf0",
"opts": {},
"name": "mathlib",
"inputRev?": "master",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4.git", {"url": "https://github.com/leanprover/std4.git",
"subDir?": null, "type": "git",
"rev": "87b0742b01e45c6cc53cd3043fe3c7cdbf87a56f", "subDir": null,
"opts": {}, "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
"name": "std", "name": "std",
"inputRev?": "main", "manifestFile": "lake-manifest.json",
"inherited": false}}, "inputRev": "v4.3.0",
{"git": "inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4", {"url": "https://github.com/leanprover-community/quote4",
"subDir?": null, "type": "git",
"rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39", "subDir": null,
"opts": {}, "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
"name": "Qq", "name": "Qq",
"inputRev?": "master", "manifestFile": "lake-manifest.json",
"inherited": true}}, "inputRev": "master",
{"git": "inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop", {"url": "https://github.com/leanprover-community/aesop",
"subDir?": null, "type": "git",
"rev": "cb87803274405db79ec578fc07c4730c093efb90", "subDir": null,
"opts": {}, "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
"name": "aesop", "name": "aesop",
"inputRev?": "master", "manifestFile": "lake-manifest.json",
"inherited": true}}, "inputRev": "master",
{"git": "inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/ProofWidgets4", {"url": "https://github.com/leanprover-community/ProofWidgets4",
"subDir?": null, "type": "git",
"rev": "f1a5c7808b001305ba07d8626f45ee054282f589", "subDir": null,
"opts": {}, "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
"name": "proofwidgets", "name": "proofwidgets",
"inputRev?": "v0.0.21", "manifestFile": "lake-manifest.json",
"inherited": true}}], "inputRev": "v0.0.23",
"name": "bookshelf"} "inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.3.0",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "bookshelf",
"lakeDir": ".lake"}

View File

@ -22,10 +22,10 @@ require leanInk from git
"doc-gen" "doc-gen"
require mathlib from git require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "https://github.com/leanprover-community/mathlib4.git" @
"master" "v4.3.0"
require std from git require std from git
"https://github.com/leanprover/std4.git" @ "https://github.com/leanprover/std4.git" @
"main" "v4.3.0"
-- ======================================== -- ========================================
-- Documentation Generator -- Documentation Generator

View File

@ -1 +1 @@
leanprover/lean4:v4.3.0-rc1 leanprover/lean4:v4.3.0