From 932071475e7e89428d81af9d7b2fab6c0b88bf3c Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 9 Jun 2023 00:56:47 +0000 Subject: [PATCH] chore: bump lean 06-07 (#4849) --- .../Analysis/Calculus/UniformLimitsDeriv.lean | 4 +- .../InnerProductSpace/Projection.lean | 131 ++++++++---------- Mathlib/Analysis/NormedSpace/Multilinear.lean | 1 - Mathlib/Tactic/Have.lean | 86 +++++++++--- Mathlib/Tactic/Replace.lean | 30 ++-- lake-manifest.json | 2 +- lean-toolchain | 2 +- test/Have.lean | 4 +- test/wlog.lean | 54 ++++---- 9 files changed, 164 insertions(+), 150 deletions(-) diff --git a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean index 9c0bbc5dd4fcb..32a2b6e4d4074 100644 --- a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean +++ b/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, diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index b14b4ce9f1660..cba752146c338 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/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) diff --git a/Mathlib/Analysis/NormedSpace/Multilinear.lean b/Mathlib/Analysis/NormedSpace/Multilinear.lean index c766e68adbc59..671c3fe8d093c 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear.lean +++ b/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 diff --git a/Mathlib/Tactic/Have.lean b/Mathlib/Tactic/Have.lean index 32270724b97c7..ae0cd388977c8 100644 --- a/Mathlib/Tactic/Have.lean +++ b/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] diff --git a/Mathlib/Tactic/Replace.lean b/Mathlib/Tactic/Replace.lean index 98a4f2cc2c2d6..43ba30f6eb048 100644 --- a/Mathlib/Tactic/Replace.lean +++ b/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 => diff --git a/lake-manifest.json b/lake-manifest.json index d0fe8ea33106b..eb896259aed50 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -22,6 +22,6 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6", + "rev": "d5471b83378e8ace4845f9a029af92f8b0cf10cb", "name": "std", "inputRev?": "main"}}]} diff --git a/lean-toolchain b/lean-toolchain index 02773fff67a50..cbd5420cdbba1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-05-31 +leanprover/lean4:nightly-2023-06-07 diff --git a/test/Have.lean b/test/Have.lean index 6795b5a452278..097fb16ef44eb 100644 --- a/test/Have.lean +++ b/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 diff --git a/test/wlog.lean b/test/wlog.lean index 31c89f221cf92..5a49daf2ded79 100644 --- a/test/wlog.lean +++ b/test/wlog.lean @@ -8,66 +8,66 @@ import Mathlib.Data.Nat.Basic example {x y : ℕ} : True := by wlog h : x ≤ y - { guard_hyp h : ¬x ≤ y - guard_hyp «this» : ∀ {x y : ℕ}, x ≤ y → True -- `wlog` generalizes by default + · guard_hyp h : ¬x ≤ y + guard_hyp this : ∀ {x y : ℕ}, x ≤ y → True -- `wlog` generalizes by default guard_target =ₛ True - trivial } - { guard_hyp h : x ≤ y + trivial + · guard_hyp h : x ≤ y guard_target =ₛ True - trivial } + trivial example {x y : ℕ} : True := by wlog h : x ≤ y generalizing x with H - { guard_hyp h : ¬x ≤ y + · guard_hyp h : ¬x ≤ y guard_hyp H : ∀ {x : ℕ}, x ≤ y → True -- only `x` was generalized guard_target =ₛ True - trivial } - { guard_hyp h : x ≤ y + trivial + · guard_hyp h : x ≤ y guard_target =ₛ True - trivial } + trivial example {x y z : ℕ} : True := by wlog h : x ≤ y + z with H - { guard_hyp h : ¬ x ≤ y + z + · guard_hyp h : ¬ x ≤ y + z guard_hyp H : ∀ {x y z : ℕ}, x ≤ y + z → True -- wlog-claim is named `H` instead of `this` guard_target =ₛ True - trivial } - { guard_hyp h : x ≤ y + z + trivial + · guard_hyp h : x ≤ y + z guard_target =ₛ True - trivial } + trivial example : ∀ _ _ : ℕ, True := by intro x y wlog h : x ≤ y -- `wlog` finds new variables - { trivial } - { trivial } + · trivial + · trivial example {x y : ℕ} : True := by wlog h : x ≤ y generalizing y x with H - { guard_hyp h : ¬ x ≤ y + · guard_hyp h : ¬ x ≤ y guard_hyp H : ∀ {x y : ℕ}, x ≤ y → True -- order of ids in `generalizing` is ignored - trivial } - { trivial } + trivial + · trivial -- metadata doesn't cause a problem example (α : Type := ℕ) (x : Option α := none) (y : Option α := by exact 0) : True := by wlog h : x = y with H - { guard_hyp h : ¬ x = y + · guard_hyp h : ¬ x = y guard_hyp H : ∀ α, ∀ {x y : Option α}, x = y → True - trivial } - { guard_hyp h : x = y + trivial + · guard_hyp h : x = y guard_target =ₛ True - trivial } + trivial -- inaccessible names work example {x y : ℕ} : True := by wlog _ : x ≤ y case _ h => -- if these hypotheses weren't inaccessible, they wouldn't be renamed by `case` - { guard_hyp h : ¬x ≤ y - guard_hyp «this» : ∀ {x y : ℕ}, x ≤ y → True + guard_hyp h : ¬x ≤ y + guard_hyp this : ∀ {x y : ℕ}, x ≤ y → True guard_target =ₛ True - trivial } + trivial case _ h => - { guard_hyp h : x ≤ y + guard_hyp h : x ≤ y guard_target =ₛ True - trivial } + trivial