use lean4 pr instead of date in adaptation notes

leanprover-community · Nov 12, 2024 · ea2e06b · ea2e06b
1 parent 961305b
commit ea2e06b
Show file tree

Hide file tree

Showing 9 changed files with 45 additions and 23 deletions.
diff --git a/Mathlib/Algebra/Lie/Semisimple/Basic.lean b/Mathlib/Algebra/Lie/Semisimple/Basic.lean
@@ -212,7 +212,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal
   set K := s'.sup id
   suffices I ≤ K by
     obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
-    exact ⟨t, Finset.Subset.trans hts' hs'.subset, htI⟩
+    exact ⟨t, hts'.trans hs'.subset, htI⟩
   -- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
   -- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
   intro x hx

diff --git a/Mathlib/AlgebraicGeometry/Modules/Tilde.lean b/Mathlib/AlgebraicGeometry/Modules/Tilde.lean
@@ -359,7 +359,8 @@ theorem localizationToStalk_mk (x : PrimeSpectrum.Top R) (f : M) (s : x.asIdeal.
   · exact homOfLE le_top
   · exact 𝟙 _
   refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_
-  #adaptation_note /-- 2024-11-11 added this refine hack to be able to add type hint in `change` -/
+  #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+    added this refine hack to be able to add type hint in `change` -/
   refine (?_ : @Eq ?ty _ _)
   change LocalizedModule.mk f 1 = (s.1 • LocalizedModule.mk f _ : ?ty)
   rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq]

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean b/Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
@@ -103,7 +103,8 @@ theorem IsBoundedBilinearMap.differentiableOn (h : IsBoundedBilinearMap 𝕜 b)
 
 variable (B : E →L[𝕜] F →L[𝕜] G)
 
-#adaptation_note /-- 2024-11-11 need `by exact` to deal with tricky unification -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  need `by exact` to deal with tricky unification -/
 @[fun_prop]
 theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {f : G' → E} {g : G' → F}
     {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} {s : Set G'} (hf : HasFDerivWithinAt f f' s x)
@@ -112,7 +113,8 @@ theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {f : G' → E} {g : G'
       (B.precompR G' (f x) g' + B.precompL G' f' (g x)) s x := by
   exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prod hg)
 
-#adaptation_note /-- 2024-11-11 need `by exact` to deal with tricky unification -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  need `by exact` to deal with tricky unification -/
 @[fun_prop]
 theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E}
     {g' : G' →L[𝕜] F} {x : G'} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean
@@ -42,7 +42,8 @@ section CLMCompApply
 variable {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H}
   {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G} {u : E → G} {u' : E →L[𝕜] G}
 
-#adaptation_note /-- 2024-11-11 split proof term into steps to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  split proof term into steps to solve unification issues. -/
 @[fun_prop]
 theorem HasStrictFDerivAt.clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
     HasStrictFDerivAt (fun y => (c y).comp (d y))
@@ -51,15 +52,17 @@ theorem HasStrictFDerivAt.clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStri
   have := this.comp x (hc.prod hd)
   exact this
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivWithinAt.clm_comp (hc : HasFDerivWithinAt c c' s x)
     (hd : HasFDerivWithinAt d d' s x) :
     HasFDerivWithinAt (fun y => (c y).comp (d y))
       ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') s x := by
   exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp_hasFDerivWithinAt x <| hc.prod hd
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivAt.clm_comp (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
     HasFDerivAt (fun y => (c y).comp (d y))
@@ -104,14 +107,16 @@ theorem HasStrictFDerivAt.clm_apply (hc : HasStrictFDerivAt c c' x)
     HasStrictFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x :=
   (isBoundedBilinearMap_apply.hasStrictFDerivAt (c x, u x)).comp x (hc.prod hu)
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivWithinAt.clm_apply (hc : HasFDerivWithinAt c c' s x)
     (hu : HasFDerivWithinAt u u' s x) :
     HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x := by
   exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp_hasFDerivWithinAt x (hc.prod hu)
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivAt.clm_apply (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
     HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x := by
@@ -239,14 +244,16 @@ theorem HasStrictFDerivAt.smul (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFD
     HasStrictFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x :=
   (isBoundedBilinearMap_smul.hasStrictFDerivAt (c x, f x)).comp x <| hc.prod hf
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivWithinAt.smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
     HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x := by
   exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp_hasFDerivWithinAt x <|
     hc.prod hf
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivAt.smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
     HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x := by
@@ -346,7 +353,8 @@ theorem HasStrictFDerivAt.mul (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDe
   ext z
   apply mul_comm
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivWithinAt.mul' (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
     HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) s x := by
@@ -360,7 +368,8 @@ theorem HasFDerivWithinAt.mul (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivW
   ext z
   apply mul_comm
 
-#adaptation_note /-- 2024-11-11 `by exact` to solve unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  `by exact` to solve unification issues. -/
 @[fun_prop]
 theorem HasFDerivAt.mul' (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :
     HasFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x := by

diff --git a/Mathlib/Analysis/InnerProductSpace/Calculus.lean b/Mathlib/Analysis/InnerProductSpace/Calculus.lean
@@ -78,7 +78,8 @@ theorem ContDiff.inner (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) :
     ContDiff ℝ n fun x => ⟪f x, g x⟫ :=
   contDiff_inner.comp (hf.prod hg)
 
-#adaptation_note /-- 2024-11-11 added `by exact` to handle a unification issue. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to handle a unification issue. -/
 theorem HasFDerivWithinAt.inner (hf : HasFDerivWithinAt f f' s x)
     (hg : HasFDerivWithinAt g g' s x) :
     HasFDerivWithinAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') s
@@ -91,7 +92,8 @@ theorem HasStrictFDerivAt.inner (hf : HasStrictFDerivAt f f' x) (hg : HasStrictF
   isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
     |>.hasStrictFDerivAt (f x, g x) |>.comp x (hf.prod hg)
 
-#adaptation_note /-- 2024-11-11 added `by exact` to handle a unification issue. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to handle a unification issue. -/
 theorem HasFDerivAt.inner (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
     HasFDerivAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') x := by
   exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)

diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
@@ -356,7 +356,8 @@ theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0)
       rwa [neg_re, ofReal_re, neg_pos]
     · exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt
 
-#adaptation_note /-- 2024-11-11 need `by exact` to deal with tricky unification -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  need `by exact` to deal with tricky unification -/
 theorem continuousAt_ofReal_cpow_const (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
     ContinuousAt (fun a => (a : ℂ) ^ y : ℝ → ℂ) x := by
   exact ContinuousAt.comp (x := x) (continuousAt_ofReal_cpow x y h)

diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
@@ -395,7 +395,8 @@ section fderiv
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {f' g' : E →L[ℝ] ℝ}
   {x : E} {s : Set E} {c p : ℝ} {n : ℕ∞}
 
-#adaptation_note /-- 2024-11-11 added `by exact` to deal with unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to deal with unification issues. -/
 theorem HasFDerivWithinAt.rpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x)
     (h : 0 < f x) : HasFDerivWithinAt (fun x => f x ^ g x)
       ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x := by
@@ -412,13 +413,15 @@ theorem HasStrictFDerivAt.rpow (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFD
       ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x :=
   (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).comp x (hf.prod hg)
 
-#adaptation_note /-- 2024-11-11 added `by exact` to deal with unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to deal with unification issues. -/
 theorem DifferentiableWithinAt.rpow (hf : DifferentiableWithinAt ℝ f s x)
     (hg : DifferentiableWithinAt ℝ g s x) (h : f x ≠ 0) :
     DifferentiableWithinAt ℝ (fun x => f x ^ g x) s x := by
   exact (differentiableAt_rpow_of_ne (f x, g x) h).comp_differentiableWithinAt x (hf.prod hg)
 
-#adaptation_note /-- 2024-11-11 added `by exact` to deal with unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to deal with unification issues. -/
 theorem DifferentiableAt.rpow (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x)
     (h : f x ≠ 0) : DifferentiableAt ℝ (fun x => f x ^ g x) x := by
   exact (differentiableAt_rpow_of_ne (f x, g x) h).comp x (hf.prod hg)
@@ -469,12 +472,14 @@ theorem HasStrictFDerivAt.const_rpow (hf : HasStrictFDerivAt f f' x) (hc : 0 < c
     HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x :=
   (hasStrictDerivAt_const_rpow hc (f x)).comp_hasStrictFDerivAt x hf
 
-#adaptation_note /-- 2024-11-11 added `by exact` to deal with unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to deal with unification issues. -/
 theorem ContDiffWithinAt.rpow (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x)
     (h : f x ≠ 0) : ContDiffWithinAt ℝ n (fun x => f x ^ g x) s x := by
   exact (contDiffAt_rpow_of_ne (f x, g x) h).comp_contDiffWithinAt x (hf.prod hg)
 
-#adaptation_note /-- 2024-11-11 added `by exact` to deal with unification issues. -/
+#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+  added `by exact` to deal with unification issues. -/
 theorem ContDiffAt.rpow (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (h : f x ≠ 0) :
     ContDiffAt ℝ n (fun x => f x ^ g x) x := by
   exact (contDiffAt_rpow_of_ne (f x, g x) h).comp x (hf.prod hg)

diff --git a/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean b/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean
@@ -94,7 +94,8 @@ theorem smoothSheafCommRing.isUnit_stalk_iff {x : M}
         apply inv_mul_cancel₀
         exact hVf y
     · intro y
-      #adaptation_note /-- 2024-11-11 was `exact`; somehow `convert` bypasess unification issues -/
+      #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+        was `exact`; somehow `convert` bypasess unification issues -/
       convert ((contDiffAt_inv _ (hVf y)).contMDiffAt).comp y
         (f.smooth.comp (smooth_inclusion hUV)).smoothAt
 

diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
@@ -351,7 +351,8 @@ lemma hasDerivAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
       mul_one, ContinuousLinearMap.coe_snd', mul_zero, add_zero, jacobiTheta₂'_term,
       jacobiTheta₂_term, mul_comm _ (cexp _)]
   rw [funext step2] at step1
-  #adaptation_note /-- 2024-11-11 need `by exact` to bypass unification failure -/
+  #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
+    need `by exact` to bypass unification failure -/
   have step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z := by
     exact ((hasFDerivAt_jacobiTheta₂ z hτ).comp z (hasFDerivAt_prod_mk_left z τ)).hasDerivAt
   rwa [← step1.tsum_eq] at step3