Skip to content

Commit fd407eb

Browse files
astrainfinitaastrainfinita
committed
Update TransferInstance.lean
1 parent c7cf5ab commit fd407eb

1 file changed

Lines changed: 44 additions & 36 deletions

File tree

‎Mathlib/Algebra/Equiv/TransferInstance.lean‎

Lines changed: 44 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,7 @@ noncomputable def _root_.Shrink.ringEquiv [Small.{v} α] [Add α] [Mul α] : Shr
191191

192192
/-- Transfer `Semigroup` across an `Equiv` -/
193193
@[to_additive "Transfer `add_semigroup` across an `Equiv`"]
194-
protected abbrev semigroup [Semigroup β] : Semigroup α := by
194+
protected abbrev semigroup [Semigroup β] : Semigroup α := zeta% by
195195
let mul := e.mul
196196
apply e.injective.semigroup _; intros; exact e.apply_symm_apply _
197197

@@ -200,7 +200,7 @@ noncomputable instance [Small.{v} α] [Semigroup α] : Semigroup (Shrink.{v} α)
200200
(equivShrink α).symm.semigroup
201201

202202
/-- Transfer `SemigroupWithZero` across an `Equiv` -/
203-
protected abbrev semigroupWithZero [SemigroupWithZero β] : SemigroupWithZero α := by
203+
protected abbrev semigroupWithZero [SemigroupWithZero β] : SemigroupWithZero α := zeta% by
204204
let mul := e.mul
205205
let zero := e.zero
206206
apply e.injective.semigroupWithZero _ <;> intros <;> exact e.apply_symm_apply _
@@ -210,7 +210,7 @@ noncomputable instance [Small.{v} α] [SemigroupWithZero α] : SemigroupWithZero
210210

211211
/-- Transfer `CommSemigroup` across an `Equiv` -/
212212
@[to_additive "Transfer `AddCommSemigroup` across an `Equiv`"]
213-
protected abbrev commSemigroup [CommSemigroup β] : CommSemigroup α := by
213+
protected abbrev commSemigroup [CommSemigroup β] : CommSemigroup α := zeta% by
214214
let mul := e.mul
215215
apply e.injective.commSemigroup _; intros; exact e.apply_symm_apply _
216216

@@ -219,7 +219,7 @@ noncomputable instance [Small.{v} α] [CommSemigroup α] : CommSemigroup (Shrink
219219
(equivShrink α).symm.commSemigroup
220220

221221
/-- Transfer `MulZeroClass` across an `Equiv` -/
222-
protected abbrev mulZeroClass [MulZeroClass β] : MulZeroClass α := by
222+
protected abbrev mulZeroClass [MulZeroClass β] : MulZeroClass α := zeta% by
223223
let zero := e.zero
224224
let mul := e.mul
225225
apply e.injective.mulZeroClass _ <;> intros <;> exact e.apply_symm_apply _
@@ -229,7 +229,7 @@ noncomputable instance [Small.{v} α] [MulZeroClass α] : MulZeroClass (Shrink.{
229229

230230
/-- Transfer `MulOneClass` across an `Equiv` -/
231231
@[to_additive "Transfer `AddZeroClass` across an `Equiv`"]
232-
protected abbrev mulOneClass [MulOneClass β] : MulOneClass α := by
232+
protected abbrev mulOneClass [MulOneClass β] : MulOneClass α := zeta% by
233233
let one := e.one
234234
let mul := e.mul
235235
apply e.injective.mulOneClass _ <;> intros <;> exact e.apply_symm_apply _
@@ -239,7 +239,7 @@ noncomputable instance [Small.{v} α] [MulOneClass α] : MulOneClass (Shrink.{v}
239239
(equivShrink α).symm.mulOneClass
240240

241241
/-- Transfer `MulZeroOneClass` across an `Equiv` -/
242-
protected abbrev mulZeroOneClass [MulZeroOneClass β] : MulZeroOneClass α := by
242+
protected abbrev mulZeroOneClass [MulZeroOneClass β] : MulZeroOneClass α := zeta% by
243243
let zero := e.zero
244244
let one := e.one
245245
let mul := e.mul
@@ -250,7 +250,7 @@ noncomputable instance [Small.{v} α] [MulZeroOneClass α] : MulZeroOneClass (Sh
250250

251251
/-- Transfer `Monoid` across an `Equiv` -/
252252
@[to_additive "Transfer `AddMonoid` across an `Equiv`"]
253-
protected abbrev monoid [Monoid β] : Monoid α := by
253+
protected abbrev monoid [Monoid β] : Monoid α := zeta% by
254254
let one := e.one
255255
let mul := e.mul
256256
let pow := e.pow ℕ
@@ -262,7 +262,7 @@ noncomputable instance [Small.{v} α] [Monoid α] : Monoid (Shrink.{v} α) :=
262262

263263
/-- Transfer `CommMonoid` across an `Equiv` -/
264264
@[to_additive "Transfer `AddCommMonoid` across an `Equiv`"]
265-
protected abbrev commMonoid [CommMonoid β] : CommMonoid α := by
265+
protected abbrev commMonoid [CommMonoid β] : CommMonoid α := zeta% by
266266
let one := e.one
267267
let mul := e.mul
268268
let pow := e.pow ℕ
@@ -274,7 +274,7 @@ noncomputable instance [Small.{v} α] [CommMonoid α] : CommMonoid (Shrink.{v}
274274

275275
/-- Transfer `Group` across an `Equiv` -/
276276
@[to_additive "Transfer `AddGroup` across an `Equiv`"]
277-
protected abbrev group [Group β] : Group α := by
277+
protected abbrev group [Group β] : Group α := zeta% by
278278
let one := e.one
279279
let mul := e.mul
280280
let inv := e.Inv
@@ -289,7 +289,7 @@ noncomputable instance [Small.{v} α] [Group α] : Group (Shrink.{v} α) :=
289289

290290
/-- Transfer `CommGroup` across an `Equiv` -/
291291
@[to_additive "Transfer `AddCommGroup` across an `Equiv`"]
292-
protected abbrev commGroup [CommGroup β] : CommGroup α := by
292+
protected abbrev commGroup [CommGroup β] : CommGroup α := zeta% by
293293
let one := e.one
294294
let mul := e.mul
295295
let inv := e.Inv
@@ -304,7 +304,7 @@ noncomputable instance [Small.{v} α] [CommGroup α] : CommGroup (Shrink.{v} α)
304304

305305
/-- Transfer `NonUnitalNonAssocSemiring` across an `Equiv` -/
306306
protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring β] :
307-
NonUnitalNonAssocSemiring α := by
307+
NonUnitalNonAssocSemiring α := zeta% by
308308
let zero := e.zero
309309
let add := e.add
310310
let mul := e.mul
@@ -316,7 +316,7 @@ noncomputable instance [Small.{v} α] [NonUnitalNonAssocSemiring α] :
316316
(equivShrink α).symm.nonUnitalNonAssocSemiring
317317

318318
/-- Transfer `NonUnitalSemiring` across an `Equiv` -/
319-
protected abbrev nonUnitalSemiring [NonUnitalSemiring β] : NonUnitalSemiring α := by
319+
protected abbrev nonUnitalSemiring [NonUnitalSemiring β] : NonUnitalSemiring α := zeta% by
320320
let zero := e.zero
321321
let add := e.add
322322
let mul := e.mul
@@ -331,11 +331,13 @@ protected abbrev natCast [NatCast β] : NatCast α :=
331331
{ natCast := fun n => e.symm n }
332332

333333
/-- Transfer `AddMonoidWithOne` across an `Equiv` -/
334-
protected abbrev addMonoidWithOne [AddMonoidWithOne β] : AddMonoidWithOne α :=
335-
{ e.addMonoid, e.one with
336-
natCast := fun n => e.symm n
337-
natCast_zero := e.injective (by simp [zero_def])
338-
natCast_succ := fun n => e.injective (by simp [add_def, one_def]) }
334+
protected abbrev addMonoidWithOne [AddMonoidWithOne β] : AddMonoidWithOne α := zeta% by
335+
let zero := e.zero
336+
let one := e.one
337+
let add := e.add
338+
let nsmul := e.smul ℕ
339+
let natCast := e.natCast
340+
apply e.injective.addMonoidWithOne _ <;> intros <;> exact e.apply_symm_apply _
339341

340342
noncomputable instance [Small.{v} α] [AddMonoidWithOne α] : AddMonoidWithOne (Shrink.{v} α) :=
341343
(equivShrink α).symm.addMonoidWithOne
@@ -345,19 +347,23 @@ protected abbrev intCast [IntCast β] : IntCast α :=
345347
{ intCast := fun n => e.symm n }
346348

347349
/-- Transfer `AddGroupWithOne` across an `Equiv` -/
348-
protected abbrev addGroupWithOne [AddGroupWithOne β] : AddGroupWithOne α :=
349-
{ e.addMonoidWithOne,
350-
e.addGroup with
351-
intCast := fun n => e.symm n
352-
intCast_ofNat := fun n => by simp only [Int.cast_natCast]; rfl
353-
intCast_negSucc := fun _ =>
354-
congr_arg e.symm <| (Int.cast_negSucc _).trans <| congr_arg _ (e.apply_symm_apply _).symm }
350+
protected abbrev addGroupWithOne [AddGroupWithOne β] : AddGroupWithOne α := zeta% by
351+
let zero := e.zero
352+
let one := e.one
353+
let add := e.add
354+
let neg := e.Neg
355+
let sub := e.sub
356+
let nsmul := e.smul ℕ
357+
let zsmul := e.smul ℤ
358+
let natCast := e.natCast
359+
let intCast := e.intCast
360+
apply e.injective.addGroupWithOne _ <;> intros <;> exact e.apply_symm_apply _
355361

356362
noncomputable instance [Small.{v} α] [AddGroupWithOne α] : AddGroupWithOne (Shrink.{v} α) :=
357363
(equivShrink α).symm.addGroupWithOne
358364

359365
/-- Transfer `NonAssocSemiring` across an `Equiv` -/
360-
protected abbrev nonAssocSemiring [NonAssocSemiring β] : NonAssocSemiring α := by
366+
protected abbrev nonAssocSemiring [NonAssocSemiring β] : NonAssocSemiring α := zeta% by
361367
let zero := e.zero
362368
let add := e.add
363369
let one := e.one
@@ -370,7 +376,7 @@ noncomputable instance [Small.{v} α] [NonAssocSemiring α] : NonAssocSemiring (
370376
(equivShrink α).symm.nonAssocSemiring
371377

372378
/-- Transfer `Semiring` across an `Equiv` -/
373-
protected abbrev semiring [Semiring β] : Semiring α := by
379+
protected abbrev semiring [Semiring β] : Semiring α := zeta% by
374380
let zero := e.zero
375381
let add := e.add
376382
let one := e.one
@@ -384,7 +390,8 @@ noncomputable instance [Small.{v} α] [Semiring α] : Semiring (Shrink.{v} α) :
384390
(equivShrink α).symm.semiring
385391

386392
/-- Transfer `NonUnitalCommSemiring` across an `Equiv` -/
387-
protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring β] : NonUnitalCommSemiring α := by
393+
protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring β] :
394+
NonUnitalCommSemiring α := zeta% by
388395
let zero := e.zero
389396
let add := e.add
390397
let mul := e.mul
@@ -396,7 +403,7 @@ noncomputable instance [Small.{v} α] [NonUnitalCommSemiring α] :
396403
(equivShrink α).symm.nonUnitalCommSemiring
397404

398405
/-- Transfer `CommSemiring` across an `Equiv` -/
399-
protected abbrev commSemiring [CommSemiring β] : CommSemiring α := by
406+
protected abbrev commSemiring [CommSemiring β] : CommSemiring α := zeta% by
400407
let zero := e.zero
401408
let add := e.add
402409
let one := e.one
@@ -410,7 +417,8 @@ noncomputable instance [Small.{v} α] [CommSemiring α] : CommSemiring (Shrink.{
410417
(equivShrink α).symm.commSemiring
411418

412419
/-- Transfer `NonUnitalNonAssocRing` across an `Equiv` -/
413-
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α := by
420+
protected abbrev nonUnitalNonAssocRing [NonUnitalNonAssocRing β] :
421+
NonUnitalNonAssocRing α := zeta% by
414422
let zero := e.zero
415423
let add := e.add
416424
let mul := e.mul
@@ -425,7 +433,7 @@ noncomputable instance [Small.{v} α] [NonUnitalNonAssocRing α] :
425433
(equivShrink α).symm.nonUnitalNonAssocRing
426434

427435
/-- Transfer `NonUnitalRing` across an `Equiv` -/
428-
protected abbrev nonUnitalRing [NonUnitalRing β] : NonUnitalRing α := by
436+
protected abbrev nonUnitalRing [NonUnitalRing β] : NonUnitalRing α := zeta% by
429437
let zero := e.zero
430438
let add := e.add
431439
let mul := e.mul
@@ -439,7 +447,7 @@ noncomputable instance [Small.{v} α] [NonUnitalRing α] : NonUnitalRing (Shrink
439447
(equivShrink α).symm.nonUnitalRing
440448

441449
/-- Transfer `NonAssocRing` across an `Equiv` -/
442-
protected abbrev nonAssocRing [NonAssocRing β] : NonAssocRing α := by
450+
protected abbrev nonAssocRing [NonAssocRing β] : NonAssocRing α := zeta% by
443451
let zero := e.zero
444452
let add := e.add
445453
let one := e.one
@@ -456,7 +464,7 @@ noncomputable instance [Small.{v} α] [NonAssocRing α] : NonAssocRing (Shrink.{
456464
(equivShrink α).symm.nonAssocRing
457465

458466
/-- Transfer `Ring` across an `Equiv` -/
459-
protected abbrev ring [Ring β] : Ring α := by
467+
protected abbrev ring [Ring β] : Ring α := zeta% by
460468
let zero := e.zero
461469
let add := e.add
462470
let one := e.one
@@ -474,7 +482,7 @@ noncomputable instance [Small.{v} α] [Ring α] : Ring (Shrink.{v} α) :=
474482
(equivShrink α).symm.ring
475483

476484
/-- Transfer `NonUnitalCommRing` across an `Equiv` -/
477-
protected abbrev nonUnitalCommRing [NonUnitalCommRing β] : NonUnitalCommRing α := by
485+
protected abbrev nonUnitalCommRing [NonUnitalCommRing β] : NonUnitalCommRing α := zeta% by
478486
let zero := e.zero
479487
let add := e.add
480488
let mul := e.mul
@@ -488,7 +496,7 @@ noncomputable instance [Small.{v} α] [NonUnitalCommRing α] : NonUnitalCommRing
488496
(equivShrink α).symm.nonUnitalCommRing
489497

490498
/-- Transfer `CommRing` across an `Equiv` -/
491-
protected abbrev commRing [CommRing β] : CommRing α := by
499+
protected abbrev commRing [CommRing β] : CommRing α := zeta% by
492500
let zero := e.zero
493501
let add := e.add
494502
let one := e.one
@@ -533,7 +541,7 @@ noncomputable instance _root_.Shrink.instRatCast [Small.{v} α] [RatCast α] :
533541
RatCast (Shrink.{v} α) := (equivShrink α).symm.ratCast
534542

535543
/-- Transfer `DivisionRing` across an `Equiv` -/
536-
protected abbrev divisionRing [DivisionRing β] : DivisionRing α := by
544+
protected abbrev divisionRing [DivisionRing β] : DivisionRing α := zeta% by
537545
let zero := e.zero
538546
let add := e.add
539547
let one := e.one
@@ -558,7 +566,7 @@ noncomputable instance [Small.{v} α] [DivisionRing α] : DivisionRing (Shrink.{
558566
(equivShrink α).symm.divisionRing
559567

560568
/-- Transfer `Field` across an `Equiv` -/
561-
protected abbrev field [Field β] : Field α := by
569+
protected abbrev field [Field β] : Field α := zeta% by
562570
let zero := e.zero
563571
let add := e.add
564572
let one := e.one

0 commit comments

Comments
 (0)