Merge pull request #570 from Seasawher/auto-update-branch

Author: Seasawher

docs/attributes.md

@@ -1,6 +1,6 @@
 # Attributes
 
-Mathlib version: `1c119a384d559bccba90477b0ef3a645d77c5bd7`
+Mathlib version: `51192f7a45ed5916e5395b2375273662b68a910f`
 
 ## Std.Internal.tree_tac
  simp theorems used by internal DTreeMap lemmas

docs/commands.md

@@ -1,6 +1,6 @@
 # Commands
 
-Mathlib version: `1c119a384d559bccba90477b0ef3a645d77c5bd7`
+Mathlib version: `51192f7a45ed5916e5395b2375273662b68a910f`
 
 ## \#adaptation_note
 Defined in: `adaptationNoteCmd`

docs/options.md

@@ -1,6 +1,6 @@
 # Options
 
-Mathlib version: `1c119a384d559bccba90477b0ef3a645d77c5bd7`
+Mathlib version: `51192f7a45ed5916e5395b2375273662b68a910f`
 
 ## Elab.async
 type: `Bool`

docs/tactics.md

@@ -1,6 +1,6 @@
 # Tactics
 
-Mathlib version: `1c119a384d559bccba90477b0ef3a645d77c5bd7`
+Mathlib version: `51192f7a45ed5916e5395b2375273662b68a910f`
 
 ## \#adaptation_note
 Defined in: `«tactic#adaptation_note_»`
@@ -7917,7 +7917,12 @@ example : ∃ x : Nat, x = x := by use 42
 
 example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42
 
-example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
+example : Nonempty Nat := by use 5
+
+example : Nonempty (PNat ≃ Nat) := by
+  use PNat.natPred, Nat.succPNat
+  · exact PNat.succPNat_natPred
+  · intro; rfl
 ```
 
 `use! e₁, e₂, ⋯` is similar but it applies constructors everywhere rather than just for
@@ -7927,7 +7932,7 @@ leaves and nodes of the tree of constructors.
 With `use!` one can feed in each `42` one at a time:
 
 ```lean
-example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42
+example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp
 
 example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
 ```
@@ -7957,7 +7962,12 @@ example : ∃ x : Nat, x = x := by use 42
 
 example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42
 
-example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
+example : Nonempty Nat := by use 5
+
+example : Nonempty (PNat ≃ Nat) := by
+  use PNat.natPred, Nat.succPNat
+  · exact PNat.succPNat_natPred
+  · intro; rfl
 ```
 
 `use! e₁, e₂, ⋯` is similar but it applies constructors everywhere rather than just for
@@ -7967,7 +7977,7 @@ leaves and nodes of the tree of constructors.
 With `use!` one can feed in each `42` one at a time:
 
 ```lean
-example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42
+example : ∃ n : {n : Nat // n % 2 = 0}, n.val > 10 := by use! 20; simp
 
 example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
 ```

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1c119a384d559bccba90477b0ef3a645d77c5bd7",
+   "rev": "51192f7a45ed5916e5395b2375273662b68a910f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",