Update dependences to match mathlib

MIL/C03_Logic/S03_Negation.lean

@@ -243,7 +243,6 @@ example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
   intro x Px
   apply h
   use x
-  exact Px
 
 example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
   rintro ⟨x, Px⟩
@@ -336,7 +335,6 @@ example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
   intro h''
   apply h'
   use x
-  exact h''
 
 /- TEXT:
 .. index:: push_neg, tactics ; push_neg

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -307,7 +307,6 @@ example : s \ t ∪ t = s ∪ t := by
   rintro (xs | xt)
   · left
     use xs
-    exact h
   right; exact xt
 
 example : s \ t ∪ t \ s = (s ∪ t) \ (s ∩ t) := by
@@ -488,7 +487,6 @@ example (h₀ : ∀ x ∈ s, ¬Even x) (h₁ : ∀ x ∈ s, Prime x) : ∀ x ∈
 example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ s, Prime x := by
   rcases h with ⟨x, xs, _, prime_x⟩
   use x, xs
-  exact prime_x
 -- QUOTE.
 
 /- TEXT:
@@ -520,7 +518,6 @@ example (h₀ : ∀ x ∈ t, ¬Even x) (h₁ : ∀ x ∈ t, Prime x) : ∀ x ∈
 example (h : ∃ x ∈ s, ¬Even x ∧ Prime x) : ∃ x ∈ t, Prime x := by
   rcases h with ⟨x, xs, _, px⟩
   use x, ssubt xs
-  exact px
 
 end
 
@@ -663,7 +660,6 @@ example : (⋃ p ∈ primes, { x | x ≤ p }) = univ := by
   simp
   rcases Nat.exists_infinite_primes x with ⟨p, primep, pge⟩
   use p, pge
-  exact primep
 
 -- BOTH:
 end

MIL/C04_Sets_and_Functions/S02_Functions.lean

@@ -183,7 +183,6 @@ example (h : Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
 example (h : s ⊆ t) : f '' s ⊆ f '' t := by
   rintro y ⟨x, xs, fxeq⟩
   use x, h xs
-  exact fxeq
 
 example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by
   intro x; apply h
@@ -260,7 +259,6 @@ example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
   constructor
   · rintro ⟨x, ⟨i, xAi⟩, fxeq⟩
     use i, x
-    exact ⟨xAi, fxeq⟩
   rintro ⟨i, x, xAi, fxeq⟩
   exact ⟨x, ⟨i, xAi⟩, fxeq⟩
 
@@ -298,7 +296,6 @@ example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
   constructor
   · rintro ⟨x, ⟨i, xAi⟩, fxeq⟩
     use i, x
-    exact ⟨xAi, fxeq⟩
   rintro ⟨i, x, xAi, fxeq⟩
   exact ⟨x, ⟨i, xAi⟩, fxeq⟩
 

MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

@@ -120,7 +120,6 @@ theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p
   have mgt2 : 2 ≤ m := two_le this mne1
   by_cases mp : m.Prime
   · use m, mp
-    exact mdvdn
   . rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
     use p, pp
     apply pdvd.trans mdvdn
@@ -535,7 +534,6 @@ theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
     ∃ p : Nat, p.Prime ∧ p ∣ n ∧ p % 4 = 3 := by
   by_cases np : n.Prime
   · use n
-    exact ⟨np, dvd_rfl, h⟩
   induction' n using Nat.strong_induction_on with n ih
   dsimp at ih
   rw [Nat.prime_def_lt] at np
@@ -557,14 +555,12 @@ theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
 SOLUTIONS: -/
   · by_cases mp : m.Prime
     · use m
-      exact ⟨mp, mdvdn, h1⟩
     rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩
     use p
     exact ⟨pp, pdvd.trans mdvdn, p4eq⟩
   obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn
   by_cases nmp : (n / m).Prime
   · use n / m
-    exact ⟨nmp, nmdvdn, h1⟩
   rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩
   use p
   exact ⟨pp, pdvd.trans nmdvdn, p4eq⟩

lake-manifest.json

@@ -4,9 +4,9 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
     "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
+    "inputRev?": "v0.0.13"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -16,24 +16,24 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "758b7d6b19adfc8a0d12be3eafb48507e2e859e5",
+    "rev": "d567f7cfc07d1a56eabb808ca3be77113520505b",
     "name": "mathlib",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "ae84bd82cca324dc958583d6f1ae08429877dcb0",
+    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+    "rev": "d13a9666e6f430b940ef8d092f1219e964b52a09",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8",
     "name": "std",
     "inputRev?": "main"}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12
+leanprover/lean4:nightly-2023-08-05