Skip to content

Commit 19b2201

Browse files
VierkantorVierkantor
committed
chore(*): go through adaptation notes for lean4#6024
We have some adaptation notes referring to lean4#6024, which changed elaboration subtly; some tricky unifications no longer get solved. I checked every reference to make sure that these still apply. We don't expect that this change gets reverted, so we can turn the remaining adaptation notes into regular comments.
1 parent ffe8eee commit 19b2201

15 files changed

Lines changed: 43 additions & 101 deletions

File tree

‎Mathlib/Algebra/Category/Ring/Epi.lean‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,7 @@ lemma CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S]
2323
∀ s : S, s ⊗ₜ[R] 1 = 1 ⊗ₜ s := by
2424
constructor
2525
· intro H
26-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
27-
we need to add `(R := R) (A := S)` in the next line to deal with unification issues. -/
28-
have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom (R := R))
26+
have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom)
2927
(CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom)
3028
(by ext r; change algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
3129
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])

‎Mathlib/Algebra/Lie/Semisimple/Basic.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -207,10 +207,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal
207207
set K := s'.sup id
208208
suffices I ≤ K by
209209
obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
210-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
211-
we could write `hts'.trans hs'.subset` instead of
212-
`Finset.Subset.trans hts' hs'.subset` in the next line. -/
213-
exact ⟨t, Finset.Subset.trans hts' hs'.subset, htI⟩
210+
exact ⟨t, hts'.trans hs'.subset, htI⟩
214211
-- Since `I` is contained in the supremum of `J` with the supremum of `s'`,
215212
-- any element `x` of `I` can be written as `y + z` for some `y ∈ J` and `z ∈ K`.
216213
intro x hx

‎Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -103,22 +103,20 @@ theorem IsBoundedBilinearMap.differentiableOn (h : IsBoundedBilinearMap 𝕜 b)
103103

104104
variable (B : E →L[𝕜] F →L[𝕜] G)
105105

106-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
107-
need `by exact` to deal with tricky unification -/
108106
@[fun_prop]
109107
theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {f : G' → E} {g : G' → F}
110108
{f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} {s : Set G'} (hf : HasFDerivWithinAt f f' s x)
111109
(hg : HasFDerivWithinAt g g' s x) :
112110
HasFDerivWithinAt (fun y => B (f y) (g y))
113111
(B.precompR G' (f x) g' + B.precompL G' f' (g x)) s x := by
112+
-- need `by exact` to deal with tricky unification
114113
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prodMk hg)
115114

116-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
117-
need `by exact` to deal with tricky unification -/
118115
@[fun_prop]
119116
theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E}
120117
{g' : G' →L[𝕜] F} {x : G'} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
121118
HasFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x := by
119+
-- need `by exact` to deal with tricky unification
122120
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prodMk hg)
123121

124122
@[fun_prop]

‎Mathlib/Analysis/Calculus/FDeriv/Mul.lean‎

Lines changed: 16 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -42,32 +42,26 @@ section CLMCompApply
4242
variable {H : Type*} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H}
4343
{c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G} {u : E → G} {u' : E →L[𝕜] G}
4444

45-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
46-
split proof term into steps to solve unification issues. -/
4745
@[fun_prop]
4846
theorem HasStrictFDerivAt.clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
4947
HasStrictFDerivAt (fun y => (c y).comp (d y))
50-
((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x := by
51-
have := isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)
52-
have := this.comp x (hc.prodMk hd)
53-
exact this
48+
((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x :=
49+
(isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)).comp x (hc.prodMk hd)
5450

55-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
56-
`by exact` to solve unification issues. -/
5751
@[fun_prop]
5852
theorem HasFDerivWithinAt.clm_comp (hc : HasFDerivWithinAt c c' s x)
5953
(hd : HasFDerivWithinAt d d' s x) :
6054
HasFDerivWithinAt (fun y => (c y).comp (d y))
6155
((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') s x := by
62-
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp_hasFDerivWithinAt x (hc.prodMk hd)
56+
-- `by exact` to solve unification issues.
57+
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp_hasFDerivWithinAt x (hc.prodMk hd)
6358

64-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
65-
`by exact` to solve unification issues. -/
6659
@[fun_prop]
6760
theorem HasFDerivAt.clm_comp (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
6861
HasFDerivAt (fun y => (c y).comp (d y))
6962
((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x := by
70-
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp x <| hc.prodMk hd
63+
-- `by exact` to solve unification issues.
64+
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp x <| hc.prodMk hd
7165

7266
@[fun_prop]
7367
theorem DifferentiableWithinAt.clm_comp (hc : DifferentiableWithinAt 𝕜 c s x)
@@ -107,21 +101,19 @@ theorem HasStrictFDerivAt.clm_apply (hc : HasStrictFDerivAt c c' x)
107101
HasStrictFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x :=
108102
(isBoundedBilinearMap_apply.hasStrictFDerivAt (c x, u x)).comp x (hc.prodMk hu)
109103

110-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
111-
`by exact` to solve unification issues. -/
112104
@[fun_prop]
113105
theorem HasFDerivWithinAt.clm_apply (hc : HasFDerivWithinAt c c' s x)
114106
(hu : HasFDerivWithinAt u u' s x) :
115107
HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x := by
116-
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp_hasFDerivWithinAt x
108+
-- `by exact` to solve unification issues.
109+
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp_hasFDerivWithinAt x
117110
(hc.prodMk hu)
118111

119-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
120-
`by exact` to solve unification issues. -/
121112
@[fun_prop]
122113
theorem HasFDerivAt.clm_apply (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
123114
HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x := by
124-
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp x (hc.prodMk hu)
115+
-- `by exact` to solve unification issues.
116+
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp x (hc.prodMk hu)
125117

126118
@[fun_prop]
127119
theorem DifferentiableWithinAt.clm_apply (hc : DifferentiableWithinAt 𝕜 c s x)
@@ -250,26 +242,24 @@ theorem HasStrictFDerivAt.smul (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFD
250242
HasStrictFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x :=
251243
(isBoundedBilinearMap_smul.hasStrictFDerivAt (c x, f x)).comp x <| hc.prodMk hf
252244

253-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
254-
`by exact` to solve unification issues. -/
255245
@[fun_prop]
256246
theorem HasFDerivWithinAt.fun_smul
257247
(hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
258248
HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x := by
259-
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp_hasFDerivWithinAt x <|
249+
-- `by exact` to solve unification issues.
250+
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp_hasFDerivWithinAt x <|
260251
hc.prodMk hf
261252

262253
@[fun_prop]
263254
theorem HasFDerivWithinAt.smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
264255
HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x :=
265256
hc.fun_smul hf
266257

267-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
268-
`by exact` to solve unification issues. -/
269258
@[fun_prop]
270259
theorem HasFDerivAt.fun_smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
271260
HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x := by
272-
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp x <| hc.prodMk hf
261+
-- `by exact` to solve unification issues.
262+
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp x <| hc.prodMk hf
273263

274264
@[fun_prop]
275265
theorem HasFDerivAt.smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
@@ -414,12 +404,11 @@ theorem HasStrictFDerivAt.mul (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDe
414404
ext z
415405
apply mul_comm
416406

417-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
418-
`by exact` to solve unification issues. -/
419407
@[fun_prop]
420408
theorem HasFDerivWithinAt.fun_mul'
421409
(ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
422410
HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a' <• b x) s x := by
411+
-- `by exact` to solve unification issues.
423412
exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
424413
(a x, b x)).comp_hasFDerivWithinAt x (ha.prodMk hb)
425414

@@ -441,11 +430,10 @@ theorem HasFDerivWithinAt.mul (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivW
441430
HasFDerivWithinAt (c * d) (c x • d' + d x • c') s x :=
442431
hc.fun_mul hd
443432

444-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
445-
`by exact` to solve unification issues. -/
446433
@[fun_prop]
447434
theorem HasFDerivAt.fun_mul' (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :
448435
HasFDerivAt (fun y => a y * b y) (a x • b' + a' <• b x) x := by
436+
-- `by exact` to solve unification issues.
449437
exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
450438
(a x, b x)).comp x (ha.prodMk hb)
451439

‎Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -157,10 +157,8 @@ theorem cmp_dist_eq_cmp_dist_coe_center (z w : ℍ) (r : ℝ) :
157157
((mul_neg_of_pos_of_neg w.im_pos (sinh_neg_iff.2 hr₀)).trans_le dist_nonneg).cmp_eq_gt.symm]
158158
have hr₀' : 0 ≤ w.im * Real.sinh r := by positivity
159159
have hzw₀ : 0 < 2 * z.im * w.im := by positivity
160-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
161-
we need to give Lean the hint `(y := w.im * Real.sinh r)`. -/
162160
simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀,
163-
← (pow_left_strictMonoOn₀ two_ne_zero).cmp_map_eq dist_nonneg (y := w.im * Real.sinh r) hr₀',
161+
← (pow_left_strictMonoOn₀ (M₀ := ℝ) two_ne_zero).cmp_map_eq dist_nonneg hr₀',
164162
dist_coe_center_sq]
165163
rw [← cmp_mul_pos_left hzw₀, ← cmp_sub_zero, ← mul_sub, ← cmp_add_right, zero_add]
166164

‎Mathlib/Analysis/InnerProductSpace/Calculus.lean‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -78,12 +78,11 @@ theorem ContDiff.inner (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) :
7878
ContDiff ℝ n fun x => ⟪f x, g x⟫ :=
7979
contDiff_inner.comp (hf.prodMk hg)
8080

81-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
82-
added `by exact` to handle a unification issue. -/
8381
theorem HasFDerivWithinAt.inner (hf : HasFDerivWithinAt f f' s x)
8482
(hg : HasFDerivWithinAt g g' s x) :
8583
HasFDerivWithinAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') s
8684
x := by
85+
-- `by exact` to handle a tricky unification.
8786
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
8887
|>.hasFDerivAt (f x, g x) |>.comp_hasFDerivWithinAt x (hf.prodMk hg)
8988

@@ -92,10 +91,9 @@ theorem HasStrictFDerivAt.inner (hf : HasStrictFDerivAt f f' x) (hg : HasStrictF
9291
isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
9392
|>.hasStrictFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)
9493

95-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
96-
added `by exact` to handle a unification issue. -/
9794
theorem HasFDerivAt.inner (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
9895
HasFDerivAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') x := by
96+
-- `by exact` to handle a tricky unification.
9997
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
10098
|>.hasFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)
10199

‎Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -203,9 +203,6 @@ theorem isBoundedLinearMap_prod_multilinear {E : ι → Type*} [∀ i, Seminorme
203203
(ContinuousMultilinearMap.prodL 𝕜 E F G).toContinuousLinearEquiv
204204
|>.toContinuousLinearMap.isBoundedLinearMap
205205

206-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
207-
we needed to add the named arguments `(ι := ι) (G := F)`
208-
to `ContinuousMultilinearMap.compContinuousLinearMapL`. -/
209206
/-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the
210207
continuous multilinear map `f (g m₁, ..., g mₙ)` is a bounded linear operation. -/
211208
theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear (g : G →L[𝕜] E) :

‎Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean‎

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -464,11 +464,10 @@ section fderiv
464464
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : E → ℝ} {f' g' : E →L[ℝ] ℝ}
465465
{x : E} {s : Set E} {c p : ℝ} {n : WithTop ℕ∞}
466466

467-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
468-
added `by exact` to deal with unification issues. -/
469467
theorem HasFDerivWithinAt.rpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x)
470468
(h : 0 < f x) : HasFDerivWithinAt (fun x => f x ^ g x)
471469
((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x := by
470+
-- `by exact` to deal with tricky unification.
472471
exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp_hasFDerivWithinAt x
473472
(hf.prodMk hg)
474473

@@ -482,19 +481,17 @@ theorem HasStrictFDerivAt.rpow (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFD
482481
((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x :=
483482
(hasStrictFDerivAt_rpow_of_pos (f x, g x) h).comp x (hf.prodMk hg)
484483

485-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
486-
added `by exact` to deal with unification issues. -/
487484
@[fun_prop]
488485
theorem DifferentiableWithinAt.rpow (hf : DifferentiableWithinAt ℝ f s x)
489486
(hg : DifferentiableWithinAt ℝ g s x) (h : f x ≠ 0) :
490487
DifferentiableWithinAt ℝ (fun x => f x ^ g x) s x := by
488+
-- `by exact` to deal with tricky unification.
491489
exact (differentiableAt_rpow_of_ne (f x, g x) h).comp_differentiableWithinAt x (hf.prodMk hg)
492490

493-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
494-
added `by exact` to deal with unification issues. -/
495491
@[fun_prop]
496492
theorem DifferentiableAt.rpow (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x)
497493
(h : f x ≠ 0) : DifferentiableAt ℝ (fun x => f x ^ g x) x := by
494+
-- `by exact` to deal with tricky unification.
498495
exact (differentiableAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)
499496

500497
@[fun_prop]
@@ -550,18 +547,16 @@ theorem HasStrictFDerivAt.const_rpow (hf : HasStrictFDerivAt f f' x) (hc : 0 < c
550547
HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x :=
551548
(hasStrictDerivAt_const_rpow hc (f x)).comp_hasStrictFDerivAt x hf
552549

553-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
554-
added `by exact` to deal with unification issues. -/
555550
@[fun_prop]
556551
theorem ContDiffWithinAt.rpow (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x)
557552
(h : f x ≠ 0) : ContDiffWithinAt ℝ n (fun x => f x ^ g x) s x := by
553+
-- `by exact` to deal with tricky unification.
558554
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp_contDiffWithinAt x (hf.prodMk hg)
559555

560-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
561-
added `by exact` to deal with unification issues. -/
562556
@[fun_prop]
563557
theorem ContDiffAt.rpow (hf : ContDiffAt ℝ n f x) (hg : ContDiffAt ℝ n g x) (h : f x ≠ 0) :
564558
ContDiffAt ℝ n (fun x => f x ^ g x) x := by
559+
-- `by exact` to deal with tricky unification.
565560
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)
566561

567562
@[fun_prop]

‎Mathlib/Data/DFinsupp/Sigma.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -63,17 +63,13 @@ theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] :
6363

6464
@[simp]
6565
theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) :
66-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
67-
we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
6866
sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j) := by
6967
ext (i j)
7068
rfl
7169

7270
@[simp]
7371
theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)]
7472
(r : γ) (f : Π₀ (i : Σ _, _), δ i.1 i.2) :
75-
#adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
76-
we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
7773
sigmaCurry (r • f) = (r • sigmaCurry f : Π₀ (i) (j), δ i j) := by
7874
ext (i j)
7975
rfl

0 commit comments

Comments
 (0)