Skip to content

Commit 0306da0

Browse files
riccardobrascab-mehta
authored andcommitted
perf(Data/DFinsupp/Defs): use fast_instance% (leanprover-community#39929)
Extracted from leanprover-community#39846.
1 parent 66fd97d commit 0306da0

1 file changed

Lines changed: 5 additions & 5 deletions

File tree

Mathlib/Data/DFinsupp/Defs.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ lemma coeFnAddMonoidHom_apply [∀ i, AddZeroClass (β i)] (v : Π₀ i, β i) :
234234
rfl
235235

236236
instance addCommMonoid [∀ i, AddCommMonoid (β i)] : AddCommMonoid (Π₀ i, β i) :=
237-
DFunLike.coe_injective.addCommMonoid _ coe_zero coe_add fun _ _ => coe_nsmul _ _
237+
fast_instance% DFunLike.coe_injective.addCommMonoid _ coe_zero coe_add fun _ _ => coe_nsmul _ _
238238

239239
instance [∀ i, AddGroup (β i)] : Neg (Π₀ i, β i) :=
240240
fun f => f.mapRange (fun _ => Neg.neg) fun _ => neg_zero⟩
@@ -267,12 +267,12 @@ theorem coe_zsmul [∀ i, AddGroup (β i)] (b : ℤ) (v : Π₀ i, β i) : ⇑(b
267267
rfl
268268

269269
instance [∀ i, AddGroup (β i)] : AddGroup (Π₀ i, β i) :=
270-
DFunLike.coe_injective.addGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => coe_nsmul _ _)
271-
fun _ _ => coe_zsmul _ _
270+
fast_instance% DFunLike.coe_injective.addGroup _ coe_zero coe_add coe_neg coe_sub
271+
(fun _ _ => coe_nsmul _ _) fun _ _ => coe_zsmul _ _
272272

273273
instance addCommGroup [∀ i, AddCommGroup (β i)] : AddCommGroup (Π₀ i, β i) :=
274-
DFunLike.coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => coe_nsmul _ _)
275-
fun _ _ => coe_zsmul _ _
274+
fast_instance% DFunLike.coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub
275+
(fun _ _ => coe_nsmul _ _) fun _ _ => coe_zsmul _ _
276276

277277
end Algebra
278278

0 commit comments

Comments
 (0)