/
nolints.txt
3482 lines (3482 loc) · 79.2 KB
/
nolints.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import .all
run_cmd tactic.skip
apply_nolint
AddCommGroup
AddCommGroup.of
AddCommMon
AddCommMon.of
AddGroup
AddGroup.of
AddMon
AddMon.of
Cauchy.extend
Cauchy.gen
Class
CommRing.colimits.cocone_fun
CommRing.colimits.cocone_morphism
CommRing.colimits.colimit
CommRing.colimits.colimit_cocone
CommRing.colimits.colimit_is_colimit
CommRing.colimits.colimit_type
CommRing.colimits.desc_fun
CommRing.colimits.desc_fun_lift
CommRing.colimits.desc_morphism
CommRing.colimits.prequotient
CommRing.colimits.relation
CpltSepUniformSpace.to_UniformSpace
Gromov_Hausdorff.GH_dist
Gromov_Hausdorff.aux_gluing
Gromov_Hausdorff.aux_gluing_struct
Gromov_Hausdorff.candidates_b_dist
Meas
Module.of
Mon.colimits.cocone_fun
Mon.colimits.cocone_morphism
Mon.colimits.colimit
Mon.colimits.colimit_cocone
Mon.colimits.colimit_is_colimit
Mon.colimits.colimit_type
Mon.colimits.desc_fun
Mon.colimits.desc_fun_lift
Mon.colimits.desc_morphism
Mon.colimits.prequotient
Mon.colimits.relation
Set.map_definable_aux
Set.mem
Set.mk
Set.subset
Top.colimit
Top.colimit_is_colimit
Top.limit
Top.limit_is_limit
Top.presheaf
Top.presheaf.pushforward
Top.presheaf.pushforward.comp
Top.presheaf.pushforward.id
Top.presheaf.pushforward_eq
Top.presheaf.stalk_pushforward
Well_order
abelianization
abelianization.lift
abelianization.lift.unique
abelianization.of
abv_sum_le_sum_abv
add_comm_group.is_Z_bilin
add_con.to_setoid
add_equiv.mk'
add_equiv.refl
add_equiv.symm
add_equiv.to_add_monoid_hom
add_equiv.to_equiv
add_equiv.trans
add_group.closure
add_group.in_closure
add_monoid.smul
add_monoid_hom.add
add_monoid_hom.comp
add_monoid_hom.id
add_monoid_hom.mk'
add_monoid_hom.neg
add_monoid_hom.zero
additive
adjoin_root
adjoin_root.lift
adjoin_root.mk
adjoin_root.of
adjoin_root.root
alg_hom.comp
alg_hom.id
alg_hom.range
alg_hom.to_ring_hom
algebra.adjoin
algebra.adjoin_eq_range
algebra.adjoin_singleton_eq_range
algebra.comap.comm_ring
algebra.comap.has_scalar
algebra.comap.of_comap
algebra.comap.ring
algebra.comap.to_comap
algebra.gi
algebra.lmul_left
algebra.lmul_right
algebra.of_id
algebra.to_comap
algebra.to_top
algebra_map
algebraic_geometry.PresheafedSpace.comp
algebraic_geometry.PresheafedSpace.id
algebraic_geometry.PresheafedSpace.stalk
algebraic_geometry.PresheafedSpace.stalk_map
alist.disjoint
alist.foldl
applicative_transformation
apply_fun_name
archimedean
archimedean.floor_ring
associated
associated.setoid
associates
associates.factor_set
associates.factor_set.coe_add
associates.factor_set.prod
associates.factors
associates.factors'
associates.mk
associates.out
associates.prime
associates.unique'
associates_int_equiv_nat
auto.add_conjuncts
auto.add_simps
auto.auto_config
auto.case_hyp
auto.case_option
auto.case_some_hyp
auto.case_some_hyp_aux
auto.classical_normalize_lemma_names
auto.common_normalize_lemma_names
auto.do_subst
auto.do_substs
auto.eelim
auto.eelims
auto.mk_hinst_lemmas
auto.normalize_hyp
auto.normalize_hyps
auto.normalize_negations
auto.preprocess_goal
auto.preprocess_hyps
auto.split_hyp
auto.split_hyps
auto.split_hyps_aux
auto.whnf_reducible
auto_cases_at
bicompl.bitraverse
bicompr.bitraverse
bifunctor
bifunctor.fst
bifunctor.snd
bilin_form.bilin_linear_map_equiv
bilin_form.to_linear_map
binder_eq_elim
binder_eq_elim.check
binder_eq_elim.check_eq
binder_eq_elim.old_conv
binder_eq_elim.pull
binder_eq_elim.push
bisequence
bitraversable
bounded_continuous_function.arzela_ascoli
bounded_continuous_function.arzela_ascoli₁
bounded_continuous_function.arzela_ascoli₂
bounded_continuous_function.const
bounded_continuous_function.dist_eq
bounded_continuous_function.dist_set_exists
bounded_continuous_function.equicontinuous_of_continuity_modulus
buffer.list_equiv_buffer
can_lift_attr
canonically_ordered_comm_semiring
card_subgroup_dvd_card
card_trivial
cardinal.aleph'.order_iso
cardinal.aleph_idx.initial_seg
cardinal.aleph_idx.order_iso
cardinal.cantor_function
cardinal.cantor_function_aux
cardinal.ord.order_embedding
cast_num
cast_pos_num
cast_znum
category_theory.Aut
category_theory.Kleisli
category_theory.Kleisli.comp_def
category_theory.Kleisli.id_def
category_theory.Kleisli.mk
category_theory.adjunction.adjunction_of_equiv_left
category_theory.adjunction.adjunction_of_equiv_right
category_theory.adjunction.cocones_iso
category_theory.adjunction.comp
category_theory.adjunction.cones_iso
category_theory.adjunction.core_hom_equiv
category_theory.adjunction.core_unit_counit
category_theory.adjunction.functoriality_counit
category_theory.adjunction.functoriality_counit'
category_theory.adjunction.functoriality_is_left_adjoint
category_theory.adjunction.functoriality_is_right_adjoint
category_theory.adjunction.functoriality_left_adjoint
category_theory.adjunction.functoriality_right_adjoint
category_theory.adjunction.functoriality_unit
category_theory.adjunction.functoriality_unit'
category_theory.adjunction.has_colimit_of_comp_equivalence
category_theory.adjunction.has_limit_of_comp_equivalence
category_theory.adjunction.id
category_theory.adjunction.left_adjoint_of_equiv
category_theory.adjunction.mk_of_hom_equiv
category_theory.adjunction.mk_of_unit_counit
category_theory.adjunction.right_adjoint_of_equiv
category_theory.as_iso
category_theory.category_struct
category_theory.comma
category_theory.comma.fst
category_theory.comma.map_left
category_theory.comma.map_left_comp
category_theory.comma.map_left_id
category_theory.comma.map_right
category_theory.comma.map_right_comp
category_theory.comma.map_right_id
category_theory.comma.nat_trans
category_theory.comma.snd
category_theory.comma_morphism
category_theory.core
category_theory.core.forget_functor_to_core
category_theory.core.inclusion
category_theory.coyoneda
category_theory.coyoneda.is_iso
category_theory.curry
category_theory.curry_obj
category_theory.currying
category_theory.discrete
category_theory.discrete.lift
category_theory.discrete.opposite
category_theory.epi
category_theory.eq_to_hom
category_theory.eq_to_iso
category_theory.equivalence.adjointify_η
category_theory.equivalence.counit
category_theory.equivalence.counit_inv
category_theory.equivalence.equivalence_of_fully_faithfully_ess_surj
category_theory.equivalence.ess_surj_of_equivalence
category_theory.equivalence.fun_inv_id_assoc
category_theory.equivalence.inv_fun_id_assoc
category_theory.equivalence.mk
category_theory.equivalence.refl
category_theory.equivalence.symm
category_theory.equivalence.to_adjunction
category_theory.equivalence.trans
category_theory.equivalence.unit
category_theory.equivalence.unit_inv
category_theory.ess_surj
category_theory.ess_surj.iso
category_theory.evaluation
category_theory.evaluation_uncurried
category_theory.full_subcategory_inclusion
category_theory.functor.adjunction
category_theory.functor.as_equivalence
category_theory.functor.associator
category_theory.functor.const
category_theory.functor.const.op_obj_op
category_theory.functor.const.op_obj_unop
category_theory.functor.flip
category_theory.functor.fun_inv_id
category_theory.functor.fun_obj_preimage_iso
category_theory.functor.inv
category_theory.functor.inv_fun_id
category_theory.functor.left_op
category_theory.functor.left_unitor
category_theory.functor.map_cocone_morphism
category_theory.functor.map_cone_inv
category_theory.functor.map_cone_morphism
category_theory.functor.map_iso
category_theory.functor.obj_preimage
category_theory.functor.of_function
category_theory.functor.op
category_theory.functor.op_hom
category_theory.functor.op_inv
category_theory.functor.right_op
category_theory.functor.right_unitor
category_theory.functor.sections
category_theory.functor.star
category_theory.functor.to_cocone
category_theory.functor.to_cone
category_theory.functor.ulift_down
category_theory.functor.ulift_down_up
category_theory.functor.ulift_up
category_theory.functor.ulift_up_down
category_theory.functor.unop
category_theory.has_hom
category_theory.has_hom.hom.op
category_theory.has_hom.hom.unop
category_theory.has_limits_of_reflective
category_theory.hom_of_element
category_theory.induced_category
category_theory.induced_functor
category_theory.is_equivalence.mk
category_theory.is_iso_of_fully_faithful
category_theory.is_iso_of_op
category_theory.is_left_adjoint
category_theory.is_right_adjoint
category_theory.iso
category_theory.iso.hom_congr
category_theory.iso.op
category_theory.iso.refl
category_theory.iso.symm
category_theory.iso.to_equiv
category_theory.iso.trans
category_theory.iso_whisker_left
category_theory.iso_whisker_right
category_theory.large_groupoid
category_theory.left_adjoint
category_theory.limits.binary_cofan
category_theory.limits.binary_cofan.mk
category_theory.limits.binary_fan
category_theory.limits.binary_fan.mk
category_theory.limits.cocone.equiv
category_theory.limits.cocone.extensions
category_theory.limits.cocone.of_cofork
category_theory.limits.cocone.of_pushout_cocone
category_theory.limits.cocone.whisker
category_theory.limits.cocone_left_op_of_cone
category_theory.limits.cocone_morphism
category_theory.limits.cocone_of_cone_left_op
category_theory.limits.cocones.forget
category_theory.limits.cocones.functoriality
category_theory.limits.cocones.precompose
category_theory.limits.cocones.precompose_comp
category_theory.limits.cocones.precompose_equivalence
category_theory.limits.cocones.precompose_id
category_theory.limits.coequalizer
category_theory.limits.coequalizer.desc
category_theory.limits.coequalizer.π
category_theory.limits.cofan
category_theory.limits.cofan.mk
category_theory.limits.cofork
category_theory.limits.cofork.of_cocone
category_theory.limits.cofork.of_π
category_theory.limits.cofork.π
category_theory.limits.colim_coyoneda
category_theory.limits.colimit
category_theory.limits.colimit.cocone
category_theory.limits.colimit.cocone_morphism
category_theory.limits.colimit.desc
category_theory.limits.colimit.hom_iso
category_theory.limits.colimit.hom_iso'
category_theory.limits.colimit.is_colimit
category_theory.limits.colimit.post
category_theory.limits.colimit.pre
category_theory.limits.colimit.ι
category_theory.limits.cone.equiv
category_theory.limits.cone.extensions
category_theory.limits.cone.of_fork
category_theory.limits.cone.of_pullback_cone
category_theory.limits.cone.whisker
category_theory.limits.cone_left_op_of_cocone
category_theory.limits.cone_morphism
category_theory.limits.cone_of_cocone_left_op
category_theory.limits.cones.forget
category_theory.limits.cones.functoriality
category_theory.limits.cones.postcompose
category_theory.limits.cones.postcompose_comp
category_theory.limits.cones.postcompose_equivalence
category_theory.limits.cones.postcompose_id
category_theory.limits.coprod
category_theory.limits.coprod.desc
category_theory.limits.coprod.inl
category_theory.limits.coprod.inr
category_theory.limits.coprod.map
category_theory.limits.equalizer
category_theory.limits.equalizer.lift
category_theory.limits.equalizer.ι
category_theory.limits.evaluate_functor_category_colimit_cocone
category_theory.limits.evaluate_functor_category_limit_cone
category_theory.limits.fan
category_theory.limits.fan.mk
category_theory.limits.fork
category_theory.limits.fork.of_cone
category_theory.limits.fork.of_ι
category_theory.limits.fork.ι
category_theory.limits.functor_category_colimit_cocone
category_theory.limits.functor_category_is_colimit_cocone
category_theory.limits.functor_category_is_limit_cone
category_theory.limits.functor_category_limit_cone
category_theory.limits.has_binary_coproducts
category_theory.limits.has_binary_products
category_theory.limits.has_coequalizers
category_theory.limits.has_colimit_of_equivalence_comp
category_theory.limits.has_colimit_of_iso
category_theory.limits.has_colimits_of_shape_of_equivalence
category_theory.limits.has_coproducts
category_theory.limits.has_equalizers
category_theory.limits.has_finite_colimits
category_theory.limits.has_finite_coproducts
category_theory.limits.has_finite_limits
category_theory.limits.has_finite_products
category_theory.limits.has_initial
category_theory.limits.has_limit_of_equivalence_comp
category_theory.limits.has_limit_of_iso
category_theory.limits.has_limits_of_shape_of_equivalence
category_theory.limits.has_products
category_theory.limits.has_pullbacks
category_theory.limits.has_pushouts
category_theory.limits.has_terminal
category_theory.limits.initial
category_theory.limits.initial.to
category_theory.limits.is_colimit.desc_cocone_morphism
category_theory.limits.is_colimit.hom_iso'
category_theory.limits.is_colimit.iso_unique_cocone_morphism
category_theory.limits.is_colimit.mk_cocone_morphism
category_theory.limits.is_colimit.of_iso_colimit
category_theory.limits.is_limit.hom_iso'
category_theory.limits.is_limit.iso_unique_cone_morphism
category_theory.limits.is_limit.lift_cone_morphism
category_theory.limits.is_limit.mk_cone_morphism
category_theory.limits.is_limit.of_iso_limit
category_theory.limits.lim_yoneda
category_theory.limits.limit
category_theory.limits.limit.cone
category_theory.limits.limit.cone_morphism
category_theory.limits.limit.hom_iso
category_theory.limits.limit.hom_iso'
category_theory.limits.limit.is_limit
category_theory.limits.limit.lift
category_theory.limits.limit.post
category_theory.limits.limit.pre
category_theory.limits.limit.π
category_theory.limits.map_pair
category_theory.limits.pair
category_theory.limits.pair_function
category_theory.limits.parallel_pair
category_theory.limits.pi.lift
category_theory.limits.pi.map
category_theory.limits.pi.π
category_theory.limits.preserves_colimit
category_theory.limits.preserves_colimits
category_theory.limits.preserves_colimits_of_shape
category_theory.limits.preserves_limit
category_theory.limits.preserves_limits
category_theory.limits.preserves_limits_of_shape
category_theory.limits.prod
category_theory.limits.prod.fst
category_theory.limits.prod.lift
category_theory.limits.prod.map
category_theory.limits.prod.snd
category_theory.limits.pullback.fst
category_theory.limits.pullback.lift
category_theory.limits.pullback.snd
category_theory.limits.pullback_cone
category_theory.limits.pullback_cone.fst
category_theory.limits.pullback_cone.mk
category_theory.limits.pullback_cone.of_cone
category_theory.limits.pullback_cone.snd
category_theory.limits.pushout.desc
category_theory.limits.pushout.inl
category_theory.limits.pushout.inr
category_theory.limits.pushout_cocone
category_theory.limits.pushout_cocone.inl
category_theory.limits.pushout_cocone.inr
category_theory.limits.pushout_cocone.mk
category_theory.limits.pushout_cocone.of_cocone
category_theory.limits.reflects_colimit
category_theory.limits.reflects_colimits
category_theory.limits.reflects_colimits_of_shape
category_theory.limits.reflects_limit
category_theory.limits.reflects_limits
category_theory.limits.reflects_limits_of_shape
category_theory.limits.sigma.desc
category_theory.limits.sigma.map
category_theory.limits.sigma.ι
category_theory.limits.terminal
category_theory.limits.terminal.from
category_theory.limits.types.colimit
category_theory.limits.types.colimit_is_colimit
category_theory.limits.types.limit
category_theory.limits.types.limit_is_limit
category_theory.limits.types.types_colimit_pre
category_theory.limits.walking_cospan.hom.comp
category_theory.limits.walking_parallel_pair_hom.comp
category_theory.limits.walking_span.hom.comp
category_theory.monad
category_theory.monad.algebra.hom
category_theory.monad.algebra.hom.comp
category_theory.monad.algebra.hom.id
category_theory.monad.comparison
category_theory.monad.comparison_forget
category_theory.monad.forget
category_theory.monad.forget_creates_limits
category_theory.monad.forget_creates_limits.c
category_theory.monad.forget_creates_limits.cone_point
category_theory.monad.forget_creates_limits.γ
category_theory.monad.free
category_theory.monadic_creates_limits
category_theory.mono
category_theory.monoidal_functor.ε_iso
category_theory.monoidal_functor.μ_iso
category_theory.nat_iso.hcomp
category_theory.nat_iso.is_iso_app_of_is_iso
category_theory.nat_iso.is_iso_of_is_iso_app
category_theory.nat_iso.of_components
category_theory.nat_iso.of_isos
category_theory.nat_iso.op
category_theory.nat_trans.left_op
category_theory.nat_trans.of_function
category_theory.nat_trans.of_homs
category_theory.nat_trans.on_presheaf
category_theory.nat_trans.op
category_theory.nat_trans.right_op
category_theory.nat_trans.unop
category_theory.obviously'
category_theory.op_op
category_theory.over
category_theory.over.colimit
category_theory.over.forget
category_theory.over.forget_colimit_is_colimit
category_theory.over.hom_mk
category_theory.over.map
category_theory.over.mk
category_theory.over.post
category_theory.prod.associativity
category_theory.prod.associator
category_theory.prod.braiding
category_theory.prod.inverse_associator
category_theory.prod.swap
category_theory.prod.symmetry
category_theory.representable
category_theory.right_adjoint
category_theory.single_obj
category_theory.single_obj.star
category_theory.small_groupoid
category_theory.sum.associativity
category_theory.sum.associator
category_theory.sum.inverse_associator
category_theory.ulift_functor
category_theory.ulift_trivial
category_theory.uncurry
category_theory.under
category_theory.under.forget
category_theory.under.forget_limit_is_limit
category_theory.under.hom_mk
category_theory.under.limit
category_theory.under.map
category_theory.under.mk
category_theory.under.post
category_theory.whisker_left
category_theory.whisker_right
category_theory.whiskering_left
category_theory.whiskering_right
category_theory.yoneda
category_theory.yoneda.is_iso
category_theory.yoneda_evaluation
category_theory.yoneda_lemma
category_theory.yoneda_pairing
category_theory.yoneda_sections
category_theory.yoneda_sections_small
cau_seq
cau_seq.abv_pos_of_not_lim_zero
cau_seq.bounded'
cau_seq.cauchy
cau_seq.cauchy₂
cau_seq.cauchy₃
cau_seq.completion.Cauchy
cau_seq.completion.discrete_field
cau_seq.completion.mk
cau_seq.completion.of_rat
cau_seq.equiv_def₃
cau_seq.inv
cau_seq.inv_aux
cau_seq.is_complete
cau_seq.le_of_exists
cau_seq.lim
cau_seq.lim_zero
cau_seq.of_eq
cau_seq.of_near
cauchy_product
cauchy_seq_bdd
centralizer.add_submonoid
cfilter.to_realizer
char_p.char_is_prime_of_ge_two
classical.DLO
classical.all_definable
classical.exists_cases
classical.inhabited_of_nonempty'
comm_ring.anti_equiv_to_equiv
comm_ring.equiv_to_anti_equiv
commutator
comp.seq
compact.realizer
completion
complex
complex.I
complex.abs
complex.cau_seq_abs
complex.cau_seq_conj
complex.cau_seq_im
complex.cau_seq_re
complex.conj
complex.cos
complex.cosh
complex.exp
complex.exp'
complex.lim_aux
complex.norm_sq
complex.of_real
complex.real_prod_equiv
complex.real_prod_homeo
complex.sin
complex.sinh
complex.tan
complex.tanh
computable
computable_pred
computable₂
computation.bind.F
computation.bind.G
computation.bisim_o
computation.cases_on
computation.corec.F
computation.is_bisimulation
computation.lift_rel_aux
computation.map_congr
computation.mem
computation.mem_rec_on
computation.parallel.aux1
computation.parallel.aux2
computation.parallel_rec
computation.terminates_rec_on
con.to_setoid
connected_component
const.bitraverse
constr_smul
cont
cont_t
cont_t.map
cont_t.monad_lift
cont_t.run
cont_t.with_cont_t
continuous.comap
continuous_map
continuous_map.coev
continuous_map.compact_open.gen
continuous_map.ev
continuous_map.induced
continuous_of_locally_uniform_limit_of_continuous
continuous_of_uniform_limit_of_continuous
conv.discharge_eq_lhs
conv.interactive.erw
conv.interactive.norm_cast
conv.interactive.norm_num
conv.interactive.norm_num1
conv.interactive.ring
conv.interactive.ring2
conv.repeat_count
conv.repeat_with_results
conv.replace_lhs
conv.slice
conv.slice_lhs
conv.slice_rhs
convex_on_linorder
ctop.realizer.id
ctop.realizer.nhds
ctop.realizer.nhds_F
ctop.realizer.nhds_σ
ctop.realizer.of_equiv
ctop.to_realizer
decidable.lt_by_cases
decidable_linear_order.lift
decidable_linear_order_of_is_well_order
decidable_of_bool
decidable_of_iff
decidable_of_iff'
decidable_zero_symm
declaration.update_with_fun
dense_or_discrete
denumerable.equiv₂
denumerable.eqv
denumerable.lower
denumerable.lower'
denumerable.mk'
denumerable.of_encodable_of_infinite
denumerable.of_equiv
denumerable.of_nat
denumerable.pair
denumerable.raise
denumerable.raise'
denumerable.raise'_finset
dfinsupp
dfinsupp.decidable_eq
dfinsupp.erase
dfinsupp.lmk
dfinsupp.lsingle
dfinsupp.map_range_def
dfinsupp.map_range_single
dfinsupp.mk
dfinsupp.pre
dfinsupp.single
dfinsupp.subtype_domain_sum
dfinsupp.sum_apply
dfinsupp.support
dfinsupp.to_has_scalar
dfinsupp.to_module
dfinsupp.zip_with
dfinsupp.zip_with_def
dioph.pell_dioph
dioph.xn_dioph
direct_sum
direct_sum.component
direct_sum.id
direct_sum.lid
direct_sum.lmk
direct_sum.lof
direct_sum.lset_to_set
direct_sum.mk
direct_sum.of
direct_sum.set_to_set
direct_sum.to_group
direct_sum.to_module
directed_order
dlist.join
dlist.list_equiv_dlist
eckmann_hilton.comm_group
eckmann_hilton.comm_monoid
eckmann_hilton.is_unital
emetric.cauchy_iff
emetric.cauchy_seq_iff
emetric.cauchy_seq_iff'
emetric.exists_ball_subset_ball
emetric.is_open_iff
emetric.mem_closure_iff'
emetric.mem_nhds_iff
emetric.nhds_eq
emetric.tendsto_at_top
emetric.tendsto_nhds
emetric.totally_bounded_iff
emetric.totally_bounded_iff'
emetric.uniform_continuous_iff
emetric.uniform_embedding_iff
emetric.uniform_embedding_iff'
empty.elim
enat
encodable.choose
encodable.choose_x
encodable.decidable_eq_of_encodable
encodable.decidable_range_encode
encodable.decode2
encodable.decode_list
encodable.decode_multiset
encodable.decode_sigma
encodable.decode_subtype
encodable.decode_sum
encodable.encodable_of_list
encodable.encode_list
encodable.encode_multiset
encodable.encode_sigma
encodable.encode_subtype
encodable.encode_sum
encodable.equiv_range_encode
encodable.fintype_arrow
encodable.fintype_pi
encodable.of_equiv
encodable.of_inj
encodable.of_left_injection
encodable.of_left_inverse
encodable.trunc_encodable_of_fintype
ennreal.Icc_mem_nhds
ennreal.ennreal_equiv_nnreal
ennreal.ennreal_equiv_sum
ennreal.nhds_of_ne_top
ennreal.tendsto_at_top
ennreal.tendsto_nhds
eq_of_forall_dist_le
eq_of_forall_edist_le
eq_of_le_of_forall_ge_of_dense
eq_of_le_of_forall_le_of_dense
equiv.Pi_congr_right
equiv.Pi_curry
equiv.Prop_equiv_bool
equiv.add_comm_group
equiv.add_comm_monoid
equiv.add_comm_semigroup
equiv.add_group
equiv.add_left
equiv.add_monoid
equiv.add_right
equiv.add_semigroup
equiv.array_equiv_fin
equiv.arrow_arrow_equiv_prod_arrow
equiv.arrow_congr
equiv.arrow_prod_equiv_prod_arrow
equiv.arrow_punit_equiv_punit
equiv.bool_equiv_punit_sum_punit
equiv.bool_prod_equiv_sum
equiv.bool_prod_nat_equiv_nat
equiv.cast
equiv.comm_group
equiv.comm_monoid
equiv.comm_ring
equiv.comm_semigroup
equiv.comm_semiring
equiv.conj
equiv.d_array_equiv_fin
equiv.decidable_eq
equiv.decidable_eq_of_equiv
equiv.discrete_field
equiv.division_ring
equiv.domain
equiv.empty_arrow_equiv_punit
equiv.empty_equiv_pempty
equiv.empty_of_not_nonempty
equiv.empty_prod
equiv.empty_sum
equiv.equiv_congr
equiv.equiv_empty
equiv.equiv_pempty
equiv.false_arrow_equiv_punit
equiv.false_equiv_empty
equiv.false_equiv_pempty
equiv.field
equiv.fin_equiv_subtype
equiv.functor
equiv.group
equiv.has_add
equiv.has_inv
equiv.has_mul
equiv.has_neg
equiv.has_one
equiv.has_zero
equiv.inhabited_of_equiv
equiv.int_equiv_nat
equiv.int_equiv_nat_sum_nat
equiv.integral_domain
equiv.inv
equiv.is_lawful_traversable
equiv.is_lawful_traversable'
equiv.list_equiv_of_equiv
equiv.list_equiv_self_of_equiv_nat
equiv.list_nat_equiv_nat
equiv.map
equiv.monoid
equiv.mul_left
equiv.mul_right
equiv.nat_equiv_nat_sum_punit
equiv.nat_prod_nat_equiv_nat
equiv.nat_sum_nat_equiv_nat
equiv.nat_sum_punit_equiv_nat
equiv.neg
equiv.nonzero_comm_ring
equiv.of_bijective
equiv.option_equiv_sum_punit
equiv.pempty_arrow_equiv_punit
equiv.pempty_equiv_pempty
equiv.pempty_of_not_nonempty
equiv.pempty_prod
equiv.pempty_sum
equiv.perm.card_support_swap
equiv.perm.cycle_factors
equiv.perm.cycle_factors_aux
equiv.perm.cycle_of
equiv.perm.disjoint
equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self
equiv.perm.is_cycle
equiv.perm.is_cycle_swap
equiv.perm.is_cycle_swap_mul_aux₁
equiv.perm.is_swap
equiv.perm.of_subtype
equiv.perm.same_cycle
equiv.perm.sign_aux
equiv.perm.sign_aux2
equiv.perm.sign_aux3
equiv.perm.sign_bij_aux
equiv.perm.sign_cycle
equiv.perm.subtype_perm
equiv.perm.support
equiv.perm.support_swap
equiv.perm.swap_factors_aux
equiv.perm.trunc_swap_factors
equiv.perm_congr
equiv.pi_equiv_subtype_sigma
equiv.plift
equiv.pnat_equiv_nat
equiv.prod_assoc
equiv.prod_comm
equiv.prod_congr
equiv.prod_empty
equiv.prod_equiv_of_equiv_nat
equiv.prod_pempty
equiv.prod_punit
equiv.prod_sum_distrib
equiv.prop_equiv_punit
equiv.psigma_equiv_sigma
equiv.psum_equiv_sum
equiv.punit_arrow_equiv
equiv.punit_equiv_punit
equiv.punit_prod
equiv.refl
equiv.ring
equiv.semigroup
equiv.semiring
equiv.set.congr
equiv.set.empty
equiv.set.image
equiv.set.image_of_inj_on
equiv.set.insert
equiv.set.of_eq
equiv.set.pempty
equiv.set.prod
equiv.set.range
equiv.set.sep
equiv.set.singleton
equiv.set.sum_compl
equiv.set.union
equiv.set.union'
equiv.set.union_sum_inter
equiv.set.univ
equiv.set_congr
equiv.sigma_congr_left
equiv.sigma_congr_right
equiv.sigma_equiv_prod
equiv.sigma_equiv_prod_of_equiv
equiv.sigma_preimage_equiv
equiv.sigma_prod_distrib
equiv.sigma_subtype_preimage_equiv
equiv.sigma_subtype_preimage_equiv_subtype
equiv.subtype_congr
equiv.subtype_congr_prop
equiv.subtype_congr_right
equiv.subtype_equiv_of_subtype'
equiv.subtype_pi_equiv_pi
equiv.subtype_quotient_equiv_quotient_subtype
equiv.subtype_subtype_equiv_subtype_exists
equiv.subtype_subtype_equiv_subtype_inter
equiv.sum_arrow_equiv_prod_arrow
equiv.sum_assoc
equiv.sum_comm
equiv.sum_congr
equiv.sum_empty
equiv.sum_equiv_sigma_bool
equiv.sum_pempty
equiv.sum_prod_distrib
equiv.swap_core
equiv.symm
equiv.to_embedding
equiv.to_iso
equiv.to_pequiv
equiv.trans
equiv.traversable
equiv.traverse
equiv.true_equiv_punit
equiv.ulift
equiv.unique_congr
equiv.unique_of_equiv
equiv.units_equiv_ne_zero
equiv.vector_equiv_array
equiv.vector_equiv_fin
equiv.zero_ne_one_class
equiv_of_dim_eq_dim
equiv_of_unique_of_unique
equiv_punit_of_unique
equiv_type_constr
erased.bind
erased.choice
erased.equiv
erased.join
erased.mk
erased.out
erased.out_type
euclidean_domain
euclidean_domain.gcd
euclidean_domain.lcm
euclidean_domain.xgcd_aux
except_t.call_cc
except_t.mk_label
except_t.pass_aux
exists.classical_rec_on
exists_eq_elim
exists_forall_ge_and
exists_gpow_eq_one
exists_mem_ne_zero_of_dim_pos
exists_pow_eq_one
expr.flip_eq
expr.flip_iff
expr.get_pis
ext_param
ext_param_type
field.closure
field.direct_limit.discrete_field
field.direct_limit.field
field.direct_limit.inv
filter
filter.Liminf
filter.Liminf_le_Liminf
filter.Liminf_le_Liminf_of_le
filter.Liminf_le_Limsup
filter.Liminf_le_of_le
filter.Limsup