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

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "565ce2c97c20428195f8e7861cc0fb1f537e4d25",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "46c490a61e979ba0754250e5806bf083a9657ffc",
+   "rev": "6dcd0d943385f315b956fc76968c842a3ad4072c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

src/commands.md

@@ -500,6 +500,10 @@ For each found declaration, it prints a line
 ```
 The variant `#kerodon_tags!` also adds the theorem statement after each summary line.
 
+# \#leansearch
+Defined in: `LeanSearchClient.leansearch_search_cmd`
+
+
 # \#lint
 Defined in: `Std.Tactic.Lint.«command#lint+-*Only___»`
 
@@ -557,6 +561,10 @@ to find a collection of minimal imports that should be sufficient for `cmd` to w
 Defined in: `«command#minimize_imports»`
 
 
+# \#moogle
+Defined in: `LeanSearchClient.moogle_search_cmd`
+
+
 # \#norm_num
 Defined in: `Mathlib.Tactic.normNumCmd`
 
@@ -2126,8 +2134,6 @@ syntax ... [Lean.Parser.Command.initialize]
 
 syntax ... [Lean.Parser.Command.mixfix]
 
-syntax ... [LeanSearchClient.search_cmd]
-
 syntax ... [lemma]
 `lemma` means the same as `theorem`. It is used to denote "less important" theorems
 

src/tactics.md

@@ -23,10 +23,18 @@ These become metavariables in the output.
 Defined in: `Mathlib.Tactic.Find.«tactic#find_»`
 
 
+# \#leansearch
+Defined in: `LeanSearchClient.leansearch_search_tactic`
+
+
 # \#loogle
 Defined in: `LeanSearchClient.loogle_tactic`
 
 
+# \#moogle
+Defined in: `LeanSearchClient.moogle_search_tactic`
+
+
 # (
 Defined in: `Lean.Parser.Tactic.paren`
 
@@ -5346,51 +5354,112 @@ of hypotheses of the form `Pᵢ → Pⱼ` or `Pᵢ ↔ Pⱼ` have been introduce
 Example:
 ```lean
 example : TFAE [P, Q, R] := by
-  tfae_have 1 → 2
-  · /- proof of P → Q -/
-  tfae_have 2 → 1
-  · /- proof of Q → P -/
-  tfae_have 2 ↔ 3
-  · /- proof of Q ↔ R -/
+  tfae_have 1 → 2 := sorry /- proof of P → Q -/
+  tfae_have 2 → 1 := sorry /- proof of Q → P -/
+  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
   tfae_finish
 ```
 
 # tfae_have
 Defined in: `Mathlib.Tactic.TFAE.tfaeHave`
 
 `tfae_have` introduces hypotheses for proving goals of the form `TFAE [P₁, P₂, ...]`. Specifically,
-`tfae_have i arrow j` introduces a hypothesis of type `Pᵢ arrow Pⱼ` to the local context,
-where `arrow` can be `→`, `←`, or `↔`. Note that `i` and `j` are natural number indices (beginning
-at 1) used to specify the propositions `P₁, P₂, ...` that appear in the `TFAE` goal list. A proof
-is required afterward, typically via a tactic block.
+`tfae_have i <arrow> j := ...` introduces a hypothesis of type `Pᵢ <arrow> Pⱼ` to the local
+context, where `<arrow>` can be `→`, `←`, or `↔`. Note that `i` and `j` are natural number indices
+(beginning at 1) used to specify the propositions `P₁, P₂, ...` that appear in the goal.
 
 ```lean
 example (h : P → R) : TFAE [P, Q, R] := by
-  tfae_have 1 → 3
-  · exact h
+  tfae_have 1 → 3 := h
   ...
 ```
 The resulting context now includes `tfae_1_to_3 : P → R`.
 
-The introduced hypothesis can be given a custom name, in analogy to `have` syntax:
+Once sufficient hypotheses have been introduced by `tfae_have`, `tfae_finish` can be used to close
+the goal. For example,
+
+```lean
+example : TFAE [P, Q, R] := by
+  tfae_have 1 → 2 := sorry /- proof of P → Q -/
+  tfae_have 2 → 1 := sorry /- proof of Q → P -/
+  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
+  tfae_finish
+```
+
+All relevant features of `have` are supported by `tfae_have`, including naming, destructuring, goal
+creation, and matching. These are demonstrated below.
+
 ```lean
-tfae_have h : 2 ↔ 3
+example : TFAE [P, Q] := by
+  -- `tfae_1_to_2 : P → Q`:
+  tfae_have 1 → 2 := sorry
+  -- `hpq : P → Q`:
+  tfae_have hpq : 1 → 2 := sorry
+  -- inaccessible `h✝ : P → Q`:
+  tfae_have _ : 1 → 2 := sorry
+  -- `tfae_1_to_2 : P → Q`, and `?a` is a new goal:
+  tfae_have 1 → 2 := f ?a
+  -- create a goal of type `P → Q`:
+  tfae_have 1 → 2
+  · exact (sorry : P → Q)
+  -- match on `p : P` and prove `Q`:
+  tfae_have 1 → 2
+  | p => f p
+  -- introduces `pq : P → Q`, `qp : Q → P`:
+  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry
+  ...
 ```
 
+# tfae_have
+Defined in: `Mathlib.Tactic.TFAE.tfaeHave'`
+
+`tfae_have` introduces hypotheses for proving goals of the form `TFAE [P₁, P₂, ...]`. Specifically,
+`tfae_have i <arrow> j := ...` introduces a hypothesis of type `Pᵢ <arrow> Pⱼ` to the local
+context, where `<arrow>` can be `→`, `←`, or `↔`. Note that `i` and `j` are natural number indices
+(beginning at 1) used to specify the propositions `P₁, P₂, ...` that appear in the goal.
+
+```lean
+example (h : P → R) : TFAE [P, Q, R] := by
+  tfae_have 1 → 3 := h
+  ...
+```
+The resulting context now includes `tfae_1_to_3 : P → R`.
+
 Once sufficient hypotheses have been introduced by `tfae_have`, `tfae_finish` can be used to close
-the goal.
+the goal. For example,
 
 ```lean
 example : TFAE [P, Q, R] := by
-  tfae_have 1 → 2
-  · /- proof of P → Q -/
-  tfae_have 2 → 1
-  · /- proof of Q → P -/
-  tfae_have 2 ↔ 3
-  · /- proof of Q ↔ R -/
+  tfae_have 1 → 2 := sorry /- proof of P → Q -/
+  tfae_have 2 → 1 := sorry /- proof of Q → P -/
+  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
   tfae_finish
 ```
 
+All relevant features of `have` are supported by `tfae_have`, including naming, destructuring, goal
+creation, and matching. These are demonstrated below.
+
+```lean
+example : TFAE [P, Q] := by
+  -- `tfae_1_to_2 : P → Q`:
+  tfae_have 1 → 2 := sorry
+  -- `hpq : P → Q`:
+  tfae_have hpq : 1 → 2 := sorry
+  -- inaccessible `h✝ : P → Q`:
+  tfae_have _ : 1 → 2 := sorry
+  -- `tfae_1_to_2 : P → Q`, and `?a` is a new goal:
+  tfae_have 1 → 2 := f ?a
+  -- create a goal of type `P → Q`:
+  tfae_have 1 → 2
+  · exact (sorry : P → Q)
+  -- match on `p : P` and prove `Q`:
+  tfae_have 1 → 2
+  | p => f p
+  -- introduces `pq : P → Q`, `qp : Q → P`:
+  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry
+  ...
+```
+
 # toFinite_tac
 Defined in: `Set.tacticToFinite_tac`
 
@@ -5750,5 +5819,3 @@ syntax ... [Lean.Parser.Tactic.unknown]
 syntax ... [Lean.cdot]
 `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails.
 
-syntax ... [LeanSearchClient.search_tactic]
-