forked from siddhartha-gadgil/LeanAide
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathOmitted15.lean
101 lines (101 loc) · 5.37 KB
/
Omitted15.lean
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
import Mathlib
#check CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv
#check CategoryTheory.CosimplicialObject.Augmented.whiskering.proof_3
#check ContMDiffMap.comp.proof_1
#check StarSubalgebra.subtype.proof_6
#check AffineMap.instAddTorsorAffineMapAddGroupIsAddTorsorToAddGroupAffineMapToAddGroupInstAddCommGroupAffineMapAddGroupIsAddTorsorToAddGroup.proof_2
#check AlgebraicGeometry.Scheme.affineBasisCoverRing.proof_4
#check SimplicialObject.Split.nondegComplexFunctor.proof_3
#check LeftInvariantDerivation.mk.inj
#check CategoryTheory.Triangulated.Octahedron.comm₂_assoc
#check CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily.proof_5
#check ContMDiffAt.cle_arrowCongr
#check CategoryTheory.Limits.coconeOfCoconeUncurry.proof_2
#check ContinuousLinearMap.bilinearComp_apply
#check CategoryTheory.evaluationLeftAdjoint.proof_8
#check CategoryTheory.Under.pushout.proof_6
#check Pretrivialization.continuousLinearMap.proof_6
#check HomologicalComplex.coneOfHasLimitEval.proof_5
#check CategoryTheory.Limits.preservesColimitOfPreservesCoequalizersAndCoproduct.proof_11
#check BilinForm.dualSubmoduleToDual.proof_5
#check polarCoord.proof_8
#check IsROrC.complexRingEquiv.proof_4
#check CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFrom.proof_2
#check CategoryTheory.ShortComplex.isColimitOfIsColimitπ.proof_3
#check AddSubgroup.instAddActionElemSetLeftTransversalsCoeAddSubgroupInstSetLikeAddSubgroupToAddMonoidToSubNegAddMonoid.proof_2
#check CategoryTheory.evaluationRightAdjoint.proof_10
#check CochainComplex.mappingCone.map_comp_assoc
#check CategoryTheory.GradedObject.mapTrifunctorObj.proof_3
#check CochainComplex.mkAux.proof_1
#check CategoryTheory.GradedObject.mapTrifunctorMap.proof_3
#check CategoryTheory.OplaxFunctor.comp.proof_2
#check Trivialization.continuousLinearMap
#check AddMonoidHom.addCommMonoid.proof_8
#check Function.Injective.field.proof_1
#check CategoryTheory.ComposableArrows.isoMk
#check CategoryTheory.Limits.Cocones.precomposeEquivalence.proof_5
#check CategoryTheory.Pseudofunctor.mk.injEq
#check ZMod.commRing.proof_25
#check Perfection.lift.proof_5
#check PresheafOfModules.Hom.instAddCommGroupHomPresheafOfModulesToQuiverToCategoryStructInstCategoryPresheafOfModules.proof_6
#check PerfectClosure.instAddCommGroup.proof_10
#check ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl.proof_6
#check CategoryTheory.Endofunctor.algebraPreadditive.proof_5
#check Trivialization.continuousLinearMap.proof_9
#check Types.monoOverEquivalenceSet.proof_9
#check Magma.AssocQuotient.instSemigroupAssocQuotient.proof_3
#check HomologicalComplex.singleMapHomologicalComplex.proof_5
#check ExteriorAlgebra.liftAlternating.proof_8
#check HomologicalComplex.dgoToHomologicalComplex.proof_4
#check ContinuousLinearEquiv.arrowCongrSL.proof_8
#check ContinuousLinearMap.projKerOfRightInverse_comp_inv
#check CategoryTheory.Sieve.instCompleteLatticeSieve.proof_12
#check ZMod.commRing.proof_14
#check PiCountable.metricSpace.proof_8
#check Function.Injective.linearOrderedField.proof_1
#check WeakDual.gelfandTransform.proof_7
#check LieAlgebra.rootSpaceWeightSpaceProduct.proof_7
#check MeasureTheory.integrableOn_condexpL2_of_measure_ne_top
#check AffineMap.instAddTorsorAffineMapAddGroupIsAddTorsorToAddGroupAffineMapToAddGroupInstAddCommGroupAffineMapAddGroupIsAddTorsorToAddGroup.proof_3
#check MultilinearMap.currySumEquiv.proof_6
#check CategoryTheory.evaluationRightAdjoint.proof_9
#check Monoid.CoprodI.lift.proof_3
#check CategoryTheory.Endofunctor.coalgebraPreadditive.proof_13
#check CategoryTheory.presheafHomSectionsEquiv.proof_3
#check CategoryTheory.ComposableArrows.IsComplex.zero'_assoc
#check PiTensorProduct.lift.proof_8
#check CategoryTheory.Comonad.coalgebraPreadditive.proof_5
#check AddCommGroupCat.Colimits.instAddCommGroupColimitType.proof_16
#check CategoryTheory.Quotient.preadditive.proof_10
#check SmoothMap.addGroup.proof_8
#check CategoryTheory.functorCategoryPreadditive.proof_16
#check TensorProduct.toMatrix_assoc
#check AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.proof_2
#check CategoryTheory.GradedObject.mapTrifunctorObj.proof_5
#check Homeomorph.changeInv.proof_3
#check CategoryTheory.ComposableArrows.homMk₄_app_two
#check Surreal.orderedAddCommGroup.proof_16
#check SchwartzMap.mkCLM
#check CategoryTheory.ComposableArrows.isoMkSucc
#check CategoryTheory.Presheaf.isSheafForIsSheafFor'.proof_9
#check LinearEquiv.trans_apply
#check CategoryTheory.ComposableArrows.isoMkSucc.proof_9
#check MultilinearMap.curryLeft.proof_5
#check SSet.horn.proof_3
#check CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.proof_8
#check MultilinearMap.currySumEquiv.proof_7
#check Homotopy.mkCoinductive.proof_1
#check hfdifferential.proof_8
#check MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left'
#check MulAut.instGroupMulAut.proof_10
#check Equiv.Set.rangeSplittingImageEquiv.proof_4
#check Function.Injective.field.proof_20
#check CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitUnivLE_of_maxSmall_self.proof_9
#check CategoryTheory.evaluationRightAdjoint.proof_8
#check CategoryTheory.Limits.preservesLimitOfPreservesEqualizersAndProduct.proof_12
#check Submodule.Quotient.equiv.proof_10
#check ModuleCat.RestrictionCoextensionAdj.app'.proof_4
#check LinearEquiv.arrowCongr.proof_6
#check SmoothMap.compLeftMonoidHom
#check CategoryTheory.Limits.coconeEquivalenceOpConeOp.proof_10
#check Ideal.quotientToQuotientRangePowQuotSucc_mk