chore: bump lean 06-07 (#4849)

Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

@@ -115,7 +115,7 @@ sequence in a neighborhood of `x`. -/
 theorem uniformCauchySeqOnFilter_of_fderiv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
     (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
     (hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOnFilter f l (𝓝 x) := by
-  let : NormedSpace ℝ E; exact NormedSpace.restrictScalars ℝ 𝕜 _
+  letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
   rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hf' ⊢
   suffices
     TendstoUniformlyOnFilter (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
@@ -179,7 +179,7 @@ convergence. See `cauchy_map_of_uniformCauchySeqOn_fderiv`.
 theorem uniformCauchySeqOn_ball_of_fderiv {r : ℝ} (hf' : UniformCauchySeqOn f' l (Metric.ball x r))
     (hf : ∀ n : ι, ∀ y : E, y ∈ Metric.ball x r → HasFDerivAt (f n) (f' n y) y)
     (hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOn f l (Metric.ball x r) := by
-  let : NormedSpace ℝ E; exact NormedSpace.restrictScalars ℝ 𝕜 _
+  letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
   have : NeBot l := (cauchy_map_iff.1 hfg).1
   rcases le_or_lt r 0 with (hr | hr)
   · simp only [Metric.ball_eq_empty.2 hr, UniformCauchySeqOn, Set.mem_empty_iff_false,

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -201,34 +201,23 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h
 /-- Characterization of minimizers for the projection on a convex set in a real inner product
 space. -/
 theorem norm_eq_iInf_iff_real_inner_le_zero {K : Set F} (h : Convex ℝ K) {u : F} {v : F}
-    (hv : v ∈ K) : (‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 :=
-  Iff.intro
-    (by
-      intro eq w hw
-      let δ := ⨅ w : K, ‖u - w‖
-      let p := ⟪u - v, w - v⟫_ℝ
-      let q := ‖w - v‖ ^ 2
-      letI : Nonempty K := ⟨⟨v, hv⟩⟩
-      have : 0 ≤ δ
-      apply le_ciInf
-      intro
-      exact norm_nonneg _
-      have δ_le : ∀ w : K, δ ≤ ‖u - w‖
-      intro w
-      apply ciInf_le
-      use (0 : ℝ)
-      rintro _ ⟨_, rfl⟩
-      exact norm_nonneg _
-      have δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖ := fun w hw => δ_le ⟨w, hw⟩
-      have : ∀ θ : ℝ, 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
-      intro θ hθ₁ hθ₂
+    (hv : v ∈ K) : (‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
+  letI : Nonempty K := ⟨⟨v, hv⟩⟩
+  constructor
+  · intro eq w hw
+    let δ := ⨅ w : K, ‖u - w‖
+    let p := ⟪u - v, w - v⟫_ℝ
+    let q := ‖w - v‖ ^ 2
+    have δ_le (w : K) : δ ≤ ‖u - w‖ := ciInf_le ⟨0, fun _ ⟨_, h⟩ => h ▸ norm_nonneg _⟩ _
+    have δ_le' (w) (hw : w ∈ K) : δ ≤ ‖u - w‖ := δ_le ⟨w, hw⟩
+    have (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1) : 2 * p ≤ θ * q := by
       have : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 :=
-        calc
-          ‖u - v‖ ^ 2 ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 := by
+        calc ‖u - v‖ ^ 2
+          _ ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 := by
             simp only [sq]; apply mul_self_le_mul_self (norm_nonneg _)
             rw [eq]; apply δ_le'
             apply h hw hv
-            exacts[le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _]
+            exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _]
           _ = ‖u - v - θ • (w - v)‖ ^ 2 := by
             have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) := by
               rw [smul_sub, sub_smul, one_smul]
@@ -239,13 +228,13 @@ theorem norm_eq_iInf_iff_real_inner_le_zero {K : Set F} (h : Convex ℝ K) {u :
             simp only [sq]
             show
               ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) +
-                  absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
-                ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
+                absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
+              ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
             rw [abs_of_pos hθ₁]; ring
       have eq₁ :
         ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
-          ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)) :=
-        by abel
+          ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)) := by
+        abel
       rw [eq₁, le_add_iff_nonneg_right] at this
       have eq₂ :
         θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) =
@@ -254,57 +243,47 @@ theorem norm_eq_iInf_iff_real_inner_le_zero {K : Set F} (h : Convex ℝ K) {u :
       rw [eq₂] at this
       have := le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)
       exact this
-      by_cases hq : q = 0
-      · rw [hq] at this
-        have : p ≤ 0
+    by_cases hq : q = 0
+    · rw [hq] at this
+      have : p ≤ 0 := by
         have := this (1 : ℝ) (by norm_num) (by norm_num)
         linarith
-        exact this
-      · have q_pos : 0 < q
-        apply lt_of_le_of_ne
-        exact sq_nonneg _
-        intro h
-        exact hq h.symm
-        by_contra hp
-        rw [not_le] at hp
-        let θ := min (1 : ℝ) (p / q)
-        have eq₁ : θ * q ≤ p :=
-          calc
-            θ * q ≤ p / q * q := mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
-            _ = p := div_mul_cancel _ hq
-
-        have : 2 * p ≤ p :=
-          calc
-            2 * p ≤ θ * q := by
-              refine' this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num)
-            _ ≤ p := eq₁
-
-        linarith)
-    (by
-      intro h
-      letI : Nonempty K := ⟨⟨v, hv⟩⟩
-      apply le_antisymm
-      · apply le_ciInf
-        intro w
-        apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
-        have := h w w.2
+      exact this
+    · have q_pos : 0 < q := lt_of_le_of_ne (sq_nonneg _) fun h ↦ hq h.symm
+      by_contra hp
+      rw [not_le] at hp
+      let θ := min (1 : ℝ) (p / q)
+      have eq₁ : θ * q ≤ p :=
         calc
-          ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) ((w : F) - v) := by linarith
-          _ ≤ ‖u - v‖ ^ 2 - 2 * inner (u - v) ((w : F) - v) + ‖(w : F) - v‖ ^ 2 := by
-            rw [sq]
-            refine' le_add_of_nonneg_right _
-            exact sq_nonneg _
-          _ = ‖u - v - (w - v)‖ ^ 2 := (@norm_sub_sq ℝ _ _ _ _ _ _).symm
-          _ = ‖u - w‖ * ‖u - w‖ := by
-            have : u - v - (w - v) = u - w
-            abel
-            rw [this, sq]
-
-      · show (⨅ w : K, ‖u - w‖) ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
-        apply ciInf_le
-        use 0
-        rintro y ⟨z, rfl⟩
-        exact norm_nonneg _)
+          θ * q ≤ p / q * q := mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
+          _ = p := div_mul_cancel _ hq
+      have : 2 * p ≤ p :=
+        calc
+          2 * p ≤ θ * q := by
+            refine' this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num)
+          _ ≤ p := eq₁
+      linarith
+  · intro h
+    apply le_antisymm
+    · apply le_ciInf
+      intro w
+      apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
+      have := h w w.2
+      calc
+        ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) ((w : F) - v) := by linarith
+        _ ≤ ‖u - v‖ ^ 2 - 2 * inner (u - v) ((w : F) - v) + ‖(w : F) - v‖ ^ 2 := by
+          rw [sq]
+          refine' le_add_of_nonneg_right _
+          exact sq_nonneg _
+        _ = ‖u - v - (w - v)‖ ^ 2 := (@norm_sub_sq ℝ _ _ _ _ _ _).symm
+        _ = ‖u - w‖ * ‖u - w‖ := by
+          have : u - v - (w - v) = u - w := by abel
+          rw [this, sq]
+    · show (⨅ w : K, ‖u - w‖) ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
+      apply ciInf_le
+      use 0
+      rintro y ⟨z, rfl⟩
+      exact norm_nonneg _
 #align norm_eq_infi_iff_real_inner_le_zero norm_eq_iInf_iff_real_inner_le_zero
 
 variable (K : Submodule 𝕜 E)

Mathlib/Analysis/NormedSpace/Multilinear.lean

@@ -1655,7 +1655,6 @@ theorem ContinuousMultilinearMap.uncurry0_curry0 (f : G[×0]→L[𝕜] G') :
 
 variable (𝕜 G)
 
-@[simp]
 theorem ContinuousMultilinearMap.curry0_uncurry0 (x : G') :
     (ContinuousMultilinearMap.curry0 𝕜 G x).uncurry0 = x :=
   rfl

Mathlib/Tactic/Have.lean

@@ -6,6 +6,51 @@ Authors: Arthur Paulino, Edward Ayers, Mario Carneiro
 import Lean
 import Mathlib.Data.Array.Defs
 
+namespace Mathlib.Tactic
+open Lean Elab.Tactic Meta Parser Term Syntax.MonadTraverser
+
+section deleteme -- once lean4#2262 is merged
+
+def hygieneInfoFn : ParserFn := fun c s =>
+  let input := c.input
+  let finish pos str trailing s :=
+    let info  := SourceInfo.original str pos trailing pos
+    let ident := mkIdent info str .anonymous
+    let stx   := mkNode `hygieneInfo' #[ident]
+    s.pushSyntax stx
+  let els s :=
+    let str := mkEmptySubstringAt input s.pos
+    finish s.pos str str s
+  if s.stxStack.isEmpty then els s else
+    let prev := s.stxStack.back
+    if let .original leading pos trailing endPos := prev.getTailInfo then
+      let str := mkEmptySubstringAt input endPos
+      let s := s.popSyntax.pushSyntax <| prev.setTailInfo (.original leading pos str endPos)
+      finish endPos str trailing s
+    else els s
+
+def hygieneInfoNoAntiquot : Parser := {
+  fn   := hygieneInfoFn
+  info := nodeInfo `hygieneInfo' epsilonInfo
+}
+
+@[combinator_formatter hygieneInfoNoAntiquot]
+def hygieneInfoNoAntiquot.formatter : PrettyPrinter.Formatter := goLeft
+@[combinator_parenthesizer hygieneInfoNoAntiquot]
+def hygieneInfoNoAntiquot.parenthesizer : PrettyPrinter.Parenthesizer := goLeft
+@[run_parser_attribute_hooks] def hygieneInfo : Parser :=
+  withAntiquot (mkAntiquot "hygieneInfo" `hygieneInfo' (anonymous := false)) hygieneInfoNoAntiquot
+
+end deleteme
+
+def optBinderIdent : Parser := leading_parser
+  -- Note: the withResetCache is because leading_parser seems to add a cache boundary,
+  -- which causes the `hygieneInfo` parser not to be able to undo the trailing whitespace
+  (ppSpace >> Term.binderIdent) <|> withResetCache hygieneInfo
+
+def optBinderIdent.name (id : TSyntax ``optBinderIdent) : Name :=
+  if id.raw[0].isIdent then id.raw[0].getId else HygieneInfo.mkIdent ⟨id.raw[0]⟩ `this |>.getId
+
 /--
 Uses `checkColGt` to prevent
 
@@ -20,25 +65,21 @@ have h
   exact Nat
 ```
 -/
-def Lean.Parser.Term.haveIdLhs' : Parser :=
-  optional (ppSpace >> ident >> many (ppSpace >>
-    checkColGt "expected to be indented" >>
-    letIdBinder)) >> optType
-
-namespace Mathlib.Tactic
-
-open Lean Elab.Tactic Meta
+def haveIdLhs' : Parser :=
+  optBinderIdent >> many (ppSpace >>
+    checkColGt "expected to be indented" >> letIdBinder) >> optType
 
-syntax "have" Parser.Term.haveIdLhs' : tactic
-syntax "let " Parser.Term.haveIdLhs' : tactic
-syntax "suffices" Parser.Term.haveIdLhs' : tactic
+syntax "have" haveIdLhs' : tactic
+syntax "let " haveIdLhs' : tactic
+syntax "suffices" haveIdLhs' : tactic
 
 open Elab Term in
-def haveLetCore (goal : MVarId) (name : Option Syntax) (bis : Array Syntax)
-  (t : Option Syntax) (keepTerm : Bool) : TermElabM (MVarId × MVarId) :=
+def haveLetCore (goal : MVarId) (name : TSyntax ``optBinderIdent)
+  (bis : Array (TSyntax ``letIdBinder))
+  (t : Option Term) (keepTerm : Bool) : TermElabM (MVarId × MVarId) :=
   let declFn := if keepTerm then MVarId.define else MVarId.assert
   goal.withContext do
-    let n := if let some n := name then n.getId else `this
+    let n := optBinderIdent.name name
     let elabBinders k := if bis.isEmpty then k #[] else elabBinders bis k
     let (goal1, t, p) ← elabBinders fun es ↦ do
       let t ← match t with
@@ -50,22 +91,21 @@ def haveLetCore (goal : MVarId) (name : Option Syntax) (bis : Array Syntax)
       let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
       pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)
     let (fvar, goal2) ← (← declFn goal n t p).intro1P
-    if let some stx := name then
-      goal2.withContext do
-        Term.addTermInfo' (isBinder := true) stx (mkFVar fvar)
+    goal2.withContext do
+      Term.addTermInfo' (isBinder := true) name.raw[0] (mkFVar fvar)
     pure (goal1, goal2)
 
 elab_rules : tactic
-| `(tactic| have $[$n:ident $bs*]? $[: $t:term]?) => do
-  let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t false
+| `(tactic| have $n:optBinderIdent $bs* $[: $t:term]?) => do
+  let (goal1, goal2) ← haveLetCore (← getMainGoal) n bs t false
   replaceMainGoal [goal1, goal2]
 
 elab_rules : tactic
-| `(tactic| suffices $[$n:ident $bs*]? $[: $t:term]?) => do
-  let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t false
+| `(tactic| suffices $n:optBinderIdent $bs* $[: $t:term]?) => do
+  let (goal1, goal2) ← haveLetCore (← getMainGoal) n bs t false
   replaceMainGoal [goal2, goal1]
 
 elab_rules : tactic
-| `(tactic| let $[$n:ident $bs*]? $[: $t:term]?) => withMainContext do
-  let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t true
+| `(tactic| let $n:optBinderIdent $bs* $[: $t:term]?) => withMainContext do
+  let (goal1, goal2) ← haveLetCore (← getMainGoal) n bs t true
   replaceMainGoal [goal1, goal2]

Mathlib/Tactic/Replace.lean

@@ -42,18 +42,16 @@ This can be used to simulate the `specialize` and `apply at` tactics of Coq.
 syntax "replace" haveDecl : tactic
 
 elab_rules : tactic
-  | `(tactic| replace $[$n?:ident]? $[: $t?:term]? := $v:term) =>
+  | `(tactic| replace $decl:haveDecl) =>
     withMainContext do
-      let name : Name := match n? with
-      | none   => `this
-      | some n => n.getId
-      let hId? := (← getLCtx).findFromUserName? name |>.map fun d ↦ d.fvarId
-      evalTactic $ ← `(tactic| have $[$n?]? $[: $t?]? := $v)
-      match hId? with
-      | some hId =>
-        try replaceMainGoal [← (← getMainGoal).clear hId]
-        catch | _ => pure ()
-      | none     => pure ()
+      let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl]
+      let origLCtx ← getLCtx
+      evalTactic $ ← `(tactic| have $decl:haveDecl)
+      let mut toClear := #[]
+      for fv in vars do
+        if let some ldecl := origLCtx.findFromUserName? fv.getId then
+          toClear := toClear.push ldecl.fvarId
+      liftMetaTactic1 (·.tryClearMany toClear)
 
 /--
 Acts like `have`, but removes a hypothesis with the same name as
@@ -86,14 +84,12 @@ h : β
 ⊢ goal
 ```
 -/
-syntax (name := replace') "replace" Parser.Term.haveIdLhs' : tactic
+syntax (name := replace') "replace" haveIdLhs' : tactic
 
 elab_rules : tactic
-| `(tactic| replace $[$n:ident $bs*]? $[: $t:term]?) => withMainContext do
-    let (goal1, goal2) ← haveLetCore (← getMainGoal) n (bs.getD #[]) t false
-    let name : Name := match n with
-    | none   => `this
-    | some n => n.getId
+| `(tactic| replace $n:optBinderIdent $bs* $[: $t:term]?) => withMainContext do
+    let (goal1, goal2) ← haveLetCore (← getMainGoal) n bs t false
+    let name := optBinderIdent.name n
     let hId? := (← getLCtx).findFromUserName? name |>.map fun d ↦ d.fvarId
     match hId? with
     | some hId =>

lake-manifest.json

@@ -22,6 +22,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6",
+    "rev": "d5471b83378e8ace4845f9a029af92f8b0cf10cb",
     "name": "std",
     "inputRev?": "main"}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-31
+leanprover/lean4:nightly-2023-06-07

test/Have.lean

@@ -26,12 +26,12 @@ example {a : Nat} : a = a := by
   exact this
 
 example : True := by
-  (let _N) -- FIXME: lean4#1670
+  let _N; -- FIXME: lean4#1670
   exact Nat
   have
   · exact 0
   have _h : Nat
-  · exact 5
+  · exact this
   have _h' x : x < x + 1
   · exact Nat.lt.base x
   have _h'' (x : Nat) : x < x + 1