Equiv

📁 Source: MathlibTest/Equiv.lean

Statistics

Metric	Count
Definitions Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv, Equiv	13
Theorems	0
Total	13

AddGroupExtension

Definitions

Name	Category	Theorems
Equiv 📖	CompData	12 math math: Equiv.refl_apply, Equiv.map_inl, Equiv.trans_apply, Equiv.refl_symm_apply, Equiv.symm_symm_apply, Equiv.coe_symm, Equiv.toAddEquiv_eq_coe, Section.equivComp_apply, Equiv.trans_symm_apply, Equiv.coe_toAddEquiv, Equiv.rightHom_map, Equiv.instAddEquivClass

Computation

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	9 math math: Equiv.refl, Stream'.WSeq.head_congr, equiv_pure_of_mem, Stream'.WSeq.get?_congr, equiv_of_mem, think_equiv, lift_eq_iff_equiv, thinkN_equiv, Equiv.equivalence

FirstOrder.Language

Definitions

Name	Category	Theorems
Equiv 📖	CompData	36 math math: PartialEquiv.toEmbedding_apply, Equiv.map_fun, Equiv.bijective, Equiv.symm_apply_apply, Equiv.injective_toEmbedding, Equiv.coe_toElementaryEmbedding, Equiv.symm_bijective, Equiv.refl_apply, Equiv.ext_iff, Equiv.map_constants, PartialEquiv.le_iff, Embedding.substructureEquivMap_apply, Equiv.apply_symm_apply, Equiv.surjective, Equiv.injective_comp, Equiv.injective, PartialEquiv.toEquiv_inclusion_apply, empty.nonempty_equiv_iff, Equiv.map_rel, IsFraisseLimit.nonempty_equiv, Equiv.instStrongHomClass, Equiv.toFun_inducedStructureEquiv, Equiv.comp_right_injective, Equiv.coe_injective, Substructure.coe_topEquiv, Equiv.coe_toHom, PartialEquiv.symm_apply, DirectLimit.Equiv_isup_of_apply, Equiv.comp_apply, PartialEquiv.toEmbeddingOfEqTop_apply, DirectLimit.Equiv_isup_symm_inclusion_apply, Equiv.coe_toEmbedding, PartialEquiv.ext_iff, Equiv.toFun_inducedStructureEquiv_Symm, Embedding.equivRange_apply, StrongHomClass.toEquiv_toFun

GroupExtension

Definitions

Name	Category	Theorems
Equiv 📖	CompData	12 math math: Equiv.toMulEquiv_eq_coe, Equiv.symm_symm_apply, Equiv.map_inl, Equiv.refl_apply, Equiv.coe_symm, Equiv.instMulEquivClass, Equiv.refl_symm_apply, Equiv.coe_toMulEquiv, Equiv.rightHom_map, Section.equivComp_apply, Equiv.trans_apply, Equiv.trans_symm_apply

HahnSeries.SummableFamily

Definitions

Name	Category	Theorems
Equiv 📖	CompOp	3 math math: Equiv_toFun, smul_eq, hsum_equiv

Lists

Definitions

Name	Category	Theorems
Equiv 📖	CompData	4 math math: Lists'.mem_def, equiv_atom, Lists'.mem_cons, Equiv.antisymm_iff

Ordnode

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	1 math math: equiv_iff

PSet

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	17 math math: mem_singleton, equiv_of_isEmpty, equiv_iff_mem, Equiv.refl, mem_def, Equiv.ext, equiv_iff, Equiv.comm, Equiv.rfl, Ordinal.mem_toPSet_iff, ZFSet.eq, Mem.ext, Equiv.eq, equiv_empty, mem_pair, ZFSet.exact, mem_insert_iff

RelSeries

Definitions

Name	Category	Theorems
Equiv 📖	CompOp	—

RootPairing

Definitions

Name	Category	Theorems
Equiv 📖	CompData	6 math math: Equiv.toHom_one, Equiv.coweightEquiv_one, Equiv.weightEquiv_inv, Equiv.coweightEquiv_inv, Equiv.mul_eq_comp, Equiv.weightEquiv_one

SetTheory.PGame

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	1 math math: instIsEquivEquiv

Stream'.WSeq

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	14 math math: Equiv.refl, Equiv.ext, join_ret, bind_ret, join_append, Equiv.equivalence, destruct_congr_iff, bind_assoc_comp, join_join, join_map_ret, ret_bind, bind_assoc, think_equiv, flatten_equiv

(root)

Definitions

Name	Category	Theorems
Equiv 📖	CompData	6173 math, 2 bridge math: Equiv.Perm.decomposeFin_symm_of_refl, Prod.Lex.toLex_lt_toLex', Equiv.sumEmpty_symm_apply, SSet.OneTruncation₂.nerveEquiv_apply, CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right, DirectSum.decompose_sub, OrderDual.isBounded_preimage_toDual, SymAlg.unsym_comp_sym, MultilinearMap.domDomCongrLinearEquiv'_symm_apply, CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv, UniformConvergenceCLM.isEmbedding_coeFn, SSet.op_δ, AddMonoidAlgebra.singleHom_apply, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', FreeAddMonoid.lift_symm_apply, CategoryTheory.Limits.Fork.IsLimit.homIso_natural, AffineEquiv.coe_symm_toEquiv, pow_ofDual, isCompl_toDual_iff, nndist_ofMul, NumberField.basisMatrix_eq_embeddingsMatrixReindex, LinearEquiv.coe_toEquiv, CategoryTheory.Functor.functorHomEquiv_apply_app, DomMulAct.smul_monoidHom_apply, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', WithBot.coe_toDualTopEquiv_eq, CategoryTheory.Quiv.equivOfIso_symm_apply, CategoryTheory.PreZeroHypercover.isoMk_hom_h₀, WithBot.ofDual_map, WithZero.logOrderIso_apply, ContinuousMap.isUniformInducing_equivBoundedOfCompact, CategoryTheory.Functor.map_homCongr, CategoryTheory.nerve.edgeMk_edge, LinearMap.restrictScalars_toMatrix, Matrix.comp_diagonal_diagonal, SupBotHom.dual_comp, WithTop.map_ofDual, Equiv.sumAssoc_symm_apply_inl, CategoryTheory.uliftCoyonedaEquiv_apply, CategoryTheory.TwoSquare.equivNatTrans_symm_apply, unitsEquivNeZero_symm_apply, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Equiv.prodSumDistrib_apply_left, Matrix.natCast_kronecker, AddCircle.coe_equivIco_mk_apply, FreeMonoid.map_apply_map_symm_eq, Finset.Colex.toColex_le_singleton, Finsupp.mulHom_ext'_iff, Equiv.invFun_as_coe, CategoryTheory.mateEquiv_counit_symm, IsUpperSet.ofDual, HahnModule.support_smul_subset_vadd_support', PEquiv.vecMul_toMatrix_toPEquiv, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, CategoryTheory.Functor.natTransEquiv_apply_app, CategoryTheory.Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, Equicontinuous.inducing_uniformFun_iff_pi, CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc, CategoryTheory.coyonedaEquiv_symm_app_apply, SetTheory.PGame.default_nim_one_rightMoves_eq, Field.Emb.Cardinal.equivLim_coherence, CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft, Equiv.Perm.subtypePerm_mul, MulChar.equivToUnitHom_mul_apply, SymmetricAlgebra.lift_ι_apply, isSublattice_preimage_ofDual, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm, Matrix.vecMulVec_empty, toLex_sub, CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm, Matrix.replicateCol_cons, FreeMonoid.freeMonoidCongr_of, Topology.lawsonClosed_of_lowerClosed, FirstOrder.Language.LEquiv.onTerm_symm_apply, PiTensorProduct.lift_reindex, AddSubgroup.quotientEquivProdOfLE_symm_apply, reindex_mem_doublyStochastic, CategoryTheory.Functor.homObjEquiv_apply_app, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three_assoc, CategoryTheory.CoreSmallCategoryOfSet.functor_obj, LocallyConstant.congrRight_apply, PerfectionMap.lift_symm_apply, AddMonoidAlgebra.lift_apply', addMonoidAlgebraEquivDirectSum_apply, ofBoolRing_one, Order.IsSuccPrelimit.dual, CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_apply_coe, MonoidAlgebra.liftMagma_apply_apply, AddChar.toMonoidHomEquiv_zero, QuaternionAlgebra.coe_linearEquivTuple_symm, WithCStarModule.equiv_add, ofDual_toAdd_zero, DomAddAct.mk_vadd_indicatorConstLp, Equiv.sigmaAssocProd_apply_fst, List.Nodup.getEquiv_apply_coe, NonemptyInterval.dual_map, Nat.divModEquiv_apply, FreeAddMonoid.toList_sum, Matrix.transposeInvertibleEquivInvertible_symm_apply, Equiv.subtypeUnivEquiv_apply, CategoryTheory.Arrow.equivSigma_symm_apply_left, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, DFA.reindex_apply_accept, OrderDual.ofDual_le_ofDual, Equiv.equiv_subsingleton_cod, CategoryTheory.conjugateEquiv_iso, Equiv.prodCongrLeft_apply_snd, Metric.Snowflaking.uniformContinuous_ofSnowflaking, WithBot.lt_ofDual_iff, Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex, Equiv.coe_vaddConst, ofAdd_multiset_prod, WithZero.val_expOrderIso_apply, InfTopHom.symm_dual_id, DirectSum.Decomposition.decompose'_eq, IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply, isLeftRegular_ofColex, Subgroup.IsComplement.equiv_fst_eq_iff_leftCosetEquivalence, CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval, Equiv.ulift_apply, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, IndexedPartition.proj_fiber, AffineEquiv.coe_toEquiv, Equiv.plift_apply, List.equivSigmaTuple_symm_apply, IntermediateField.algHomEquivAlgHomOfSplits_symm_apply, sigmaFinsuppEquivDFinsupp_support, Diffeomorph.toEquiv_injective, Nat.Primes.prodNatEquiv_symm_apply, CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp, Subgroup.quotientEquivOfEq_mk, Equiv.uniqueProd_symm_apply, CategoryTheory.Iso.eHomCongr_inv_comp_assoc, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_map, Subgroup.equivSMul_apply_coe, LinearEquiv.extendScalarsOfIsLocalizationEquiv_symm_apply, Submonoid.equivOp_symm_apply_coe, CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply, nndist_ofAdd, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, FreeMonoid.toList_prod, CircleDeg1Lift.translate_inv_apply, Equiv.inv_def, nhds_ofMul, DFinsupp.lex_lt_iff_of_unique, FreeMonoid.ofList_smul, Quiver.SingleObj.pathEquivList_nil, toLex_mul, CategoryTheory.Localization.Preadditive.homEquiv_symm_apply, FreeAddMonoid.lift_ofList, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, FundamentalGroupoid.equiv_symm_apply_as, CategoryTheory.Classifier.SubobjectRepresentableBy.pullback_homEquiv_symm_obj_Ω₀, extDeriv_constOfIsEmpty, Equiv.toPEquiv_apply, SimpleGraph.incidenceSetEquivNeighborSet_apply_coe, WithTop.toDualBotEquiv_coe, val_inv_unitsEquivProdSubtype_symm_apply, CategoryTheory.Limits.IsLimit.equivIsoLimit_apply, MeasureTheory.ComplexMeasure.equivSignedMeasure_symm_apply, IsLowerSet.ofDual, Set.dual_ordConnectedComponent, Equiv.Set.union_symm_apply_left, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, SetTheory.PGame.exists_leftMoves_neg, reindex_mem_doublyStochastic_iff, AddEquiv.addMonoidHomCongrLeftEquiv_apply, Additive.toMul_mono, Topology.IsGeneratedBy.homeomorph_symm_coe, LightCondensed.ihomPoints_apply, SetTheory.PGame.Domineering.shiftUp_apply, zpowersMulHom_symm_apply, Equiv.sumCompl_symm_apply_pos, CategoryTheory.shrinkYonedaEquiv_comp, UniformOnFun.gen_eq_preimage_restrict, Equiv.optionIsSomeEquiv_symm_apply_coe, Equiv.coe_constVSub_symm, FreeAddMonoid.count_apply, NumberField.Units.logEmbedding_fundSystem, toColex_ofColex, CategoryTheory.Subfunctor.Subpresheaf.range_eq_ofSection', Lex.forall, Matrix.abs_det_reindex, ofBoolRing_sub, nsmul_finEquivZMultiples_symm_apply, Equiv.piComm_apply, ZSpan.volume_real_fundamentalDomain, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom, UniformFun.ofFun_one, AddEquiv.toMultiplicative_apply_symm_apply, PartENat.withTopEquiv_symm_apply, AddMonoidHom.toMultiplicative_add, SimpleGraph.Walk.IsHamiltonian.getVertEquiv_apply, Rack.toEnvelGroup.univ_uniq, CategoryTheory.Functor.curryingEquiv_symm_apply_obj_obj, ContinuousAlternatingMap.norm_ofSubsingleton_id_le, Order.height_ofDual, Finsupp.curryEquiv_apply, CategoryTheory.Bicategory.conjugateEquiv_whiskerRight, IntermediateField.algHomEquivAlgHomOfSplits_apply_apply, finSumFinEquiv_apply_left, AlgebraicGeometry.coprodSpec_apply, Finsupp.equivCongrLeft_apply, SetTheory.PGame.relabel_moveLeft', CategoryTheory.iterated_mateEquiv_conjugateEquiv, strictAntiOn_toDual_comp_iff, Polynomial.Gal.smul_def, UniformOnFun.toFun_one, FreeAddMonoid.toPiTensorProduct, RootPairing.chainTopCoeff_reflectionPerm_right, MvPolynomial.comapEquiv_symm_coe, ofDual_max, Homeomorph.piCongr_apply, MulChar.toUnitHom_eq, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso, isMin_toDual_iff, LeftOrdContinuous.rightOrdContinuous_dual, toColex_sub, Hamming.toHamming_sub, WithBot.orderIsoPUnitSumLex_symm_inl, MonotoneOn.dual_left, Quiver.starEquivCostar_symm_apply_fst, OrderedFinpartition.extendEquiv_apply, CategoryTheory.Subfunctor.Subpresheaf.range_eq_ofSection, DirectSum.decompose_of_mem_same, SSet.ι₀_snd_assoc, MonoidHom.toAdditive_apply_apply, Fintype.coe_finsetEquivSet, OrderIso.coe_dualDual_symm, Additive.ofMul_eq_top, Equiv.symm_preimage_preimage, FreeAddMonoid.lift_apply, Combinatorics.Subspace.IsMono.reindex, CategoryTheory.ReflQuiv.adj.homEquiv_symm_apply, Set.Ioi_ofDual, CategoryTheory.Iso.isoCongr_symm_apply, CategoryTheory.ExponentiableMorphism.homEquiv_symm_apply_eq, StrictAntiOn.dual_left, CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from, WithTop.toDual_top, Additive.ofMul_bot, RootPairing.reflectionPerm_eq_iff_smul_root, CategoryTheory.FunctorToTypes.functorHomEquiv_symm_apply_app_app, CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm, CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val, RingEquiv.op_apply_apply, AddEquiv.addSubgroupMap_symm_apply, NumberField.Units.fun_eq_repr, SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace, ModuleCat.freeHomEquiv_apply, isLeftRegular_toLex, Bifunctor.mapEquiv_apply, Matrix.compAlgEquiv_apply, supClosed_preimage_ofDual, AddEquiv.piAdditive_apply, RelIso.toEquiv_injective, AddMonoidAlgebra.liftNCRingHom_single, CategoryTheory.CountableCategory.instObjAsType, MeasureTheory.VectorMeasure.equivMeasure_apply, Finset.uIcc_toDual, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv_symm, RootPairing.Hom.root_weightMap, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, contDiff_prodAssoc_symm, MeasureTheory.integral_domSMul, SupBotHom.symm_dual_comp, finEquivZPowers_symm_apply, CategoryTheory.shrinkYonedaEquiv_symm_map_assoc, TopHom.symm_dual_id, Multiplicative.ofAdd_eq_top, ArchimedeanOrder.le_def, AddMonoidHom.toMultiplicativeRight_apply_apply, Equiv.neg_def, Cardinal.extend_function_finite, Multiset.coe_consEquiv_of_eq_of_eq, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, Matrix.mul_mul_left, RingHom.eq_liftOfRightInverse, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, CategoryTheory.Bicategory.mateEquiv_comp_id_right, Subgroup.transferTransversal_apply, Matrix.det_det, ContinuousLinearEquiv.coe_prodAssoc, Monoid.Foldl.ofFreeMonoid_apply, AddAutAdditive_apply_symm_apply, Equiv.isHomeomorph_of_discrete, SkewMonoidAlgebra.lift_apply', Matrix.adjugate_fin_two, Topology.WithUpper.continuous_toUpper, PiTensorProduct.lift_reindex_symm, RingEquiv.asBoolRingAsBoolAlg_apply, CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_inv, ComplexShape.Embedding.AreComplementary.desc'_inl, Matrix.diagonal_vec3, orderOf_ofAdd_eq_addOrderOf, finSumEquivOfFinset_inr, Multiset.cast_symm_apply_fst, AddMonoidHom.liftOfRightInverse_comp_apply, sSupHom.symm_dual_id, ExteriorAlgebra.lift_symm_apply, PiTensorProduct.map_reindex_symm, RelIso.sumLexComplRight_apply, DFinsupp.equivFunOnFintype_symm_coe, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_comp, CategoryTheory.FunctorToTypes.shrinkMap_app, Hamming.ofHamming_zero, isAddRightRegular_ofMul, CategoryTheory.eHomEquiv_id, normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity, List.sortedGT_map_ofDual, CategoryTheory.Quiv.homEquivOfIso_symm_apply, Finset.Colex.toColex_univ, HahnModule.coeff_single_smul_vadd, FreeAddMonoid.toList_comp_ofList, InfHom.symm_dual_comp, InverseSystem.piEquivSucc_self, Finsupp.toColex_monotone, Matrix.one_kronecker, Equiv.boolArrowEquivProd_symm_apply, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', Flag.coe_map, toDegLex_inj, DirectSum.decomposeAlgEquiv_symm_apply, DFinsupp.equivProdDFinsupp_smul, CompleteLatticeHom.dual_symm_apply_toFun, Topology.WithLawson.ofLawson_toLawson, Equiv.piCongrLeft_apply, Finset.map_filter, PrimeSpectrum.primeSpectrumProd_symm_inl, TopologicalSpace.Closeds.complOrderIso_symm_apply, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', AddMagma.FreeAddSemigroup.lift_symm_apply, UniformFun.edist_eval_le, CategoryTheory.WithInitial.isColimitEquiv_apply_desc_right, OrderHom.dual_id, NumberField.IsCMField.equivInfinitePlace_symm_apply, WType.equivSigma_apply, Subgroup.equivOp_symm_apply_coe, FreeMagma.lift_of, isBot_ofDual_iff, toDual_pow, CategoryTheory.Bicategory.Adjunction.homEquiv₂_symm_apply, Quaternion.imK_equivProd_symm_apply, CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π, CartanMatrix.C_two, Finset.exists_equiv_extend_of_card_eq, MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, Lex.exists, OrderIso.sumLexIicIoi_symm_apply_of_lt, Subgroup.IsComplement.coe_equiv_snd_eq_one_iff_mem, CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj_symm_apply, FintypeCat.uSwitch_map_uSwitch_map, PiTensorProduct.reindex_reindex, CategoryTheory.Sieve.overEquiv_pullback, RootPairing.reflectionPerm_involutive, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ, pow_toColex, Matrix.abs_det_submatrix_equiv_equiv, CategoryTheory.Adjunction.homEquiv_naturality_left_square, Equiv.piOptionEquivProd_symm_apply, Cardinal.mk_preimage_equiv_lift, LightCondensed.ihomPoints_symm_comp, FirstOrder.Language.Embedding.equivRange_toEquiv_apply, WithZero.lift'_symm_apply_apply, AddSubsemigroup.coe_toSubsemigroup_symm_apply, Function.fromTypes_cons_equiv_symm_apply, sInfHom.dual_id, Polynomial.sylvester_comm, Finset.Ioi_toDual, AntivaryOn.dual, Pi.toColex_monotone, Equiv.apply_symm_apply, toLex_inj, CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def, ofColex_one, Equiv.piSplitAt_symm_apply, AddSubgroup.mem_toSubgroup', Topology.WithUpperSet.toUpperSet_inj, SSet.stdSimplex.obj₀Equiv_symm_apply, CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition', Prod.Lex.lt_iff', Pi.colex_asc, Matrix.reindex_mem_colStochastic_iff, tangentMap_chart, FreeMonoid.lift_restrict, SSet.OneTruncation₂.nerveHomEquiv_id, DomMulAct.symm_mk_pow, SupHom.dual_id, Order.succ_toAdd, Set.up_union, DomMulAct.smul_linearMap_apply, Multiset.coe_subsingletonEquiv, Multiplicative.toAdd_image_setMul, Metric.Snowflaking.preimage_ofSnowflaking_closedBall, Equiv.restrictPreimageFinset_symm_apply_coe, isTop_toDual_iff, CategoryTheory.Bicategory.mateEquiv_vcomp, OrderMonoidIso.withZero_symm_apply_symm_apply, SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe, IsCyclic.val_mulAutMulEquiv_apply, CategoryTheory.ShrinkHoms.id_def, equivShrink_symm_div, toMul_uzpow, CategoryTheory.conjugateEquiv_symm_id, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, even_ofMul_iff, dist_toDual, CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right_symm, OrderDual.instNeBotNhdsWithinIio, CategoryTheory.Bicategory.conjugateEquiv_adjunction_id_symm, Equiv.piCongrSigmaFiber_symm_apply, OrderMonoidIso.withZero_symm_apply_apply, AddSubgroup.IsComplement.quotientAddGroupMk_leftQuotientEquiv, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, DomAddAct.map_mk_symm_nhds, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, TensorAlgebra.ι_comp_lift, CategoryTheory.nerve.functorOfNerveMap_map, isSquare_toMul_iff, StandardEtalePair.homEquiv_symm_apply, SSet.opFunctorCompOpFunctorIso_inv_app_app, equivEquivIso_hom, Matrix.diagonal_fin_two, Disjoint.dual, strictAntiOn_comp_ofDual_iff, UniformOnFun.uniformContinuous_ofUniformFun, Equiv.refl_apply, MulEquiv.toAdditive_apply_apply, AddMonoidAlgebra.mapDomainAddEquiv_single, finEquivPowers_apply, Complex.lipschitz_equivRealProd, Prod.Lex.compare_def, Topology.WithLawson.isOpen_preimage_ofLawson, Equiv.piCongr_apply_apply, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Action.diagonalSuccIsoTensorDiagonal_inv_hom, FreeAddSemigroup.lift_comp_of, Equiv.sumAssoc_apply_inr, finCongr_apply, Equiv.arrowCongr'_apply, AddEquiv.toMultiplicativeRight_apply_apply, Cardinal.mk_equiv_le_embedding, strictMono_dual_iff, Equiv.sigmaSigmaSubtypeEq_apply, PreQuasiregular.equiv_symm_apply, CliffordAlgebra.lift_ι_apply, Equiv.subtypeEquivRight_apply_coe, OrderDual.ofDual_bot, DualNumber.range_lift, CategoryTheory.Limits.biproduct.whiskerEquiv_inv, MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero, AddCircle.equivIccQuot_comp_mk_eq_toIcoMod, SSet.Subcomplex.range_eq_ofSimplex, MulHom.op_symm_apply_apply, pow_toLex, AddEquiv.additiveMultiplicative_apply, FreeAlgebra.lift_comp_ι, Matrix.toSquareBlock_def, IsMinFilter.dual, CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_φ, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_f, CofiniteTopology.continuous_of, sigmaFinsuppAddEquivDFinsupp_apply, toBoolRing_inf, Equiv.mulLeft₀_apply, Set.dual_ordConnectedSection, WithLp.coe_congr, SupIrred.ofDual, Matrix.submatrix_vecMul_equiv, TwoSidedIdeal.equivMatrix_symm_apply_ringCon, DFA.comap_reindex, Homeomorph.homeomorph_mk_coe, RelIso.relHomCongr_symm_apply, MulEquiv.piMultiplicative_apply, Equiv.Perm.perm_symm_on_of_perm_on_finset, Set.Ioc_ofDual, RootPairing.reflectionPerm_sq, Equiv.sigmaCongrLeft_apply, CategoryTheory.Functor.RepresentableBy.homEquiv_eq, Equiv.divRight_symm_apply, CoxeterSystem.lift_apply_simple, OrderIso.invENNReal_symm_apply, IsSymmetricAlgebra.equiv_apply, PresheafOfModules.homEquivOfIsLocallyBijective_symm_apply, DomMulAct.coe_mkHomeomorph_symm, supIrred_ofDual, CategoryTheory.SingleObj.mapHom_id, Prod.Lex.monotone_fst, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, Matrix.charmatrix_reindex, NumberField.Units.regOfFamily_eq_det, ofDual_inf, Equiv.prod_assoc_image, CartanMatrix.D_four, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left, equivShrink_symm_sub, Complex.equivRealProd_apply, WithTop.lt_toDual_iff, CategoryTheory.ShiftedHom.opEquiv_symm_add, Equiv.sigmaPreimageEquiv_symm_apply_snd_coe, ofBoolAlg_inj, RingHom.liftOfSurjective_comp, MeasureTheory.volume_measurePreserving_piCongrLeft, isCompl_ofDual_iff, finSuccEquiv_zero, Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, ModuleCat.Iso.homCongr_eq_arrowCongr, OrderIso.neg_apply, UniformOnFun.ofFun_sum, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm_assoc, WithOne.lift_coe, toMul_ofMul, toLex_ofNat, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left, CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ, CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit, VertexOperator.of_coeff_apply_coeff, DomMulAct.smul_mulDistribActionHom_apply, IndexedPartition.equivQuotient_symm_proj_apply, MeasureTheory.Measure.domSMul_apply, CategoryTheory.Limits.opCompYonedaSectionsEquiv_symm_apply_coe, norm_ofAdd, Multiplicative.ofAdd_le, Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe, Specialization.ofEquiv_toEquiv, AddConstMap.coe_addLeftHom_apply, UniformOnFun.uniformContinuous_eval, CategoryTheory.Limits.yonedaCompLimIsoCocones_inv_app, Equiv.coe_fn_symm_mk, CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true, CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, Equiv.sumIsRight_apply, genericPoints.equiv_symm_apply, BoundedLatticeHom.dual_id, DomAddAct.isOpenEmbedding_mk, Quiver.SingleObj.toPrefunctor_symm_id, BoundedOrderHom.symm_dual_id, SSet.S.equivElements_symm_apply_dim, PEquiv.toMatrix_toPEquiv_mulVec, Sym.coe_equivNatSumOfFintype_apply_apply, toDegLex_injective, DFinsupp.equivFunOnFintype_single, PartENat.withTopEquiv_one, toColex_vadd, Finsupp.equivFunOnFinite_apply, MvPolynomial.comapEquiv_coe, StrictAntiOn.dual, CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_symm_apply_val, Equiv.sigmaAssocProd_apply_snd_snd, IntermediateField.algHomEquivAlgHomOfSplits_apply, UniformOnFun.ofFun_toFun, Homeomorph.piCongrLeft_symm_apply, Bundle.TotalSpace.toProd_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm_assoc, Matrix.kroneckerMap_reindex_right, RootPairing.Hom.root_weightMap_apply, AddMonoidAlgebra.mapDomainAddEquiv_apply, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str, AlgEquiv.op_apply_apply, Equiv.permCongr_symm_apply, Equiv.vanishesTrivially_comp, toDual_vadd', CategoryTheory.Functor.FullyFaithful.homEquiv_apply, ofLex_add, Pi.single_comp_equiv, MeasureTheory.Measure.pi_map_piCongrLeft, Shrink.linearEquiv_symm_apply, finsum_comp_equiv, isRightRegular_ofLex, WithTop.le_toDual_iff, LieAlgebra.lieCharacterEquivLinearDual_apply, DFinsupp.toLex_monotone, LieAlgebra.of_smul, WithCStarModule.equiv_symm_snd, Rep.to_Module_monoidAlgebra_map_aux, CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_id, toLex_eq_one, Equiv.exists_congr_right, CategoryTheory.tensorRightHomEquiv_symm_naturality, toColex_inv, isUpperSet_preimage_toDual_iff, SetTheory.PGame.add_moveLeft_inl, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, CliffordAlgebra.range_lift, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply, PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal, Matrix.kroneckerTMul_assoc', SSet.horn.yonedaEquiv_ι, Multiset.coeEquiv_apply_coe, Codisjoint.dual, Antitone.dual_right, DomMulAct.mem_stabilizer_iff, RelIso.map_rel_iff', Monoid.CoprodI.lift_of, CategoryTheory.conjugateEquiv_symm_comp_assoc, CategoryTheory.Limits.coyonedaCompLimIsoCones_inv_app, Delone.DeloneSet.mapIsometry_trans, Sym.coe_equivNatSum_apply_apply, isMinOn_dual_iff, Specialization.isOpen_toEquiv_preimage, Equiv.withBotCongr_apply, CategoryTheory.Subfunctor.ofSection_eq_range, Equiv.symm_comp_self, Equiv.ofLeftInverse_apply_coe, SemimoduleCat.Iso.homCongr_eq_arrowCongr, Sequential.isoEquivHomeo_apply, SimpleGraph.Iso.connectedComponentEquiv_symm_apply, Equiv.exists_congr_left, List.SortedLT.of_map_ofDual, toMul_neg, CategoryTheory.Localization.SmallHom.equiv_equiv_symm, WithBot.ofDual_le_iff, ofLex_ratCast, BialgEquiv.coe_toEquiv, CommRing.Pic.mul_eq_tensor, ArchimedeanClass.FiniteResidueField.mk_eq_zero, Equiv.Perm.symm_mul, affineIndependent_equiv, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv, Equiv.finsuppUnique_symm_apply_support_val, ContinuousMap.val_unitsLift_apply_apply, Equiv.semiconj_conj, Equiv.divLeft_involutive, zpowersHom_symm_apply, Finset.map_ofDual_max, toColex_add, Cardinal.mk_preimage_equiv, RelIso.sumLexComplLeft_symm_apply, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply, Finset.Colex.toColex_lt_toColex_iff_max'_mem, UniformOnFun.isometry_restrict, GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity, Sequential.isoEquivHomeo_symm_apply, optionProdEquiv_symm_inr, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one, Pi.ofLex_apply, Equiv.Set.rangeInl_symm_apply_coe, Equiv.embeddingEquivOfFinite_apply, LinearMap.toMatrixOrthonormal_reindex, autEquivZmod_symm_apply_natCast, CategoryTheory.ForgetEnrichment.equivFunctor_map, Finset.image_univ_equiv, Lat.dual_map, ofDual_iInf, Equiv.boolNot_apply, HVertexOperator.coeff_isPWOsupport, StarAlgHom.prodEquiv_apply, Sum.Lex.inr_le_inr_iff, contMDiff_equivTangentBundleProd_symm, finSuccEquiv_symm_none, AddChar.directSum_apply, FreeGroup.lift_of_eq_id, InfTopHom.symm_dual_comp, FreeMonoid.countP_of, SheafOfModules.unitHomEquiv_symm_comp, Matrix.mul_val_succ, Fin.insertNthEquiv_apply, CategoryTheory.yonedaEquiv_apply, finSuccEquiv_succ, equivShrink_top, Subgroup.IsComplement.equiv_one, WithBot.orderIsoPUnitSumLex_symm_inr, ofAdd_toAdd, Matrix.kroneckerMap_assoc₁, CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp, OrderDual.toDual_le_toDual, uliftMultiplesHom_symm_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, CategoryTheory.Localization.LeftBousfield.galoisConnection, MonoidHom.coe_toMultiplicative_range, CategoryTheory.FreeGroupoid.functorEquiv_apply, CategoryTheory.ForgetEnrichment.equivInverse_map, OrderIso.subLeft_apply, FirstOrder.Language.Term.constantsVarsEquiv_symm_apply, DirectSum.lequivCongrLeft_apply, Equiv.comp_surjective, Topology.WithLowerSet.ofLowerSet_inj, toDual_sInf, Equiv.prodPiEquivSumPi_apply, CategoryTheory.Functor.Final.colimitCoconeOfComp_isColimit, Sym2.lift_comp_map, CategoryTheory.Functor.equivCatHom_symm_apply, NonUnitalStarAlgHom.prodEquiv_symm_apply, contDiff_prodAssoc, DomMulAct.smul_addMonoidHom_apply, FreeMonoid.ofList_append, Orientation.map_of_isEmpty, Finsupp.equivMapDomain_single, SymAlg.sym_bijective, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply, CategoryTheory.InducedCategory.homEquiv_apply, LinOrd.dual_map, CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str, CategoryTheory.Bicategory.Adjunction.homEquiv₁_apply, AddAction.stabilizer_vadd_eq_stabilizer_map_conj, SetSemiring.up_lt_up, groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁, Homeomorph.toEquiv_piCongr, OrderIso.sumLexIioIci_symm_apply_Ici, SymAlg.sym_neg, Matrix.diagonal_vec1, CategoryTheory.Limits.WidePullbackCone.reindex_pt, Int.divModEquiv_apply, Finset.ofDual_inf, OrderIso.dualAntisymmetrization_symm_apply, Finsupp.Lex.single_strictAnti, RootPairing.Hom.comp_indexEquiv_symm_apply, SymAlg.sym_zero, CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation, FreeAddSemigroup.lift_symm_apply, Multiplicative.toAdd_mono, groupCohomology.mem_cocycles₁_of_addMonoidHom, RingHom.liftOfSurjective_comp_apply, Equiv.coe_toEmbedding, SSet.Subcomplex.Pairing.dim_p, norm_ofMul, Module.Basis.equiv_apply, Equiv.piCongrSet_apply, Abelianization.lift_unique, Affine.Simplex.excenterWeightsUnnorm_reindex, Equiv.toPartialEquiv_apply, Fin.consEquiv_apply, FintypeCat.equivEquivIso_apply_hom, Equiv.piSplitAt_apply, Set.opEquiv_apply, CategoryTheory.InjectiveResolution.of_def, DistLat.dual_map, Equiv.Set.image_apply, ModuleCat.extendRestrictScalarsAdj_homEquiv_apply, QuotientAddGroup.equivIocMod_zero, FreeAbelianGroup.lift_add, Additive.ofMul_top, Equiv.piCongrRight_symm_apply, CategoryTheory.Coyoneda.objOpOp_inv_app, CategoryTheory.GradedObject.comapEquiv_counitIso, SheafOfModules.freeHomEquiv_freeMap, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, Orientation.volumeForm_map, WCovBy.toDual, IsBot.toDual, Matrix.blockTriangular_transvection', Finset.Colex.le_iff_max'_mem, CategoryTheory.Iso.homCongr_trans, RingEquiv.op_apply_symm_apply, CategoryTheory.Subobject.wideCospan_map_term, CategoryTheory.FunctorToTypes.binaryProductEquiv_apply, BotHom.dual_apply_apply, AddMonoidAlgebra.lift_mapRangeRingHom_algebraMap, RingEquiv.piCongrLeft_symm_apply, ofMul_list_prod, Homeomorph.toEquiv_piCongrLeft, ofLex_sub, Equiv.traverse_def, UniformFun.uniformSpace_eq_iInf_precomp_of_cover, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, Equiv.Perm.permCongr_eq_mul, LinearMap.IsSymmetric.directSum_decompose_apply, CategoryTheory.Limits.IsColimit.equivIsoColimit_apply, FreeNonUnitalNonAssocAlgebra.of_comp_lift, SSet.opFunctorCompOpFunctorIso_hom_app_app, AddAutAdditive_apply_apply, finTwoArrowEquiv'_apply, CategoryTheory.Functor.FullyFaithful.isoEquiv_apply, CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_apply_coe, Matrix.lift_cRank_submatrix, NonemptyInterval.toLex_strictMono, UniversalEnvelopingAlgebra.lift_unique, Equiv.trans_apply, Finset.Colex.cons_lt_cons, CategoryTheory.CommSq.instHasLift, SetSemiring.imageHom_def, Finset.Nat.antidiagonalEquivFin_symm_apply_coe, Order.succ_ofAdd, Finset.Colex.toColex_sdiff_le_toColex_sdiff', Equiv.subtypeEquivCodomain_symm_apply, Matrix.sum_sum_single, AddMonoid.Coprod.neg_def, Equiv.left_inv', Opposite.equivToOpposite_coe, Fin.snocEquiv_apply, Cardinal.mk_eq_nat_iff, Metric.PiNatEmbed.toPiNatEquiv_apply_ofPiNat, Equiv.sumSigmaDistrib_symm_apply, CategoryTheory.Presheaf.freeYonedaHomEquiv_comp, MonoidHom.toHomPerm_apply_symm_apply, Equiv.sigmaPUnit_symm_apply_snd, Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst, DFinsupp.subtypeSupportEqEquiv_apply_coe, Subgroup.quotientEquivProdOfLE_apply, Equiv.optionEquivSumPUnit_symm_inr, Fintype.card_equiv, CategoryTheory.Pi.equivalenceOfEquiv_unitIso, MvPolynomial.supDegree_esymmAlgHomMonomial, ofDual_min, CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc, Equiv.eq_symm_comp, TopologicalSpace.Opens.complOrderIso_apply, Colex.forall, Equiv.piCongrLeft_preimage_univ_pi, monotoneOn_comp_ofDual_iff, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply, CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply, CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_apply, OrderIso.inv_symm_apply, CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_symm_apply, RingEquiv.piCongrLeft'_apply, Equiv.ofFiberEquiv_map, FreeMonoid.toList_mul, CompleteLatticeHom.dual_id, toDual_smul', Subsemigroup.equivOp_symm_apply_coe, NonemptyInterval.coe_dual, AddMonoidHom.coe_toMultiplicativeRight, Metric.Snowflaking.toSnowflaking.sizeOf_spec, CategoryTheory.Pi.equivalenceOfEquiv_counitIso, PresheafOfModules.freeYonedaEquiv_symm_app, CategoryTheory.Limits.biproduct.matrixEquiv_symm_apply, Equiv.bijective, ofLex_intCast, ofBoolAlg_inf, Equiv.piCongrLeft_symm_apply, Prod.Lex.monotone_fst_ofLex, Sym2.sortEquiv_apply_coe, Multiplicative.ofAdd_lt, AddSubmonoid.coe_toSubmonoid_apply, Representation.asAlgebraHom_def, DomMulAct.continuous_mk, FreeLieAlgebra.of_comp_lift, Ordinal.one_toPGame_leftMoves_default_eq, Multiplicative.ofAdd_image_setAdd, CategoryTheory.tensorLeftHomEquiv_naturality, Homeomorph.coe_symm_toEquiv, isRegular_toLex, IsometryEquiv.piCongrLeft'_apply, Matrix.eRank_submatrix, CStarMatrix.ofMatrix_apply, ofAdd_zero, CategoryTheory.FinCategory.categoryAsType_comp, Sum.Lex.inr_strictMono, SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, DFinsupp.equivFunOnFintype_apply, SetTheory.PGame.relabel_moveRight, AddMonoidAlgebra.divOfHom_apply_apply, FirstOrder.Language.Term.constantsVarsEquivLeft_apply, UniformOnFun.toFun_ofFun, CategoryTheory.leftAdjointOfStructuredArrowInitialsAux_symm_apply, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_left, RootPairing.Equiv.id_indexEquiv_apply, toBoolRing_ofBoolRing, SymAlg.unsym_mul, TwoSidedIdeal.equivMatrix_apply, CategoryTheory.Bicategory.conjugateEquiv_symm_id, uliftZPowersHom_symm_apply, Equiv.divLeft_symm_apply, Orientation.map_eq_neg_iff_det_neg, ofColex_div, UniformFun.toFun_sub, Unitization.starLift_symm_apply_apply, Maximal.dual, nnnorm_toMul, UniformOnFun.toFun_neg, AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_symm_apply_coe, UniformEquiv.coe_toEquiv, Equiv.ofBijective_apply_symm_apply, Matrix.kroneckerMap_reindex, Nat.pairEquiv_apply, CategoryTheory.Limits.Bicone.whisker_pt, WithZero.coe_expEquiv_apply, toAdd_mul, CategoryTheory.Bicategory.conjugateEquiv_apply, Unitization.starLift_apply_apply, CategoryTheory.Adjunction.eq_homEquiv_apply, Topology.WithLower.toLower_inj, DirectSum.decompose_eq_mul_idempotent, AddAutAdditive_symm_apply_symm_apply, FreeMonoid.toList_nil, SSet.prodStdSimplex.objEquiv_apply_fst, isRight_finSumNatEquiv_symm_apply, MonoidHom.fiberEquivKer_symm_apply, ofDual_ofNat, MvPolynomial.rename_msymm, Equiv.arrowCongr_apply, ClosureOperator.conjBy_apply, LinearEquiv.coe_symm_toEquiv, CategoryTheory.MonObj.ofRepresentableBy_one, Quiver.starEquivCostar_apply_fst, Equiv.Perm.sum_comp', Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, Prod.Lex.toLexOrderHom_coe, UniformOnFun.lipschitzWith_one_ofFun_toFun, FreeGroup.lift_apply_of, UniformFun.toFun_ofFun, CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π, Prod.Lex.toLex_le_toLex', Function.FromTypes.curry_two_eq_curry, HahnSeries.support_abs, CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj_apply, ofColex_add, CategoryTheory.FinCategory.asTypeToObjAsType_map, AddSubsemigroup.coe_toSubsemigroup_apply, Monovary.dual_left, Finset.Colex.lt_iff_exists_forall_lt, DegLex.forall_iff, Matrix.updateCol_reindex, DirectSum.decompose_of_mem, Equiv.pprodEquivProd_apply, DomMulAct.map_mk_symm_nhds, equivIsoIso_hom, Equiv.transPartialEquiv_symm_apply, FundamentalGroupoid.equiv_apply, Matrix.comp_single_single, CliffordAlgebra.ι_range_map_lift, DomMulAct.comap_mk_nhds, Equiv.mapMatrix_apply, zmultiples_equiv_zmultiples_apply, AddCircle.equivIco_coe_eq, MulEquiv.prodMultiplicative_symm_apply, CategoryTheory.Iso.homFromEquiv_symm_apply, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply, AlgHom.op_apply_apply, nndist_toMul, CategoryTheory.uliftCoyonedaEquiv_uliftCoyoneda_map, SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply, FreeAddMonoid.vadd_def, BoundedContinuousFunction.isEmbedding_coeFn, Equiv.prodUnique_symm_apply, IsLeast.dual, Equiv.Perm.sameCycle_inv_apply_left, CategoryTheory.TwoSquare.equivNatTrans_apply, EquicontinuousOn.tendsto_uniformOnFun_iff_pi, AlgEquiv.toAlgHom_op, Equiv.instIdempotentOpCoeForallForallArrowCongr, CategoryTheory.coyonedaEquiv_comp, CategoryTheory.uliftYonedaEquiv_symm_apply_app, AddMonoidHom.fiberEquiv_symm_apply, Equiv.ofLeftInverse_symm_apply, Equiv.symm_apply_apply, ContinuousAlternatingMap.piEquiv_apply, SymAlg.unsym_zero, Filter.tendsto_prodAssoc_symm, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_left, monotone_dual_iff, OrderDual.isBounded_preimage_ofDual, Equiv.emptySum_apply_inr, ContinuousMap.piEquiv_symm_apply, Equiv.altCongrHom_apply_coe, CategoryTheory.conjugateEquiv_symm_apply_app, MulAction.toPerm_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality, Monoid.CoprodI.inv_def, Equiv.prodPUnit_apply, ContinuousMap.continuous_iff_continuous_uniformOnFun, SetSemiring.down_one, toDual_zero, coe_equiv_lpPiLp_symm, Matrix.vandermonde_succ, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, NonemptyInterval.dual_top, CategoryTheory.nerve.homEquiv_apply, BoundedLatticeHom.symm_dual_comp, UniformOnFun.isEmbedding_toFun_finite, Rep.homEquiv_apply_hom, Magma.AssocQuotient.lift_comp_of', HahnEmbedding.Partial.truncLT_mem_range_extendFun, MulAutMultiplicative_symm_apply_apply, toDegLex_ofDegLex, finCongr_symm_apply_coe, CategoryTheory.conjugateEquiv_apply_app, TopologicalSpace.Opens.complOrderIso_symm_apply, Equiv.Perm.SameCycle.symm_apply_right, isExtrFilter_dual_iff, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_left, antivaryOn_toDual_left, CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp, MonoidAlgebra.lift_symm_apply, Equiv.equivCongr_refl_left, CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app, Finset.Ioc_ofDual, Polynomial.eval₂_ofFinsupp, Multiset.consEquiv_symm_some, Module.Relations.Solution.directSumEquiv_apply_var, List.getEquivOfForallCountEqOne_apply, DirectSum.decompose_symm_sub, DomAddAct.isOpenEmbedding_mk_symm, Order.pred_ofAdd, AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe, Matrix.submatrix_single_equiv, CochainComplex.fromSingle₀Equiv_apply_coe, sigmaFinsuppAddEquivDFinsupp_symm_apply, MulEquiv.monoidHomCongrLeftEquiv_apply, Finset.Colex.toColex_strictMono, Topology.WithLawson.toLawson_inj, InfTopHom.dual_id, ofDual_hnot, TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace_symm_apply_apply, CategoryTheory.frobeniusMorphism_mate, Equiv.optionSubtype_symm_apply_apply_coe, FirstOrder.Language.Formula.equivSentence_not, Equiv.Perm.perm_inv_on_of_perm_on_finite, Function.update_updateFinset, Metric.Snowflaking.ofSnowflaking_comp_toSnowflaking, CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation, DFinsupp.equivProdDFinsupp_apply, DualNumber.lift_apply_eps, Additive.toMul_le, Equiv.congr_fun, isSquare_ofAdd_iff, SetTheory.PGame.add_moveRight_inr, Module.Relations.Solution.IsPresentation.linearMapEquiv_apply, Equiv.sigmaAssocProd_apply_snd_fst, Quaternion.re_equivProd_symm_apply, Equiv.setSubtypeComm_apply, NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le, SimpleGraph.hasseDualIso_apply, CategoryTheory.Limits.Pi.reindex_hom_π_assoc, Finsupp.sum_equivMapDomain, toDual_sSup, ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquiv_apply, SetSemiring.down_mul, AlgEquiv.prodCongr_apply, CommBialgCat.isoEquivBialgEquiv_apply, WithCStarModule.equiv_symm_neg, QuasilinearOn.dual, LatticeHom.dual_symm_apply_toFun, Equiv.Set.insert_symm_apply_inr, StrictMono.dual_right, Equiv.pnatEquivNat_apply, CategoryTheory.Bicategory.mateEquiv_id_comp_right, CategoryTheory.Localization.SmallShiftedHom.equiv_comp, CategoryTheory.Adjunction.conjugateEquiv_leftAdjointCompIso_inv, PartialEquiv.transEquiv_symm_apply, Metric.Snowflaking.image_toSnowflaking_emetricClosedBall, MulEquiv.op_apply_symm_apply, HahnSeries.SummableFamily.hsum_smul_module, Equiv.Perm.decomposeFin_symm_apply_one, RootPairing.reflectionPerm_self, Submodule.coe_isComplEquivProj_symm_apply, UniformOnFun.toFun_div, CategoryTheory.Limits.Pi.reindex_hom_π, isAddRightRegular_toColex, SetTheory.PGame.mul_moveRight_inl, Equiv.toFun_as_coe, Topology.WithUpper.toUpper_ofUpper, Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde, extDerivWithin_constOfIsEmpty, LieAlgebra.bracket_ofTwoCocycle, SheafOfModules.GeneratingSections.epi, SeparationQuotient.liftNormedAddGroupHomEquiv_apply, Specialization.toEquiv_inj, toLex_vadd', SymAlg.unsym_add, Polynomial.rootsExpandPowEquivRoots_apply, Matrix.vec_of, Equiv.mulLeft₀_symm_apply, Algebra.Norm.Transitivity.comp_det_mul_pow, finSuccEquiv'_eq_some, Homeomorph.piCongrLeft_apply_apply, Finset.Colex.mem_initSeg, MonoidHom.toAdditive_symm_apply_apply, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp_symm_assoc, nndist_toDual, Matrix.updateRow_submatrix_equiv, FreeMonoid.toList_ofList, PartialFun.Iso.mk_inv, CategoryTheory.Sieve.overEquiv_le_overEquiv_iff, AddAction.orbitZMultiplesEquiv_symm_apply', FreeNonUnitalNonAssocAlgebra.lift_unique, Complex.equivRealProd_symm_apply, Equiv.toOrderIsoSet_symm_apply, Sym.coe_equivNatSum_symm_apply, sigmaAntidiagonalEquivProd_symm_apply_snd, tangentBundle_model_space_coe_chartAt, CategoryTheory.Subfunctor.Subpresheaf.ofSection_eq_range', Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom, StandardEtalePair.homEquiv_apply_coe, toDual_eq_zero, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd, RootPairing.flipEquiv_apply, Equiv.sumPiEquivProdPi_symm_apply, MonoidAlgebra.mapDomainAddEquiv_single, Sum.Lex.inl_bot, Equiv.leftInverse_symm, SSet.nonDegenerateEquivOfIso_symm_apply_coe, SymAlg.sym_add, CategoryTheory.Subobject.symm_apply_mem_iff_mem_image, OrderAddMonoidIso.coe_toEquiv_symm, NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, TensorProduct.toMatrix_assoc, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right, CategoryTheory.nerve.edgeMk_id, FirstOrder.Ring.lift_genericPolyMap, CategoryTheory.nerve.right_edge, WithBot.map_ofDual, CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_φ, Sym.cast_rfl, OrthonormalBasis.coe_reindex, Orientation.reindex_neg, Finset.geomSum_le_geomSum_iff_toColex_le_toColex, ofDual_preimage_latticeClosure, SimpleGraph.Iso.map_symm_apply, SkewPolynomial.φ_iterate_apply, AddAction.orbitZMultiplesEquiv_symm_apply, Equiv.equivCongr_apply_apply, SetTheory.PGame.mulOption_neg_neg, norm_toAdd, AlgEquiv.arrowCongr_apply, StrictMonoOn.dual_left, ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply, ofDual_smul, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, AntivaryOn.dual_right, FreeAddGroup.lift_mk, SkewPolynomial.monomial_def, Equiv.sigmaSumDistrib_symm_apply, HahnSeries.SummableFamily.Equiv_toFun, OrderIso.smulRightDual_apply, unitsEquivProdSubtype_apply_coe, CategoryTheory.FunctorToTypes.binaryCoproductEquiv_apply, Fintype.finsetEquivSet_apply, Fin.revOrderIso_apply, CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_symm_apply_self, MeasurableEquiv.coe_toEquiv, ExteriorAlgebra.lift_ι_apply, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst, AffineBasis.coord_reindex, zpowersHom_apply, ContinuousLinearEquiv.unitsEquivAut_apply, MeasurableEquiv.coe_sumPiEquivProdPi, Finset.Colex.erase_lt_erase, Set.coe_biUnionEqSigmaOfDisjoint_symm_apply, powersHom_symm_apply, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_symm_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, isAddLeftRegular_ofDual, Equiv.Set.univ_symm_apply, RingEquiv.asBoolRingAsBoolAlg_symm_apply, Monoid.CoprodI.mrange_eq_iSup, Finset.Colex.erase_le_erase, SetTheory.PGame.mul_moveRight_inr, strictMonoOn_dual_iff, Prod.Lex.prodLexAssoc_symm_apply, MeasureTheory.continuous_diracProbaEquiv, MeasureTheory.LevyProkhorov.toMeasureEquiv_symm_apply_toMeasure, AddEquiv.symmEquiv_symm_apply_symm_apply, AddChar.toMonoidHomEquiv_symm_apply, ZSpan.quotientEquiv_apply_mk, AddSubsemigroup.toSubsemigroup'_closure, Equiv.Set.insert_apply_left, SupHom.symm_dual_comp, WithConv.equiv_apply, isAddLeftRegular_ofColex, WithZero.expOrderIso_symm_apply, CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality', OrderIso.dualDual_apply, Diffeomorph.contMDiff_toFun, Equiv.coe_ofInjective_symm, CategoryTheory.HomOrthogonal.matrixDecomposition_id, CategoryTheory.PreZeroHypercover.interLift_h₀, FirstOrder.Ring.realize_termOfFreeCommRing, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, MulAutMultiplicative_apply_apply, CategoryTheory.uliftCoyonedaEquiv_symm_apply_app, Equiv.toPartialEquiv_symm_apply, isAddRegular_toAdd, ofBoolAlg_bot, FirstOrder.Field.lift_genericMonicPoly, Multiplicative.ofAdd_eq_bot, isLowerSet_preimage_toDual_iff, CategoryTheory.Functor.representableByUliftFunctorEquiv_symm_apply_homEquiv, InverseSystem.globalEquiv_compatibility, Equiv.asEmbedding_apply, equivTangentBundleProd_apply, Finset.piCongrLeft_comp_restrict, Function.piCongrLeft'_symm_update, AddMagma.FreeAddSemigroup.lift_comp_of, PreQuasiregular.equiv_apply_val, Matrix.hadamard_of_one, Equiv.symm_symm_apply, FreeAbelianGroup.liftMonoid_coe_addMonoidHom, Equiv.boolArrowEquivProd_apply, CliffordAlgebra.ι_comp_lift, CategoryTheory.Discrete.equivalence_unitIso, Fin.castLEquiv_symm_apply, Matrix.coe_ofAddEquiv_symm, CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm, EquicontinuousOn.inducing_uniformOnFun_iff_pi', Finset.Colex.toColex_le_toColex_iff_max'_mem, Equiv.add_def, DividedPowers.equiv_apply, Equiv.piCongrLeft_preimage_pi, PiTensorProduct.reindex_comp_tprod, Hamming.nndist_eq_hammingDist, equivShrink_symm_bot, Function.OfArity.curryEquiv_symm_apply, MeasureTheory.Measure.infinitePi_map_piCongrLeft, Algebra.traceMatrix_reindex, Equiv.sum_comp, SSet.opFunctor_map, pow_finEquivZPowers_symm_apply, Equiv.Perm.perm_inv_mapsTo_of_mapsTo, supPrime_toDual, dist_ofDual, Matrix.diagonal_vec2, MvPowerSeries.lexOrder_def_of_ne_zero, Finset.toDual_min', toAdd_multiset_sum, toDual_compares_toDual, Normal.algHomEquivAut_symm_apply, ArchimedeanClass.FiniteElement.val_add, Finset.Ioo_orderDual_def, Pi.toLex_update_le_self_iff, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, uniformContinuous_toMul, CliffordAlgebra.lift_unique, SetTheory.PGame.mul_moveLeft_inl, ofColex_vadd', Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe, UniformOnFun.ofFun_div, CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural, DomMulAct.map_mk_nhds, edist_ofDual, ContinuousAlternatingMap.ofSubsingleton_apply_toContinuousMultilinearMap, OrderIso.dual_apply, Homeomorph.continuousMapCongr_symm_apply, CategoryTheory.FunctorToTypes.binaryCoproductEquiv_symm_apply, gc_upperPolar_lowerPolar, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, Unitization.lift_symm_apply_apply, AddEquiv.toMultiplicativeLeft_apply_symm_apply, Sum.Lex.toLex_lt_toLex, CategoryTheory.Coyoneda.objOpOp_hom_app, CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_symm_τr, Invertible.mulRight_apply, PerfectRing.liftEquiv_comp_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map, disjoint_toDual_iff, powCoprime_symm_apply, SSet.Subcomplex.ofSimplexProd_eq_range, CategoryTheory.nerve.homEquiv_edgeMk, FreeMonoid.lift_of_comp_eq_map, Matrix.GeneralLinearGroup.upperRightHom_apply, Equiv.uniqueSigma_apply, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, Finsupp.mapRange.equiv_refl, CategoryTheory.Over.postAdjunctionLeft_unit_app_left, Pi.toLex_update_lt_self_iff, OrderIso.sumLexIicIoi_symm_apply_of_le, BoundedOrderHom.dual_apply_toOrderHom, Field.Emb.Cardinal.succEquiv_coherence, Equiv.bijective_comp, Topology.WithUpper.ofUpper_lt_ofUpper, Hamming.ofHamming_smul, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, FreeMonoid.lift_ofList, AddMonCat.equivalence_inverse_map, Equiv.prodAssoc_apply, Metric.Snowflaking.mk_eq_toSnowflaking, FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_fst, WithZero.lt_ofAdd_iff, CategoryTheory.Functor.homObjEquiv_symm_apply_app, Metric.Snowflaking.val_eq_ofSnowflaking, finSigmaFinEquiv_apply, NumberField.InfinitePlace.mkReal_coe, HahnSeries.SummableFamily.smul_apply, CategoryTheory.Adjunction.mkOfHomEquiv_counit_app, MultilinearMap.curryFinFinset_apply, gc_upperBounds_lowerBounds, ContinuousLinearEquiv.compContinuousAlternatingMap_coe, FirstOrder.Language.LEquiv.onFormula_apply, SSet.stdSimplex.obj₀Equiv_apply, Subgroup.IsComplement.equiv_mul_left_of_mem, Orientation.map_eq_iff_det_pos, Subgroup.smul_leftQuotientEquiv, groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂, Quiver.SingleObj.toPrefunctor_apply_map, continuous_toAdd, Equiv.Set.congr_symm_apply, Equiv.optionCongr_one, Equiv.permCongrHom_coe, CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm, CategoryTheory.Functor.equivCatHom_apply, ofBoolRing_add, infClosed_preimage_toDual, Matrix.uniqueEquiv_symm_apply, HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_symm_mk, SSet.prodStdSimplex.objEquiv_δ_apply, SetTheory.PGame.toRightMovesNim_one_symm, Equicontinuous.tendsto_uniformFun_iff_pi, AddMonCat.equivalence_counitIso, toDual_sdiff, Matrix.uniqueAddEquiv_symm_apply, Equiv.divRight₀_symm_apply, Submonoid.toAddSubmonoid_closure, Topology.WithUpper.ofUpper_le_ofUpper, ofLex_vadd, Equiv.Perm.decomposeFin.symm_sign, MonovaryOn.dual_left, CategoryTheory.Iso.eHomCongr_comp_assoc, MvPolynomial.rename_psum, RootPairing.Hom.comp_indexEquiv_apply, CategoryTheory.Adjunction.homEquiv_unit, Sym.coe_equivNatSumOfFintype_symm_apply, CategoryTheory.Under.postAdjunctionRight_unit_app_right, CategoryTheory.Limits.WidePullbackCone.reindex_base, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, pow_ofColex, CategoryTheory.conjugateEquiv_leftUnitor_hom, Homeomorph.continuousMapCongr_apply, SetSemiring.zero_def, SkewMonoidAlgebra.lift_of, Complex.lift_apply, Subgroup.range_zpowersHom, PartOrd.dual_map, SkewMonoidAlgebra.lift_single, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm, SSet.op_σ, Module.Relations.Solution.IsPresentation.linearMapEquiv_symm_apply, DFinsupp.lex_lt_iff, CategoryTheory.uliftYonedaEquiv_apply, HahnEmbedding.Partial.orderTop_eq_iff, multiplesEquivMultiples_apply, ofDual_himp, norm_ofDual, CategoryTheory.Iso.homCongr_comp, CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_apply, uniformContinuous_ofMul, uliftPowersHom_symm_apply, UniformOnFun.postcomp_uniformContinuous, CategoryTheory.Arrow.equivSigma_apply_snd_snd, CategoryTheory.bijection_natural, CategoryTheory.Functor.Initial.limitConeComp_isLimit, FreeCommRing.lift_of, RingHom.eq_liftOfSurjective, ChainComplex.toSingle₀Equiv_apply_coe, ofLex_pow, CategoryTheory.Limits.Pi.reindex_inv_π_assoc, SetTheory.PGame.Domineering.shiftRight_apply, OrderDual.toDual_inj, SkewMonoidAlgebra.lift_apply, Equiv.algEquiv_apply, ofMul_multiset_prod, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.Functor.FullyFaithful.homEquiv_symm_apply, Equiv.equivPUnit_symm_apply, Monoid.Coprod.con_inv_mul_cancel, Equiv.equivCongr_refl_right, AddChar.coe_toMonoidHomEquiv, Equiv.subtypeSubtypeEquivSubtype_apply_coe, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, CategoryTheory.CartesianClosed.homEquiv_apply_eq, CategoryTheory.Classifier.SubobjectRepresentableBy.homEquiv_eq, RootPairing.pairing_reflectionPerm_self_left, MvPolynomial.coe_mapEquivMonic_comp', ofColex_smul', MulEquiv.prodMultiplicative_apply, pow_toDual, RootPairing.weylGroup_apply_root, Rack.envelAction_prop, monovary_toDual_right, CategoryTheory.Bicategory.mateEquiv_symm_apply', CircleDeg1Lift.translate_iterate, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, Equiv.sumAssoc_apply_inl_inl, Rack.ad_conj, ExteriorAlgebra.lift_comp_ι, Order.pred_toMul, WithBot.ofDual_apply_coe, AddAut.conj_symm_apply, Matrix.adjugate_fin_three, Matrix.natCast_fin_three, Finsupp.DegLex.single_lt_iff, CategoryTheory.Localization.homEquiv_eq, DFinsupp.sigmaCurryLEquiv_apply, CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_apply, Equiv.hasSum_iff, Equiv.punitProd_symm_apply, AddEquiv.toMultiplicativeRight_apply_symm_apply, CategoryTheory.Bicategory.conjugateEquiv_id_comp_right_apply, EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq, IsSublattice.of_dual, Finset.Colex.singleton_le_toColex, AddHom.op_apply_apply, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality', RelIso.emptySumLex_apply, UniformOnFun.ofFun_inv, Tropical.tropEquiv_coe_fn, AddMonoidAlgebra.of_apply, CartanMatrix.D_three, CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply, Equiv.Perm.extendDomain_apply_subtype, AlgEquiv.equivCongr_apply, Equiv.sigmaSigmaSubtype_symm_apply, Finsupp.mapDomain.coe_linearEquiv, ZFSet.coeEquiv_apply_coe, UniversalEnvelopingAlgebra.ι_comp_lift, AlgHom.opComm_symm_apply_apply, Homeomorph.sumProdDistrib_symm_apply, Topology.IsQuotientMap.liftEquiv_symm_apply_coe, Diffeomorph.sumAssoc_coe, AddValuation.toValuation_ofValuation, DomMulAct.isInducing_mk_symm, QuaternionAlgebra.equivTuple_symm_apply, NumberField.Units.logEmbeddingQuot_apply, Small.equiv_small, zpowersMulHom_apply, equicontinuousWithinAt_iff_continuousWithinAt, HahnEmbedding.Partial.coeff_eq_of_mem, Delone.DeloneSet.mapIsometry_symm_apply_carrier, AddCommMonCat.equivalence_functor_map, CategoryTheory.Functor.map_isoCongr, sigmaFinsuppEquivDFinsupp_add, Matrix.neg_of, Finset.Colex.toColex_image_lt_toColex_image, InfHom.dual_apply_toFun, CategoryTheory.Functor.coconeTypesEquiv_apply_pt, AffineBasis.coe_reindex, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, Topology.WithScott.toScott_ofScott, IsGalois.intermediateFieldEquivSubgroup_apply, SymAlg.unsym_inv, FreeLieAlgebra.lift_comp_of, Equiv.sub_def, isQuasiregular_iff', Equiv.forall_congr_left, Equiv.funSplitAt_symm_apply, SSet.prodStdSimplex.objEquiv_naturality, RootPairing.pairing_reflectionPerm_self_right, Equiv.prodSumDistrib_apply_right, NumberField.Units.basisOfIsMaxRank_apply, AddMonoidHom.toMultiplicativeRight_symm_apply_apply, DirectSum.coe_decompose_mul_add_of_left_mem, CategoryTheory.Limits.Concrete.prodEquiv_apply_fst, CategoryTheory.nerve.nonempty_compStruct_iff, SubAddAction.ofFixingAddSubgroup.append_left, Equiv.Finset.union_inl, FreeMonoid.lift_comp_of, RootPairing.Equiv.root_indexEquiv_eq_smul, FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_snd_coe, Matrix.eta_fin_three, lipschitzOnWith_cfc_fun_of_subset, Polynomial.rootsExpandEquivRoots_apply, Metric.Snowflaking.image_ofSnowflaking_eball, Matrix.eRank_reindex, CategoryTheory.Limits.Types.Small.productIso_inv_comp_π, CategoryTheory.Limits.FintypeCat.productEquiv_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left, CategoryTheory.uliftYonedaEquiv_symm_map, UniformFun.postcomp_isUniformInducing, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, DomAddAct.isInducing_mk, LinearIsometryEquiv.piLpCongrLeft_apply, PowerBasis.leftMulMatrix, CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π, TopHom.dual_symm_apply_apply, FreeAbelianGroup.liftAddEquiv_symm_apply, toBoolAlg_zero, NumberField.Units.regulator_eq_det, finPiFinEquiv_apply, NonemptyInterval.dual_pure, OrthogonalIdempotents.equiv, MulEquiv.withZero_apply_symm_apply, Matrix.replicateRow_empty, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, Metric.Snowflaking.preimage_toSnowflaking_emetricClosedBall, continuousOn_cfc_setProd, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, Subgroup.IsComplement.equiv_snd_eq_iff_rightCosetEquivalence, Matrix.of_add_of, OrderIso.coe_symm_toEquiv, Hamming.nnnorm_eq_hammingNorm, ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_apply_toFun, Finset.Ioo_ofDual, Cardinal.mk_subtype_of_equiv, OrderIso.coe_dualDual, toDual_wcovBy_toDual_iff, AddMonoidHom.mulOp_apply_apply, Module.Ray.linearEquiv_smul_eq_map, DFinsupp.sum_eq_sum_fintype, FintypeCat.uSwitchEquiv_naturality, finRotate_succ_eq_decomposeFin, Equiv.iSup_comp, UniformOnFun.tendsto_iff_tendstoUniformlyOn, CategoryTheory.Limits.Sigma.whiskerEquiv_hom, subtypeOrEquiv_symm_inl, Equiv.withBotSubtypeNe_symm_apply_coe, infPrime_ofDual, isAddRegular_ofColex, Metric.Snowflaking.isBounded_preimage_ofSnowflaking_iff, CompHausLike.isoEquivHomeo_symm_apply, GaloisConnection.dual, TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf, AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr, Equiv.toEmbedding_injective, fixingAddSubmonoid_fixedPoints_gc, Matrix.comp_transpose, Equiv.optionSubtypeNe_symm_of_ne, MeasureTheory.Measure.sum_comp_equiv, Bundle.TotalSpace.toProd_symm_apply_proj, Equiv.pprodProd_apply, LatticeHom.dual_apply_toFun, Order.isPredPrelimit_toDual_iff, gelfandStarTransform_symm_apply, Matrix.reindex_mem_rowStochastic_iff, Matrix.piRingEquiv_symm_apply, toDual_vadd, FintypeCat.equivEquivIso_symm_apply_symm_apply, isLeftRegular_toMul, CategoryTheory.FinCategory.categoryAsType_id, Metric.Snowflaking.image_toSnowflaking_eball, CategoryTheory.Limits.IsColimit.homEquiv_apply, FreeAddGroup.lift_apply_of, groupCohomology.isMulCocycle₁_of_mem_cocycles₁, Submonoid.closure_singleton_eq, ofDual_pow, MonoidHom.apply_mnat, finSumNatEquiv_symm_apply_fin, ofMul_vadd, FreeGroupBasis.lift_apply_apply, InverseSystem.PEquivOn.compat, Pi.le_toLex_update_self_iff, InfHom.dual_id, WithTop.ofDual_apply_top, CategoryTheory.Functor.Final.colimitCoconeComp_isColimit, Equiv.coe_subtypeEquivCodomain_symm, Equiv.Perm.sameCycle_symm_apply_right, dist_ofAdd, Bundle.Trivial.isInducing_toProd, DomAddAct.continuous_mk_symm, ContinuousAlternatingMap.alternatizeUncurryFin_constOfIsEmptyLIE_comp, Equiv.optionCongr_injective, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc, FreeAlgebra.liftAux_eq, CategoryTheory.opEquiv_apply, AlgebraicGeometry.coe_opensRestrict_symm_apply, finCongr_apply_mk, Sym2.lift₂_mk, Function.IsFixedPt.equiv_symm, Matrix.smul_of, FreeAddMonoid.ofList_append, Matrix.replicateRow_cons, Interval.coe_dual, AddEquiv.toAdditive_toMultiplicative_symm_apply, NonemptyInterval.fst_dual, TensorAlgebra.lift_symm_apply, CategoryTheory.Quiv.homEquivOfIso_apply, UniformFun.toFun_zero, Primrec.of_equiv_symm_iff, AlgEquiv.op_apply_symm_apply, LatticeHom.symm_dual_id, Orientation.rotation_map, AddMonoidHom.fiberEquivKer_apply, FreeAddGroup.lift_unique, SymAlg.sym_sub, CategoryTheory.Equivalence.inverseFunctor_map, Setoid.quotientKerEquivOfRightInverse_apply, DirectSum.decompose_symm_neg, LinearMap.polyCharpolyAux_map_eval, Topology.WithUpperSet.toUpperSet_specializes_toUpperSet, FreeAbelianGroup.liftAddGroupHom_apply, powCoprime_inv, CommRing.Pic.inv_eq_dual, RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply, finSumNatEquiv_apply_left, toColex_eq_zero, FinEnum.equiv_up, BddOrd.dual_map, WithTop.orderIsoSumLexPUnit_toLex, Affine.Simplex.excenterWeights_reindex, CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply, Equiv.Perm.subtypeEquivSubtypePerm_apply_coe, finSumNatEquiv_symm_apply_add_left, CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism, Set.Iio_toDual, ofAdd_bot, Metric.Snowflaking.ediam_image_ofSnowflaking, Set.PartiallyWellOrderedOn.imageProdLex, Equiv.piCongrLeft_symm_preimage_univ_pi, SSet.Subcomplex.PairingCore.pairing_p_equivII, UniformFun.isometry_ofFun_continuousMap, AddSubmonoid.equivOp_apply_coe, OrderIso.divLeft_apply, AlgHom.prodEquiv_symm_apply, NumberField.Units.finrank_mul_regOfFamily_eq_det, CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight, QuadraticAlgebra.equivProd_symm_apply, CategoryTheory.Sheaf.ΓHomEquiv_naturality_left, Equiv.toHomeomorph_refl, CategoryTheory.Limits.biproduct.matrixEquiv_apply, Function.update_comp_equiv, ofMul_zpow, ContinuousAffineEquiv.coe_toEquiv, Algebra.GrothendieckGroup.lift_symm_apply, FirstOrder.Language.LEquiv.onSentence_apply, MeasureTheory.distribHaarChar_apply, AddSubgroup.IsComplement.mk''_rightQuotientEquiv, Topology.isGeneratedBy_iff, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f, ArchimedeanOrder.val_of, ContinuousMultilinearMap.range_toUniformOnFun, CategoryTheory.Oplax.StrongTrans.Modification.equivOplax_symm_apply, antitone_toDual_comp_iff, DualNumber.lift_inlAlgHom_eps, ContinuousAlternatingMap.piEquiv_symm_apply, GrpCat.toAddGrp_map, FreeAddMonoid.ofList_vadd, Finset.Colex.toColex_sdiff_lt_toColex_sdiff, DFinsupp.prod_eq_prod_fintype, ZSpan.volume_fundamentalDomain, Affine.Simplex.median_reindex, Sum.Lex.inl_mono, DyckWord.equivTreesOfNumNodesEq_symm_apply_coe, PartialEquiv.transEquiv_target, basis_toMatrix_basisFun_mul, Fin.coe_of_injective_castSucc_symm, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, InfPrime.dual, Pi.ofColex_apply, Matrix.submatrix_id_mul_right, Prod.Lex.sumLexProdLexDistrib_symm_apply, MulChar.equivToUnitHom_symm_coe, exteriorPower.presentation.relationsSolutionEquiv_symm_apply_var, WithZero.lift'_coe, Function.Embedding.optionEmbeddingEquiv_apply_snd_coe, Function.fromTypes_nil_equiv_apply, Sum.Lex.toLexRelIsoLE_coe, WithBot.toDual_map, QuadraticAlgebra.lift_apply_apply, Hamming.ofHamming_sub, Equiv.image_eq_iff_eq, Matrix.reindex_apply, FreeAddMonoid.ofList_map, CategoryTheory.uliftYonedaEquiv_naturality, Equiv.symmEquiv_apply_apply, Function.fromTypes_zero_equiv_symm_apply, ofLex_eq_one, dotProduct_comp_equiv_symm, CategoryTheory.Sieve.overEquiv_symm_iff, toDual_max, Height.mulHeight_comp_equiv, ofMul_pow, NumberField.InfinitePlace.orbitRelEquiv_apply_mk'', DirectSum.coe_decompose_mul_of_left_mem_of_le, DihedralGroup.oddCommuteEquiv_symm_apply, CategoryTheory.Subfunctor.Subpresheaf.IsGeneratedBy.of_equiv, MonoidHom.fiberEquiv_symm_apply, equivShrink_symm_zero, CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over, CategoryTheory.conjugateEquiv_counit_symm, IsBot.ofDual, CategoryTheory.Sieve.functorPushforward_over_map, DirectSum.decompose_symm_one, isMax_ofDual_iff, ExteriorAlgebra.ι_comp_lift, CommRing.Pic.mk_eq_iff, TopCat.Sheaf.extend_hom_app, CategoryTheory.Functor.mapBicone_whisker, Finset.Colex.toColex_sdiff_le_toColex_sdiff, toDual_inv, ofMul_inv, CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq, Equiv.sumIsLeft_symm_apply_coe, Pi.mulSingle_comp_equiv, Equiv.sumProdDistrib_symm_apply_right, Equiv.sumArrowEquivProdArrow_symm_apply_inr, DFinsupp.colex_lt_iff_of_unique, Matrix.natCast_fin_two, MulAutMultiplicative_symm_apply_symm_apply, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, bddBelow_preimage_toDual, UniformFun.tendsto_iff_tendstoUniformly, DirectSum.coe_decompose_mul_of_left_mem, Set.Ici_ofDual, UniformOnFun.one_apply, MonomialOrder.degLex_le_iff, powCoprime_one, Equiv.mulEquiv_apply, CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply, continuous_ofDual, ofAdd_list_prod, CategoryTheory.Functor.natTransEquiv_symm_apply_app, Matrix.inv_reindex, AddEquiv.coe_prodAssoc, CategoryTheory.Functor.homEquivOfIsLeftKanExtension_symm_apply, Tuple.graphEquiv₂_apply, Equiv.eq_preimage_iff_image_eq, Equiv.subtypeEquivRight_apply, WithTop.orderIsoSumLexPUnit_symm_inl, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, CategoryTheory.PreZeroHypercover.reindex_f, RootPairing.chainBotCoeff_reflectionPerm_right, UniformOnFun.edist_eval_le, optionProdEquiv_mk_some, DilationEquiv.coe_toEquiv, CategoryTheory.PreZeroHypercover.isoMk_hom_s₀, CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit, CategoryTheory.Bicategory.conjugateEquiv_comp_id_right_apply, MvPolynomial.rename_esymm, SymAlg.sym_injective, Equiv.tsum_eq, UniformOnFun.postcomp_isUniformInducing, ofBoolRing_toBoolRing, Topology.WithLowerSet.isLowerSet_toLowerSet_preimage, Iio_orderDual_def, toAdd_zpow, TensorAlgebra.lift_ι_apply, FreeAddMagma.lift_comp_of, SSet.prodStdSimplex.objEquiv_apply_snd, Invertible.mulLeft_apply, PiTensorProduct.reindex_trans, WithCStarModule.equiv_neg, AddMonoidAlgebra.lift_apply, Matrix.eta_fin_two, addMonoidAlgebraEquivDirectSum_symm_apply, ContinuousMap.equivFnOfDiscrete_apply, Equiv.biSup_comp, SSet.hoFunctor.unitHomEquiv_eq, Equiv.toEmbedding_apply, Finsupp.sigmaFinsuppEquivPiFinsupp_apply, TopologicalSpace.Closeds.complOrderIso_apply, LinearEquiv.sumPiEquivProdPi_apply, RootPairing.reflectionPerm_coroot, ContinuousMultilinearMap.ofSubsingleton_symm_apply_apply, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, SetTheory.PGame.mul_moveLeft_inr, Order.succ_ofMul, CommRing.Pic.mk_eq_self, Equiv.transPartialEquiv_source, FreeAddSemigroup.lift_of, HahnSeries.SummableFamily.smul_hsum, Antivary.dual_left, SkewPolynomial.φ_def, Finset.geomSum_ofColex_strictMono, Matrix.updateRow_reindex, strictMono_comp_ofDual_iff, Topology.IsGeneratedBy.continuous_equiv_symm, Equiv.right_inv', Metric.Snowflaking.image_ofSnowflaking_ball, IsMax.toDual, CategoryTheory.nerve.homEquiv_comp, CategoryTheory.nerve.left_edge, MeasureTheory.ComplexMeasure.equivSignedMeasure_apply, CategoryTheory.nerve.mk₁_homEquiv_apply, Equiv.swap_comp_apply, monoidEndToAdditive_apply_apply, Pi.mulSingle_multiplicativeOfAdd_eq, Finset.map_toDual_max, finSuccEquiv'_symm_coe_above, Metric.Snowflaking.isBounded_image_ofSnowflaking_iff, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left, LinearEquiv.funCongrLeft_apply, CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply, FreeAddMonoid.toList_of, Equiv.optionSubtype_apply_symm_apply, Equiv.Set.union_apply_left, isRegular_ofAdd, addOrderOf_ofMul_eq_orderOf, ArchimedeanClass.FiniteElement.val_mul, RootPairing.corootSpanMem_reflectionPerm_self, RelIso.relHomCongr_apply, Topology.WithLowerSet.toLowerSet_ofLowerSet, Finset.equivBitIndices_apply, WithBot.le_toDual_iff, Complex.equivRealProd_apply_le', Int.toAdd_pow, Equiv.cast_eq_iff_heq, AddSubmonoid.closure_singleton_eq, finsuppEquivDFinsupp_apply, IncidenceAlgebra.mu_ofDual, MulAction.toPerm_symm_apply, DFinsupp.Lex.le_iff_of_unique, FreeAlgebra.lift_ι_apply, IsFreeGroup.lift_of, Interval.dual_top, DomMulAct.mk_smul_toLp, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, AddConstEquiv.toEquiv_injective, InfHom.dual_symm_apply_toFun, HahnSeries.embDomainOrderEmbedding_apply, CategoryTheory.Localization.Preadditive.homEquiv_apply, CoalgEquiv.toEquiv_injective, cmp_toDual, List.getEquivOfForallCountEqOne_symm_apply_val, WithTop.ofDual_lt_ofDual_iff, FreeAddMonoid.toList_zero, CategoryTheory.Arrow.equivSigma_apply_fst, dist_toAdd, IsGreatest.dual, MulEquiv.withZero_apply_apply, CategoryTheory.InducedCategory.homEquiv_symm_apply_hom, Matrix.charpoly.univ_coeff_eval₂Hom, Equiv.image_subset, AddMonoidHom.toMultiplicative_symm_apply_apply, DyckWord.equivTreesOfNumNodesEq_apply_coe, FreeAddMonoid.ofList_cons, Equiv.mulRight₀_apply, CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_f, PerfectRing.liftEquiv_id_apply, isClosedMap_ofAdd, CategoryTheory.Limits.Types.isLimitEquivSections_apply, CategoryTheory.GrothendieckTopology.mem_over_iff, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_pt, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one_assoc, CategoryTheory.Limits.WalkingPair.swap_apply_right, ContinuousMultilinearMap.prodEquiv_symm_apply_fst, antitoneOn_toDual_comp_iff, Complex.antilipschitz_equivRealProd, PartENat.withTopEquiv_ofNat, AddMonoidHom.coe_toMultiplicativeLeft, WithBot.toDual_bot, MeasureTheory.measurePreserving_piCongrLeft, GradedAlgebra.proj_recompose, Monoid.CoprodI.lift_mrange_le, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, OrderIso.sumLexIioIci_symm_apply_Iio, DualNumber.lift_smul, DihedralGroup.oddCommuteEquiv_apply, LieAlgebra.lieCharacterEquivLinearDual_symm_apply, exteriorPower.presentation.relationsSolutionEquiv_apply_apply, SkewMonoidAlgebra.coeff_equivMapDomain, Equiv.symm_comp_eq, Equiv.sigmaEquivProd_symm_apply, Equiv.arrowProdEquivProdArrow_apply, Prod.Lex.le_iff, Equiv.embeddingFinSucc_snd, PiTensorProduct.reindex_tprod, MulEquiv.coe_prodAssoc, DomAddAct.symm_mk_neg, CategoryTheory.conjugateEquiv_symm_iso, AddSubgroup.toSubgroup_closure, Equiv.Perm.extendDomain_apply_image, BoundedOrderHom.dual_id, DomMulAct.continuous_mk_symm, HahnSeries.of_symm_smul_of_eq_mul, List.sortedGE_map_ofDual, UniformEquiv.piCongrLeft_symm_apply, CategoryTheory.Equivalence.symmEquivFunctor_map, CategoryTheory.Limits.Cofork.IsColimit.homIso_apply_coe, LinearEquiv.isAdjointPair_symm_iff, Topology.WithScott.ofScott_inj, AddHom.mulOp_apply_apply, MonoidHom.toAdditiveLeft_apply_apply, toBoolAlg_add, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, CategoryTheory.Functor.partialRightAdjointHomEquiv_comp, HahnSeries.SummableFamily.smul_toFun, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, PowerBasis.liftEquiv_symm_apply, Matrix.transpose_empty_cols, CartanMatrix.D_three', isTranscendenceBasis_equiv, Set.uIoo_toDual, AddEquiv.op_symm_apply_symm_apply, IsCyclic.val_inv_mulAutMulEquiv_apply, ofColex_mul, Equiv.sigmaFiberEquiv_apply, LinearIsometryEquiv.coe_prodAssoc_symm, finSumFinEquiv_apply_right, AlgHom.opComm_apply_apply, CategoryTheory.Adjunction.conjugateEquiv_leftAdjointIdIso_hom, DomMulAct.isClosedEmbedding_mk, CategoryTheory.Subfunctor.ofSection_eq_range', AddChar.coe_toAddMonoidHom, Homeomorph.toEquiv_injective, NumberField.Units.fundSystem_mk, Equiv.bijOn_symm_image, HahnEmbedding.IsPartial.truncLT_mem_range, PrimitiveSpectrum.gc_closureOperator, CategoryTheory.Limits.Pi.whiskerEquiv_inv, Abelianization.coe_lift_symm, finSuccEquivLast_castSucc, CategoryTheory.Functor.partialRightAdjointHomEquiv_map, DomMulAct.smul_mulActionHom_apply, MulEquiv.arrowCongr_apply, FreeGroup.lift_unique, Subgroup.IsComplement.leftCosetEquivalence_equiv_fst, Equiv.Perm.sameCycle_inv_apply_right, NonUnitalAlgHom.prodEquiv_apply, CategoryTheory.Limits.biproduct.reindex_inv, Matrix.of_one_hadamard, InverseSystem.invLimEquiv_apply_coe, OrderHom.symm_dual_id, SupClosed.dual, toLex_ofLex, CategoryTheory.Functor.CorepresentableBy.homEquiv_eq, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, Cardinal.extend_function_of_lt, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply, MeasurableEquiv.toEquiv_injective, isOfFinOrder_ofAdd_iff, Equiv.pprodEquivProdPLift_apply, Monoid.CoprodI.range_eq_iSup, Metric.Snowflaking.image_ofSnowflaking_eq_preimage, SupHom.dual_comp, Equiv.sumCompl_apply_inl, supIrred_toDual, Monoid.PushoutI.NormalWord.cons_head, ContinuousAlternatingMap.ofSubsingletonLIE_apply, Set.up_mul, OrthonormalBasis.equiv_apply, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_fst, MeasurableEquiv.measurable_toFun, Equiv.symm_apply_eq, AddMagma.FreeAddSemigroup.lift_comp_of', CategoryTheory.Limits.IsLimit.homEquiv_symm_π_app, even_toAdd_iff, Abelianization.lift_apply_of, CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv, toMul_zero, Matrix.isUnit_submatrix_equiv, CategoryTheory.Localization.SmallHom.equiv_mkInv, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, Equiv.subtypePreimage_apply, Matrix.submatrix_updateCol_equiv, OrderIso.sumDualDistrib_symm_inl, CStarMatrix.of_sub_of, finSuccAboveEquiv_symm_apply_ne_last, CommAlgCat.isoEquivAlgEquiv_apply, Normal.algHomEquivAut_apply, CommRing.Pic.mapAlgebra_apply, Quiver.SingleObj.toPrefunctor_comp, NonUnitalAlgHom.prodEquiv_symm_apply, CategoryTheory.PreZeroHypercover.reindex_X, Pi.single_additiveOfMul_eq, CategoryTheory.Adjunction.homAddEquiv_sub, FreeGroup.injective_lift_of_ping_pong, CategoryTheory.tensorLeftHomEquiv_tensor, OrderMonoidIso.withZero_apply_symm_apply, Equiv.finsuppUnique_apply, SSet.Subcomplex.yonedaEquiv_coe, finAddFlip_apply_mk_right, Equiv.pnatEquivNat_symm_apply, CommRing.Pic.ext_iff, FreeAddMonoid.toList_add, Equiv.zero_def, ofDual_compares_ofDual, isAddRightRegular_ofDual, Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem, WithTop.toDual_lt_iff, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, ModularGroup.coe_T_inv, Unitization.starLift_range, ofBoolAlg_sup, OrderDual.ext_iff, IsPrimitiveRoot.primitiveRootsPowEquiv_symm_apply_coe, Rep.ofMulDistribMulAction_ρ_apply_apply, SSet.OneTruncation₂.ofNerve₂.natIso_hom_app_obj, WithZeroMulInt.toNNReal_neg_apply, Set.Finite.equiv_image_eq_iff_subset, Fintype.card_eq, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_assoc, DomAddAct.symm_mk_add, toMul_add, CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp, CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_fst, isClosedMap_toDual, CategoryTheory.FinCategory.asTypeToObjAsType_obj, sigmaFinsuppEquivDFinsupp_symm_apply, toMul_sum, CategoryTheory.Sieve.overEquiv_top, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map, CategoryTheory.Limits.CofanTypes.equivOfIsColimit_symm_apply, ContinuousMap.addUnitsLift_apply_neg_apply, IsAzumaya.mulLeftRight_comp_congr, NumberField.IsCMField.equivInfinitePlace_apply, HahnSeries.order_abs, FreeMonoid.ofList_toList, optionProdEquiv_symm_inl, Set.opEquiv_self_symm_apply_coe, Subgroup.mem_toAddSubgroup', AddCircle.equivIccQuot_comp_mk_eq_toIocMod, isClosedMap_ofMul, Delone.DeloneSet.mapIsometry_symm_apply_coveringRadius, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_three, ofColex_eq_zero, SheafOfModules.freeHomEquiv_symm_comp, CategoryTheory.CosimplicialObject.cechConerveEquiv_symm_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality', SetTheory.PGame.relabel_moveLeft, Equiv.symm_trans_apply, CategoryTheory.Iso.homCongr_refl, OrderIso.equivClosureOperator_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, minimal_toDual, TensorAlgebra.lift_comp_ι, Matrix.submatrix_mulVec_equiv, disjoint_ofDual_iff, ContinuousMap.val_unitsLift_symm_apply_apply, CategoryTheory.Functor.RepresentableBy.equivOfIsoObj_symm_apply, coe_toLexLinearEquiv, Nat.ofAdd_mul, Nat.Primes.prodNatEquiv_apply, ofAdd_image_zmultiples_eq_zpowers_ofAdd, Representation.norm_ofMulDistribMulAction_eq, toLex_add, CategoryTheory.HomOrthogonal.equiv_of_iso, Subgroup.smul_apply_eq_smul_apply_inv_smul, AddSubmonoid.toSubmonoid_closure, CategoryTheory.FunctorToTypes.binaryProductEquiv_symm_apply, Equiv.psigmaCongrRight_apply, ContinuousAlternatingMap.norm_ofSubsingleton, toDual_intCast, RootPairing.Equiv.comp_indexEquiv_apply, CategoryTheory.GradedObject.comapEquiv_unitIso, PerfectRing.liftEquiv_apply, CommRing.Pic.instFreeAsModuleOfNat, isRightRegular_toColex, PadicInt.continuousAddCharEquiv_of_norm_mul_apply, Valuation.ofAddValuation_apply, Complex.preimage_equivRealProd_prod, SimpleGraph.Walk.IsHamiltonian.getVertEquiv_symm_apply, Module.Relations.Solution.directSumEquiv_symm_apply_var, FreeGroup.lift_symm_apply, AddSubgroup.range_zmultiplesHom, Equiv.permCongr_trans, autEquivZmod_symm_apply_intCast, AddConstEquiv.coe_symm_toEquiv, BoundedOrderHom.symm_dual_comp, Equiv.piCongrLeft_symm_preimage_pi, toMul_sub, FreeAddGroup.closure_eq_range, Set.graphOn_prod_graphOn, Set.dual_ordConnected, Matrix.of_zero, QuaternionAlgebra.coe_addEquivProd, toDual_mul, zmultiplesHom_ker_eq, AddAction.stabilizerEquivStabilizer_symm_apply, Real.sinhEquiv_symm_apply, SetTheory.PGame.moveRight_nim, Rack.act'_apply, Finsupp.prod_equivMapDomain, CartanMatrix.B_two, Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem, FreeMonoid.toList_of, Module.Basis.det_reindex_symm, sSupHom.dual_symm_apply_toFun, isAddLeftRegular_toLex, AddCircle.continuous_equivIoc_symm, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, Finsupp.equivFunOnFinite_symm_apply_support, CategoryTheory.uliftYonedaEquiv_comp, cmpLE_ofDual, Quiver.SingleObj.pathEquivList_symm_cons, Fin.cycleIcc_to_cycleRange, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply, AlternatingMap.ofSubsingleton_apply_apply, SSet.stdSimplex.face_obj, DomAddAct.mk_zsmul, Subsemigroup.toAddSubsemigroup_closure, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply, Equiv.Set.univPi_symm_apply_coe, finCongr_apply_coe, monotone_toDual_comp_iff, OrderMonoidHom.inrₗ_apply, ofLex_neg, CategoryTheory.Functor.sectionsEquivHom_naturality, Set.Finite.subtypeEquivToFinset_apply_coe, CategoryTheory.evalEquiv_apply, MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_val, CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply, strictAnti_toDual_comp_iff, AffineBasis.basisOf_reindex, Real.sinhEquiv_apply, FintypeCat.equivEquivIso_apply_inv, finSumFinEquiv_symm_apply_castAdd, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, sInfHom.dual_apply_toFun, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, Equiv.sigmaUnique_apply, MonoidHom.coe_toAdditive_map, AlgEquiv.opComm_apply_apply, IsPGroup.powEquiv_apply, CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply, Equiv.plift_symm_apply, SSet.stdSimplex.map_apply, ofLex_natCast, QuaternionAlgebra.lift_apply, DFA.reindex_refl, toAdd_pow, Matrix.comp_toSquareBlock, Interval.dual_bot, AddEquiv.symmEquiv_apply_symm_apply, Pi.lex_desc, CovBy.toDual, toColex_one, CategoryTheory.CartesianClosed.homEquiv_symm_apply_eq, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, CategoryTheory.conjugateEquiv_whiskerRight, DomMulAct.smul_aeeqFun_aeeq, NonemptyInterval.dual_map₂, ofColex_inv, Equiv.sumIsLeft_apply, NonUnitalRingHom.op_symm_apply_apply, InfHom.dual_comp, DFinsupp.Colex.le_iff_of_unique, RingEquiv.coe_mk, CategoryTheory.bijection_symm_apply_id, nhds_toAdd, HNNExtension.NormalWord.unitsSMulGroup_snd, ofDual_sInf, Equiv.Set.rangeInr_apply_inr, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, Sum.Lex.toLex_le_toLex, Orientation.map_eq_det_inv_smul, Equiv.instAssociativeCoeForallForallArrowCongr, Specialization.toEquiv_le_toEquiv, Metric.Snowflaking.image_ofSnowflaking_closedEBall, SSet.ι₀_snd, ComplexShape.symmetryEquiv_apply_coe, ComplexShape.symmetryEquiv_symm_apply_coe, Matrix.cramer_reindex, Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply, Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem, Sym.equivCongr_apply, Equiv.trans_def, Rep.resIndAdjunction_homEquiv_symm_apply, Finset.toDual_inf', DirectSum.decompose_mul_add_left, AddUnits.addRight_apply, CategoryTheory.Localization.homEquiv_comp, Equiv.piFinsetUnion_right, Metric.Snowflaking.preimage_toSnowflaking_closedBall, Subgroup.quotientEquivProdOfLE_symm_apply, OrderIso.conj_apply, DomMulAct.isQuotientMap_mk_symm, RootPairing.pairingIn_reflectionPerm_self_left, CategoryTheory.Enriched.FunctorCategory.homEquiv_comp, CategoryTheory.ShortComplex.Homotopy.equivSubZero_symm_apply, CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app, CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp, TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage, Equiv.punitProd_apply, MonoidAlgebra.lift_apply', toLex_pow, RingQuot.eq_lift_comp_mkRingHom, SymAlg.sym_inv, Matrix.adjugate_fin_three_of, CategoryTheory.Bicategory.conjugateIsoEquiv_apply_inv, CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc, equicontinuousOn_iff_continuousOn, SSet.StrictSegal.spineInjective, ContinuousMap.sigmaEquiv_symm_apply, Module.Basis.repr_reindex, coe_ofLexMulEquiv, SymAlg.sym_unsym, AddEquiv.add_submonoid_map_symm_apply, Abelianization.lift_of_comp, MvPolynomial.renameEquiv_apply, toDual_compl, CategoryTheory.ProjectiveResolution.of_def, ArchimedeanClass.FiniteElement.val_sub, MonoidHom.fiberEquivKer_apply, Finsupp.DegLex.single_antitone, Finsupp.Lex.single_lt_iff, PerfectRing.liftEquiv_symm_apply, Primrec.of_equiv, WithCStarModule.equiv_symm_smul, FreeNonUnitalNonAssocAlgebra.lift_symm_apply, FreeSemigroup.lift_symm_apply, CategoryTheory.Functor.corepresentableByUliftFunctorEquiv_apply_homEquiv, Equiv.pow_def, UniformOnFun.lipschitzWith_iff, Equiv.prodCongr_apply, OrderDual.toDual_lt_toDual, toBoolAlg_add_add_mul, AddHom.op_symm_apply_apply, ofMul_image_powers_eq_multiples_ofMul, CategoryTheory.mateEquiv_hcomp, Equiv.image_compl, Topology.WithUpperSet.isUpperSet_toUpperSet_preimage, Valuation.toAddValuation_apply, Shrink.ext_iff, Equiv.subtypeEquivRight_symm_apply, CategoryTheory.Functor.curryingEquiv_apply_obj, CategoryTheory.Sieve.overEquiv_symm_pullback, DomAddAct.comap_mk.symm_nhds, PEquiv.toMatrix_toPEquiv_mul, FreeAddGroup.lift_of_eq_id, CategoryTheory.yonedaEquiv_yoneda_map, CliffordAlgebra.even.lift_ι, Matrix.reindex_isTotallyUnimodular, OrthonormalBasis.reindex_apply, Fin.insertNthEquiv_symm_apply, Algebra.embeddingsMatrixReindex_eq_vandermonde, CompleteOrthogonalIdempotents.equiv, Quaternion.equivProd_apply, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, isClosedMap_toAdd, MeasureTheory.Measure.infinitePiNat_map_piCongrLeft, toLex_ratCast, Zsqrtd.lift_symm_apply_coe, Algebra.adjoin_range_eq_range_freeAlgebra_lift, Orientation.rightAngleRotation_map', CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc, SemilatSupCat.dual_map, Equiv.Finset.union_symm_left, WithZero.lift_coe, Matrix.kroneckerMap_reindex_left, Finset.Colex.ofColex_top, TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf, RootPairing.flipEquiv_symm_apply, Set.LeftInvOn.extendDomain, genericPoints.equiv_apply, Equiv.prodComm_apply, lipschitzOnWith_cfc_fun, CategoryTheory.unit_conjugateEquiv_symm, CategoryTheory.CatEnrichedOrdinary.Hom.id_eq, Additive.toMul_lt, ManyOneEquiv.of_equiv, CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app, Equiv.addRight_symm_apply, Subgroup.coe_toAddSubgroup_symm_apply, Equiv.Set.sumCompl_symm_apply_of_mem, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, WithCStarModule.linearEquiv_apply, ZMod.lift_castAddHom, Finset.ofDual_sup', Equiv.subtypeQuotientEquivQuotientSubtype_mk, Nat.divModEquiv_symm_apply, Matrix.toLin'_reindex, HahnModule.coeff_smul_order_add_order, HahnModule.of_symm_smul, CategoryTheory.Discrete.equivalence_functor, IsMaxOn.dual, Subgroup.IsComplement.equiv_snd_eq_one_of_mem_of_one_mem, CategoryTheory.unit_conjugateEquiv, sSupHom.dual_apply_toFun, EquivLike.coe_symm_apply_apply, Matrix.mul_mul_right, isClosedMap_ofDual, AddEquiv.arrowCongr_apply, DomAddAct.symm_mk_zsmul, Monoid.PushoutI.homEquiv_symm_apply, Sum.Lex.toLexRelIsoLE_symm_coe, equivShrink_symm_top, Equiv.Set.sumCompl_symm_apply, CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_right, DomMulAct.mk_smul_indicatorConstLp, CategoryTheory.Groupoid.isoEquivHom_apply, CategoryTheory.Enriched.FunctorCategory.homEquiv_id, Equiv.addEquiv_apply, DFinsupp.Colex.lt_iff, toLex_intCast, PartENat.withTopEquiv_symm_ofNat, CategoryTheory.Groupoid.isoEquivHom_symm_apply_hom, UniformOnFun.continuous_rng_iff, AlgebraicGeometry.affineOpensRestrict_apply_coe_coe, Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open', ofDegLex_inj, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', FreeAddMonoid.ofList_nil, Prod.Lex.sumLexProdLexDistrib_apply, CategoryTheory.FunctorToTypes.shrink_map, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_φ, CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as, Matrix.ofNat_fin_three, FreeAddMonoid.toList_map, finSuccEquiv'_at, Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Function.Embedding.congr_apply, Matrix.comp_apply, WithOne.lift_one, CategoryTheory.EnrichedOrdinaryCategory.homEquiv_id, Monotone.dual_left, Equiv.psigmaEquivSigma_apply, CategoryTheory.Localization.homEquiv_symm_apply, SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe, CategoryTheory.ObjectProperty.galoisConnection_isColocal, ZMod.lift_comp_coe, Equiv.Perm.subtypeEquivSubtypePerm_apply_of_mem, CategoryTheory.Groupoid.invEquiv_apply, MulArchimedeanOrder.lt_def, finSuccEquiv'_ne_last_apply, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Matrix.adjugate_reindex, UniformConvergenceCLM.topologicalSpace_eq, ofAdd_smul, CategoryTheory.CountableCategory.instLocallySmallObjAsType, isAddRightRegular_toLex, LieModuleEquiv.toEquiv_injective, Matrix.compRingEquiv_symm_apply, Multiplicative.ofAdd_strictMono, equivShrink_div, CategoryTheory.unitCompPartialBijective_natural, MulEquiv.AddMonoid.End_apply, MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, Finsupp.sumFinsuppEquivProdFinsupp_symm_inr, BoundedLatticeHom.dual_symm_apply_toFun, CategoryTheory.typeEquiv_counitIso_inv_app_val_app, ofLex_toLex, UniformFun.isometry_ofFun_boundedContinuousFunction, Field.Emb.Cardinal.equivSucc_coherence, finCycle_symm_apply, DomMulAct.symm_mk_one, CategoryTheory.FinCategory.objAsTypeToAsType_map, WithBot.toDual_apply_bot, WithTop.orderIsoSumLexPUnit_top, UniformFun.toFun_smul, Function.fromTypes_succ_equiv_symm_apply, CategoryTheory.Localization.SmallHom.equiv_mk, Equiv.hasProd_iff, ofMul_image_zpowers_eq_zmultiples_ofMul, AddMonoidHom.liftOfRightInverse_comp, Equiv.subtypeEquivCodomain_apply, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map, CategoryTheory.Functor.flippingEquiv_symm_apply_map_app, Set.uIcc_ofDual, Equiv.Perm.set_support_inv_eq, CategoryTheory.MorphismProperty.gc_llp_rlp, Finpartition.exists_enumeration, RightOrdContinuous.orderDual, Finset.Colex.lt_iff_exists_filter_lt, AntitoneOn.dual_right, toAdd_eq_zero, FreeMonoid.ofList_nil, UniformFun.ofFun_zero, CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft, UniformEquiv.coe_symm_toEquiv, CoxeterSystem.lengthParity_comp_simple, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_apply, SetTheory.PGame.default_nim_one_leftMoves_eq, Multiplicative.toAdd_eq_top, CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_φ, Function.FromTypes.curryEquiv_symm_apply, SheafOfModules.freeHomEquiv_comp_apply, TopologicalSpace.Compacts.equiv_symm_apply, isLowerSet_preimage_ofDual_iff, AffineEquiv.toEquiv_injective, WithZero.val_inv_expOrderIso_apply, CategoryTheory.shrinkYonedaEquiv_naturality, IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le, RingQuot.liftAlgHom_mkAlgHom_apply, OrderIso.compl_symm_apply, UniformFun.ofFun_div, Ioi_orderDual_def, Rack.invAct_apply, ContinuousMap.equivBoundedOfCompact_apply, Quiver.Hom.opEquiv_apply, Equiv.sumCompl_apply_inr, Equiv.withTopSubtypeNe_symm_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Subgroup.IsComplement.equiv_fst_mul_equiv_snd, Subgroup.quotientEquivProdOfLE'_symm_apply, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc, MonovaryOn.dual_right, HahnSeries.leadingCoeff_pos_iff, CategoryTheory.ComposableArrows.arrowEquiv_symm_apply, Cardinal.mk_equiv_eq_arrow_of_lift_eq, RingQuot.lift_unique, FreeAddMonoid.freeAddMonoidCongr_of, CategoryTheory.yonedaEquiv_naturality', FreeMonoid.count_of, AddEquiv.mulOp_symm_apply, monovaryOn_toDual_right, ofBoolRing_le_ofBoolRing_iff, RootPairing.Hom.coroot_coweightMap, Topology.WithUpper.isOpen_preimage_ofUpper, Equiv.prodPProd_apply, antivary_toDual_right, ofBoolAlg_mul_ofBoolAlg_eq_left_iff, Topology.WithLower.isOpen_def, AddAut.conj_inv_apply, MaximalSpectrum.equivSubtype_symm_apply_asIdeal, CategoryTheory.Localization.SmallShiftedHom.equiv_mk, SymAlg.invOf_sym, CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_obj, QuotientAddGroup.equivIcoMod_symm_apply, toDual_min, EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi, CompleteLatticeHom.symm_dual_id, SSet.ι₁_snd_assoc, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, finTwoArrowEquiv_symm_apply, Prod.Lex.uniqueProd_apply, Equiv.withTopCongr_apply, Matrix.ofNat_fin_two, FreeMonoid.toList_cons, NormedAddGroupHom.Equalizer.liftEquiv_apply, AddChar.coe_toAddMonoidHomEquiv, toLex_zero, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal, CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe, CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app, CategoryTheory.Functor.flippingEquiv_symm_apply_obj_obj, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', finEquivMultiples_symm_apply, CStarMatrix.toCLM_apply_single, Finset.Colex.toColex_le_toColex, Equiv.graph_inv, Finset.equivBitIndices_symm_apply, t1Space_TFAE, Equiv.piCongr'_symm_apply_symm_apply, DirectSum.decompose_symm_algebraMap, OrderIso.sumLexCongr_apply, Equiv.eq_comp_symm, Topology.WithLawson.isOpen_def, CategoryTheory.Functor.curryingFlipEquiv_apply_obj, FreeAddMonoid.ofList_toList, AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply, CategoryTheory.Iso.toEquiv_fun, Equiv.injective_comp, StrictAnti.dual_left, WithCStarModule.equiv_zero, Cardinal.mk_equiv_of_eq, edist_toAdd, Finset.Icc_orderDual_def, Equiv.Finset.union_symm_right, AlgEquiv.funUnique_apply, ContinuousAlgEquiv.cast_symm_apply, Finset.Ioo_toDual, Fin.cycleRange_symm_zero, Concept.swapEquiv_apply, Set.Ico_toDual, Finset.map_toDual_min, Matroid.mapEquiv_dep_iff, AlgEquiv.toRingEquiv_unop, Set.powersetCard.ofFinEmbEquiv_symm_apply, WithBot.toDualTopEquiv_coe, Matrix.det_reindex, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, AlgebraicGeometry.IsOpenImmersion.opensEquiv_apply_coe, ofBoolRing_zero, RingQuot.liftAlgHom_unique, ofDual_eq_one, ofDual_compl, multiplesHom_symm_apply, MvPolynomial.universalFactorizationMapPresentation_map, isLeft_finSumNatEquiv_symm_apply, IsTop.ofDual, isOpenMap_toAdd, Equiv.ulift_symm_apply, SetSemiring.add_def, ContinuousMap.unitsLift_apply_inv_apply, DirectSum.decompose_symm_add, codisjoint_ofDual_iff, Set.Icc_ofDual, Additive.ofMul_strictMono, CategoryTheory.uliftYonedaEquiv_uliftYoneda_map, CategoryTheory.Localization.SmallShiftedHom.equiv_shift', groupCohomology.norm_ofAlgebraAutOnUnits_eq, ofDual_neg, Matrix.reindexLieEquiv_apply, FreeGroup.range_lift_eq_closure, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal, Additive.ofMul_mono, MeasureTheory.VectorMeasure.equivMeasure_symm_apply, AddChar.toMonoidHom_apply, UniformFun.edist_le, WithLp.equiv_symm_apply, finCycle_apply, CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_map_term, ArchimedeanOrder.of_val, Affine.Simplex.touchpointWeights_reindex, Multiplicative.toAdd_image_nsmul, Fin.coe_of_injective_castLE_symm, DomMulAct.isClosedEmbedding_mk_symm, isMax_toDual_iff, Set.powersetCard.mem_compl, CategoryTheory.Adjunction.mkOfHomEquiv_unit_app, AddMonoidHom.toMultiplicative_id, Additive.toMul_strictMono, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, ofAdd_sum, MulEquiv.toMultiplicative_toAdditive_symm_apply, UniformOnFun.topologicalSpace_eq, FreeMonoid.comp_lift, TrivSqZeroExt.liftEquiv_apply, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, AddChar.toAddMonoidHomEquiv_symm_zero, Equiv.coe_vaddConst_symm, Cardinal.mk_equiv_eq_zero_iff_ne, isAtom_dual_iff_isCoatom, Module.Basis.coe_reindex, CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe, CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd, Sym.cast_cast, MeasurableEquiv.measurable_invFun, Equiv.sumAssoc_apply_inl_inr, DomMulAct.mk_smul_mulActionHom_apply, Set.Ioo_ofDual, CategoryTheory.LocalizerMorphism.equiv_smallHomMap', Rep.resIndAdjunction_homEquiv_apply, equivShrink_mul, RingQuot.lift_mkRingHom_apply, groupCohomology.isMulCocycle₂_of_mem_cocycles₂, MvPolynomial.supDegree_esymm, CStarMatrix.toCLM_apply_eq_sum, CategoryTheory.coyonedaEquiv_naturality, Matrix.cons_transpose, DFinsupp.linearEquivFunOnFintype_symm_apply, Equiv.Perm.decomposeOption_symm_of_none_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, LieAlgebra.LieEquiv.ofCoboundary_toFun, DirectSum.coe_decompose_mul_of_right_mem_of_not_le, PadicInt.coe_adicCompletionIntegersEquiv_apply, DomAddAct.mk_add, Equiv.invOn, Order.IsSuccLimit.dual, DirectSum.coe_decompose_mul_of_left_mem_of_not_le, FreeCommRing.lift_comp_of, DFinsupp.equivCongrLeft_apply, CategoryTheory.coyonedaEquiv_apply, UniformFun.toFun_one, Topology.WithUpper.ofUpper_toUpper, Metric.Snowflaking.toSnowflaking_ofSnowflaking, ComplexShape.Embedding.AreComplementary.equiv_inl, AlgEquiv.piCongrLeft'_apply, Topology.WithUpper.toUpper_lt_toUpper, Subgroup.IsComplement.equiv_symm_apply, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, Equiv.pprodCongr_symm_apply, CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app, UniversalEnvelopingAlgebra.lift_ι_apply, SSet.ι₁_snd, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, FreeLieAlgebra.lift_unique, AlgEquiv.piCongrLeft_apply, Rack.toEnvelGroup.univ, NumberField.mixedEmbedding.logMap_eq_logEmbedding, ofDegLex_toDegLex, Equiv.semiconj₂_conj, SSet.Truncated.StrictSegal.spineInjective, DyckWord.equivTree_symm_apply, Equiv.conj_comp, SimpleGraph.incMatrix_mul_transpose, FreeAddGroup.map_eq_lift, Homeomorph.piCongrLeft_apply, RootPairing.reflectionPerm_root, QuaternionAlgebra.lift_symm_apply, Prod.Lex.toLex_lt_toLex, Equiv.piCongrSigmaFiber_apply, ContinuousMultilinearMap.prodEquiv_symm_apply, Continuous.homeoOfEquivCompactToT2.t1_counterexample, AddSubgroup.IsComplement.rightQuotientEquiv_apply, Multiset.map_univ_val_equiv, AddMonoidHom.op_symm_apply_apply, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, Specialization.ofEquiv_inj, Tropical.tropEquiv_symm_coe_fn, sigmaFinsuppEquivDFinsupp_smul, Cardinal.lift_mk_eq', FreeAddMonoid.toList_of_add, Equiv.ofLeftInverseOfCardLE_apply, AddEquiv.mulOp_apply, toAdd_ofAdd, Monoid.CoprodI.Word.equivPair_symm, Set.up_empty, AddEquiv.toMultiplicativeRight_symm_apply_apply, Quaternion.equivTuple_apply, ContinuousMap.val_addUnitsLift_apply_apply, strictMonoOn_toDual_comp_iff, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map, OrderMonoidIso.withZero_apply_apply, Equiv.optionSubtypeNe_symm_apply, CategoryTheory.PreOneHypercover.inter_p₂, Matrix.of_apply, exteriorPower.ιMultiDual_apply_ιMulti, Homeomorph.continuous_sumAssoc, Matrix.diagonal_kroneckerTMul, edist_toMul, finSuccEquiv'_below, UniformFun.lipschitzWith_ofFun_iff, PiTensorProduct.lift_comp_reindex, CategoryTheory.WithTerminal.isLimitEquiv_symm_apply_lift, isRightRegular_toDual, FreeGroupBasis.reindex_apply, DomMulAct.isEmbedding_mk, FirstOrder.Language.Formula.equivSentence_inf, HomotopicalAlgebra.AttachCells.reindex_π, CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm, Equiv.Perm.refl_inv, Cardinal.lift_mk_eq, nnnorm_ofAdd, Equiv.prodCongrLeft_apply_fst, Matrix.vecMul_permMatrix, Finset.Colex.toColex_lt_singleton, AddEquiv.piAdditive_symm_apply, PrimeSpectrum.primeSpectrumProd_symm_inr, AddOpposite.opEquiv_apply, List.SortedGT.of_map_ofDual, IsGLB.dual, toMul_zsmul, Equiv.funUnique_apply, Finsupp.prod_hom_add_index, WithZero.toMulBot_coe_ofAdd, Algebra.TensorProduct.liftEquiv_apply, Matrix.toLin_finTwoProd_apply, Metric.Snowflaking.ediam_preimage_ofSnowflaking, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, LatticeHom.dual_id, CategoryTheory.Limits.Types.limitEquivSections_symm_apply, CategoryTheory.Adjunction.homAddEquiv_add, Antitone.dual, Equiv.Perm.perm_symm_mapsTo_iff_mapsTo, isExtrOn_dual_iff, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, FreeMonoid.lift_eval_of, InfIrred.dual, toDual_hnot, Matrix.diagonal_fin_one, BddDistLat.dual_map, DFA.reindex_apply_start, Finset.Colex.singleton_lt_singleton, CliffordAlgebra.reverseOpEquiv_opComm, CStarMatrix.reindexₐ_apply, ofDual_ratCast, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor, Equiv.sigmaUnique_symm_apply, AddGrpCat.toGrp_map, CStarMatrix.ofMatrix_eq_ofMatrixL, Matrix.rank_submatrix, Prod.Lex.covBy_iff, toAdd_one, MulOpposite.opEquiv_apply, Multiplicative.toAdd_eq_bot, exteriorPower.pairingDual_ιMulti_ιMulti, UniformFun.toFun_prod, FreeMonoid.toList_of_mul, Equiv.Set.sumDiffSubset_symm_apply_of_notMem, Homeomorph.image_apply_coe, Pi.lt_toColex_update_self_iff, Equiv.ofBijective_symm_apply_apply, Shrink.algEquiv_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, CategoryTheory.Bicategory.conjugateEquiv_symm_comm, Set.uIcc_toDual, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, Setoid.prodQuotientEquiv_symm_apply, AddSubgroup.vadd_leftQuotientEquiv, Matrix.val_planeConformalMatrix, CategoryTheory.Bicategory.mateEquiv_symm_apply, CategoryTheory.Functor.Elements.initialOfCorepresentableBy_snd, finTwoArrowEquiv_apply, Equiv.iInf_comp, Finsupp.fst_sumFinsuppEquivProdFinsupp, Equiv.ofBijective_apply, StrictMono.dual_left, ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply, toColex_neg, groupHomology.H1AddEquivOfIsTrivial_single, SymAlg.sym_eq_one_iff, PresheafOfModules.homEquivOfIsLocallyBijective_apply, WithTop.ofDual_apply_coe, Module.Basis.det_reindex, CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd, Set.opEquiv_self_apply_coe, Set.Ioc_toDual, WithZero.lift'_unique, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, equicontinuous_iff_continuous, Equiv.optionSubtype_symm_apply_apply_none, PresheafOfModules.unitHomEquiv_apply_coe, Equiv.optionEquivSumPUnit_none, Rep.coindResAdjunction_homEquiv_apply, ContinuousMap.continuous_iff_continuous_uniformFun, SimpleGraph.Walk.IsHamiltonian.supportGetEquiv_apply, CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_apply, CategoryTheory.Limits.WidePullbackShape.equivalenceOfEquiv_functor_obj_some, Matroid.mapEquiv_ground_eq, AddMonoidAlgebra.lift_single, Finsupp.Colex.le_iff_of_unique, tangentBundle_model_space_coe_chartAt_symm, CategoryTheory.PreZeroHypercover.interSnd_h₀, Equiv.coe_piCongr', Finsupp.Lex.le_iff_of_unique, Topology.WithUpperSet.ofUpperSet_le_iff, CategoryTheory.conjugateEquiv_symm_comp, Affine.Simplex.range_faceOpposite_reindex, WithTop.toDual_apply_top, coe_equiv_lpPiLp, HahnEmbedding.Seed.coeff_baseEmbedding, Affine.Simplex.altitudeFoot_reindex, Matrix.dualNumberEquiv_symm_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, finSumFinEquiv_symm_last, tangentBundleModelSpaceHomeomorph_coe, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv, FreeMonoid.ofList_cons, Matrix.cons_mul, MulOpposite.opEquiv_symm_apply, UniformFun.toFun_div, DirectSum.decompose_algebraMap, Monoid.CoprodI.Word.mem_equivPair_tail_iff, Iic_orderDual_def, SupHom.symm_dual_id, ofBoolAlg_symmDiff, CategoryTheory.Limits.Trident.IsLimit.homIso_apply_coe, UniformOnFun.ofFun_sub, AddMonoidHom.coe_toMultiplicative', Equiv.image_eq_preimage, CategoryTheory.Sheaf.ΓObjEquivHom_naturality_symm, Equiv.subLeft_symm_apply, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply, MonoidHom.op_symm_apply_apply, SetSemiring.one_def, RootPairing.Equiv.comp_indexEquiv_symm_apply, IndexedPartition.equivQuotient_index_apply, Equiv.ofInjective_symm_apply, Equiv.subtypeEquivRight_symm_apply_coe, Additive.ofMul_le, nnnorm_toDual, Function.piCongrLeft'_update, Finsupp.DegLex.lt_iff, CategoryTheory.tensorRightHomEquiv_naturality, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, Equiv.piCongrLeft_sumInl, equivTangentBundleProd_symm_apply_snd, CircleDeg1Lift.translate_apply, Valuation.ofAddValuation_toAddValuation, CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app, Traversable.foldl.unop_ofFreeMonoid, Function.updateFinset_updateFinset, Equiv.option_symm_apply_none_iff, Equiv.finite_left, MvPolynomial.leadingCoeff_toLex_C, Equiv.smul_def, AddMonoidAlgebra.lift_symm_apply, RootPairing.coroot_eq_neg_iff, toColex_smul, Matrix.one_submatrix_mul, FinPartOrd.dual_map, ContinuousMap.coe_equivFnOfDiscrete, CompleteLat.dual_map, Equiv.Perm.coe_inv, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply, SimpleGraph.Walk.IsHamiltonian.supportGetEquiv_symm_apply_val, Submodule.singleton_smul, toColex_vadd', MulEquiv.op_apply_apply, circleEquivGen_symm_apply, Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt, Quiver.Hom.opEquiv_symm_apply, Matrix.reindex_updateRow, InfTopHom.dual_comp, WeakDual.CharacterSpace.compContinuousMap_apply, CategoryTheory.tensorRightHomEquiv_tensor, lipschitzOnWith_cfcₙ_fun, maximal_toDual, RootPairing.root_eq_neg_iff, Equiv.finite_right, DomAddAct.vadd_aeeqFun_aeeq, Hamming.toHamming_smul, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_f_coe, CategoryTheory.Localization.SmallShiftedHom.equiv_chgUniv, CStarMatrix.toCLM_apply, CategoryTheory.Subfunctor.range_eq_ofSection', AddEquiv.symm_map_add, CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt, Hamming.toHamming_add, NonUnitalStarAlgHom.prodEquiv_apply, FreeAddMagma.lift_comp_of', BoundedLatticeHom.symm_dual_id, CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv, uliftMultiplesHom_apply_apply, CategoryTheory.CatEnrichedOrdinary.Hom.base_comp, Multiset.cast_apply_fst, CategoryTheory.Functor.RepresentableBy.equivOfIsoObj_apply, SheafOfModules.conjugateEquiv_pullbackComp_inv, MulEquiv.multiplicativeAdditive_apply, Additive.toMul_bot, Finsupp.equivFunOnFinite_symm_coe, AddEquiv.addMonoidHomCongrRightEquiv_symm_apply, finSumFinEquiv_symm_apply_natAdd, Metric.Snowflaking.ofSnowflaking_toSnowflaking, Delone.DeloneSet.mapIsometry_refl, Submodule.isIdempotentElemEquiv_apply_coe, powCoprime_apply, LinearEquiv.piCongrLeft'_symm_apply, List.sortedLE_map_toDual, AddChar.toAddMonoidHomEquiv_symm_apply, MulEquiv.monoidHomCongrRightEquiv_apply, CategoryTheory.Functor.corepresentableByUliftFunctorEquiv_symm_apply_homEquiv, SymAlg.unsym_smul, CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv, Equiv.preimage_subset, FirstOrder.Language.BoundedFormula.realize_relabelEquiv, Matrix.BlockTriangular.comp, Equiv.finsuppUnique_symm_apply_apply, Function.FromTypes.uncurry_two_eq_uncurry, CategoryTheory.discreteEquiv_symm_apply_as, AddEquiv.toMultiplicative_apply_apply, Order.IsPredLimit.dual, Sym.mem_cast, Encodable.decode_ofEquiv, Metric.Snowflaking.image_toSnowflaking_eq_preimage, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq, Unitization.lift_range, DomAddAct.vadd_Lp_ae_eq, FintypeCat.equivEquivIso_symm_apply_apply, Sym2.coe_lift_symm_apply, AddAction.IsBlock.of_addSubgroup_of_conjugate, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two, RootPairing.Hom.indexEquiv_mul, Finsupp.lex_lt_iff_of_unique, CategoryTheory.Limits.IsColimit.homEquiv_symm_naturality, CStarMatrix.smul_of, RelIso.IsWellOrder.preimage, UniformFun.dist_le, CategoryTheory.Equivalence.induced_inverse_map, CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_symm_apply, Equiv.existsUnique_congr_left, FreeGroup.closure_eq_range, SupBotHom.dual_id, CategoryTheory.nerve.homEquiv_id, AddChar.toMonoidHomEquiv_symm_one, WithCStarModule.linearEquiv_symm_apply, CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ι, gc_Ici_sInf, FormalMultilinearSeries.changeOriginIndexEquiv_apply_fst, SetTheory.PGame.moveRight_neg, IsMin.ofDual, Equiv.equivCongr_trans, Matrix.submatrix_updateRow_equiv, LinearMap.polar_gc, Zsqrtd.lift_apply_apply, Equiv.induced_symm, val_unitsEquivProdSubtype_symm_apply, DividedPowers.equiv_apply', Equiv.Set.image_symm_preimage, Subgroup.quotientEquivSigmaZMod_apply, CategoryTheory.Functor.isIso_ranAdjunction_homEquiv_iff, toAdd_vadd, LE.le.dual, TwoSidedIdeal.coe_equivMatrix_symm_apply, Fin.consEquiv_symm_apply, FreeMonoid.toList_map, Equiv.sumCompl_apply_symm_of_neg, Equiv.cast_apply, ContinuousLinearEquiv.coe_prodProdProdComm, Equiv.sumCongr_apply, BoundedOrderHom.dual_comp, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, Equiv.subtypeEquivCodomain_symm_apply_eq, derivationToSquareZeroEquivLift_symm_apply_apply_coe, Delone.DeloneSet.mapIsometry_symm_apply_packingRadius, CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply, MonoidHom.coe_toAdditiveLeft, CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_map, Denumerable.ofEquiv_ofNat, FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply, CliffordAlgebra.lift_symm_apply, SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk, Int.tendsto_zmultiplesHom_cofinite, Subgroup.IsComplement.rightCosetEquivalence_equiv_snd, Equiv.inducedStructure_funMap, MeasurableEquiv.piCongrLeft_apply_apply, Set.SurjOn.extendDomain, CategoryTheory.CoreSmallCategoryOfSet.functor_map, Matrix.submatrix_id_mul_left, Equiv.sigmaAssocProd_symm_apply_snd, WithBot.toDual_le_iff, Nat.image_piFinTwoEquiv_finMulAntidiag, Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero, finEquivZMultiples_apply, Equiv.Perm.one_symm, FreeAddGroup.freeAddGroupCongr_apply, AddMonoidAlgebra.GradesBy.decompose_single, Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe, ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply, Nat.pairEquiv_symm_apply, Equiv.comp_bijective, Matrix.compLinearEquiv_symm_apply, AddEquiv.prodAdditive_apply, freeGroupEquivCoprodI_symm_apply, WithBot.ofDual_lt_iff, Filter.Realizer.ofEquiv_F, UniformOnFun.lipschitzWith_eval, Submodule.coe_isComplEquivProj_apply, MvPolynomial.monic_esymm, CategoryTheory.mateEquiv_symm_apply, QuadraticAlgebra.lift_symm_apply_coe, Equiv.ofFiberEquiv_apply, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply, AlgEquiv.op_symm_apply_symm_apply, ArchimedeanClass.FiniteResidueField.mk_eq_mk, CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to, ofLex_one, Interval.dual_pure, UniversalEnvelopingAlgebra.lift_symm_apply, Finset.Ico_ofDual, Topology.WithLowerSet.toLowerSet_inj, MaximalSpectrum.equivSubtype_apply_coe, OnePoint.equivProjectivization_symm_apply_mk, translate_eq_domAddActMk_vadd, RootPairing.pairingIn_reflectionPerm_self_right, Metric.Snowflaking.preimage_toSnowflaking_eball, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply, Finsupp.equivMapDomain_eq_mapDomain, RingEquiv.coe_toEquiv, Equiv.Perm.mul_symm, Additive.ext_iff, Monoid.CoprodI.Word.equivPair_tail, WithBot.toDual_apply_coe, Finset.toDual_inf, CategoryTheory.Functor.curryingEquiv_symm_apply_map_app, ContinuousMap.toUniformOnFun_toFun, AddValuation.ofValuation_toValuation, isAddRegular_toLex, coe_finRotate_symm_of_ne_zero, SetTheory.PGame.forall_rightMoves_neg, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, Topology.WithUpperSet.toUpperSet_le_iff, Finset.Ioc_orderDual_def, FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_fst, SSet.Subcomplex.PairingCore.equivI_apply_coe, CategoryTheory.Presheaf.uliftYonedaAdjunction_homEquiv_app, SetTheory.PGame.forall_leftMoves_neg, Quiver.SingleObj.toHom_apply, Finset.toDual_max', Finset.Colex.insert_le_insert, Order.PFilter.sInf_gc, CategoryTheory.Bicategory.conjugateEquiv_symm_comp, CommBialgCat.isoEquivBialgEquiv_symm_apply, HahnModule.ext_iff, Multiplicative.ofAdd_bot, Set.coe_snd_unionEqSigmaOfDisjoint, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc, CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst_assoc, CategoryTheory.CommSq.right_adjoint_hasLift_iff, RingEquiv.sumArrowEquivProdArrow_symm_apply, WithBot.toDual_lt_toDual_iff, FreeAddMonoid.lift_comp_of, Quiver.starEquivCostar_apply_snd, CategoryTheory.Limits.Types.Small.limitCone_π_app, ofBoolAlg_sdiff, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply, ofColex_inj, List.sortedLT_map_ofDual, LinearEquiv.extendScalarsOfIsLocalizationEquiv_apply, UniformOnFun.uniformContinuous_toFun, RingHom.liftOfRightInverse_comp_apply, CartanMatrix.A_three, CategoryTheory.Bicategory.mateEquiv_hcomp, FreeCommRing.of_cons, Finsupp.sumFinsuppEquivProdFinsupp_symm_apply, CategoryTheory.Iso.homCongr_apply, Equiv.natSumNatEquivNat_symm_apply, PrincipalSeg.subrelIso_symm_apply, OrderIso.dualAntisymmetrization_apply, Equiv.permCongr_apply, Fintype.coe_finsetOrderIsoSet_symm, UniformEquiv.toEquiv_injective, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, Matrix.cRank_reindex, antitoneOn_comp_ofDual_iff, Matrix.col_eq_transpose, IsometryEquiv.piCongrLeft_symm_apply, Set.up_image, Equiv.Perm.refl_mul, ContinuousMultilinearMap.prodEquiv_apply, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, Set.exists_equiv_range_eq_graphOn_univ, CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_comp, FirstOrder.Language.Term.realize_constantsVarsEquivLeft, OrderDual.toDual_le, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symm, CategoryTheory.Adjunction.homEquiv_naturality_right_square_iff, CategoryTheory.conjugateEquiv_counit, Homeomorph.continuous_sumAssoc_symm, GradedRing.mem_support_iff, WCovBy.ofDual, codisjoint_toDual_iff, DualNumber.lift_apply_apply, Topology.WithUpper.ofUpper_inj, CategoryTheory.Functor.flippingEquiv_symm_apply_obj_map, WithBot.ofDual_lt_ofDual_iff, WithCStarModule.norm_single, Equiv.Perm.subtypeEquivSubtypePerm_apply_of_not_mem, WithTop.ofDual_le_ofDual_iff, EquivFunctor.mapEquiv_apply, MultilinearMap.iteratedFDeriv_aux, Matrix.rank_reindex, HahnModule.of_symm_add, Topology.WithLowerSet.ofLowerSet_le_iff, Equiv.finsetCongr_apply, CategoryTheory.Limits.isLimitConeOfAdj_lift, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, AddMonoidHom.op_apply_apply, Equiv.optionCongr_apply, Topology.WithUpper.toUpper_inj, OrderIso.sumLexIicIoi_apply_inr, DFinsupp.subtypeSupportEqEquiv_symm_apply_coe, AlgEquiv.arrowCongr_comp, Nat.Primes.coe_prodNatEquiv_apply, FreeRing.lift_comp_of, MulRingNorm.mulRingNormEquivAbsoluteValue_symm_apply, antitone_dual_iff, Matrix.piAddEquiv_symm_apply, UniformOnFun.continuousOn_eval₂, Monoid.foldlM.ofFreeMonoid_apply, Unitization.lift_symm_apply, AntitoneOn.dual_left, Topology.WithUpperSet.ofUpperSet_toUpperSet, Matrix.lift_cRank_reindex, ofDual_one, Equiv.permCongr_mul, CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp, Multiplicative.mem_toSubgroup, Equiv.Set.univ_apply, WithCStarModule.equiv_symm_sub, CategoryTheory.Adjunction.homAddEquiv_symm_zero, AddEquiv.addMonoidHomCongrLeftEquiv_symm_apply, Monoid.PushoutI.homEquiv_apply_coe, Set.PartiallyWellOrderedOn.fiberProdLex, HomotopicalAlgebra.AttachCells.reindex_cofan₂, CategoryTheory.Functor.RepresentableBy.homEquiv_comp, Finset.Ioc_toDual, Equiv.Perm.decomposeFin_symm_apply_succ, CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom, toLex_natCast, CategoryTheory.conjugateEquiv_rightUnitor_hom, Topology.IsGeneratedBy.homeomorph_coe, CategoryTheory.LocalizerMorphism.equiv_smallShiftedHomMap, Set.Iic_toDual, WittVector.liftEquiv_apply, AlgebraicGeometry.coprodSpec_coprodMk, CStarMatrix.mul_entry_mul_eq_inner_toCLM, Matrix.kronecker_assoc, ZMod.lift_comp_castAddHom, Matrix.trace_fin_one_of, AddMonoidAlgebra.lift_of, nsmulCoprime_neg, RelIso.sumLexComplRight_symm_apply, powersHom_apply, CoxeterMatrix.reindexGroupEquiv_apply_simple, ofAdd_add, WithTop.toDual_lt_toDual_iff, Finset.mem_map_equiv, ofDual_iSup, MulEquiv.symm_map_mul, Set.dual_ordSeparatingSet, CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val, AddMonoidHom.coe_toMultiplicative, SkewMonoidAlgebra.lift_unique', ConvexOn.dual, BialgEquiv.toEquiv_injective, MulAction.orbitZPowersEquiv_symm_apply, CategoryTheory.Functor.RepresentableBy.isRepresentedBy, PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply, OrderHom.dual_comp, Topology.WithScott.toScott_inj, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id, IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime_apply_coe, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul, SetSemiring.down_imageHom, Sum.Lex.inl_strictMono, Equiv.toIso_hom, MeasurableEquiv.coe_piCongrLeft, Homeomorph.sumProdDistrib_apply, MulChar.ofUnitHom_eq, PartENat.withTopEquiv_symm_one, Sym2.sortEquiv_symm_apply, FreeAbelianGroup.lift_unique, CStarMatrix.ofMatrix_symm_apply, Finset.Colex.toColex_mono, ModuleCat.homEquiv_extendScalarsComp, DirectSum.coe_decompose_mul_of_right_mem, CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_snd, CategoryTheory.CommSq.left_adjoint_hasLift_iff, WithBot.ofDual_symm_apply, CategoryTheory.Limits.Pi.reindex_inv_π, AddEquiv.symmEquiv_symm_apply_apply, Equiv.sigmaSigmaSubtype_apply, IsFreeGroup.lift_symm_apply, Equiv.prodProdProdComm_apply, FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence, PartENat.withTopEquiv_natCast, QuaternionAlgebra.re_equivProd_symm_apply, ofColex_smul, MvPolynomial.supDegree_toLex_C, ContinuousLinearEquiv.unitsEquivAut_symm_apply, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso, Sym.cons_equiv_eq_equiv_cons, Matrix.replicateRow_mul_replicateCol, Fin.revPerm_apply, AddEquiv.prodAdditive_symm_apply, Equiv.sumProdDistrib_apply_left, LieAlgebra.of_zero, Invertible.mulLeft_symm_apply, Algebra.leftMulMatrix_complex, RingHom.equivRatAlgHom_apply, Equiv.mul_def, ContinuousMultilinearMap.prodEquiv_symm_apply_snd, CategoryTheory.conjugateEquiv_mateEquiv_vcomp, isRightRegular_toLex, Algebra.Norm.Transitivity.eval_zero_comp_det, Monotone.dual_right, DomMulAct.mk_smul_mulDistribActionHom_apply, MulEquiv.symmEquiv_apply_apply, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, IsPrimitiveRoot.primitiveRootsPowEquiv_apply_coe, CategoryTheory.Limits.WidePullbackCone.reindex_π, Equiv.existsUnique_congr_right, CategoryTheory.ShiftedHom.opEquiv'_symm_apply, Finset.Icc_toDual, AddCircle.measurePreserving_equivIoc, powersMulHom_apply, BoolAlg.dual_map, Circle.argEquiv_symm_apply, UniformFun.ofFun_smul, Equiv.neg_apply, groupCohomology.cocyclesOfIsMulCocycle₂_coe, Subgroup.toAddSubgroup_closure, RootPairing.RootPositiveForm.rootLength_reflectionPerm_self, FirstOrder.Language.Term.constantsVarsEquiv_apply, Equiv.sigmaAssocProd_symm_apply_fst, Equiv.sumProdDistrib_apply_right, Equiv.divRight_apply, Hamming.ofHamming_add, ofDegLex_injective, sSupHom.dual_comp, Matrix.isHermitian_submatrix_equiv, Set.powersetCard.coe_compl, DFinsupp.equivProdDFinsupp_add, Equiv.coe_prodComm, Monovary.dual_right, ArchimedeanClass.FiniteElement.val_zero, Equiv.set_forall_iff, CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply, CategoryTheory.mateEquiv_conjugateEquiv_vcomp, CategoryTheory.CommSq.LiftStruct.opEquiv_symm_apply, SymmetricAlgebra.lift_comp_ι, WithZero.toMulBot_zero, InfPrime.ofDual, Fin.castLEquiv_apply, RootPairing.chainTopCoeff_reflectionPerm_left, CategoryTheory.Bicategory.mateEquiv_eq_iff, toLex_inv, CategoryTheory.Arrow.equivSigma_symm_apply_hom, WithZero.lift_zero, NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace_apply, SymmetricAlgebra.lift_ι, OrderMonoidHom.inlₗ_apply, ContinuousMultilinearMap.piEquiv_apply, SymAlg.unsym_injective, CircleDeg1Lift.translate_zpow, Equiv.preimage_symm_preimage, Submodule.isIdempotentElemEquiv_symm_apply_coe, DFinsupp.sigmaCurryLEquiv_symm_apply, FirstOrder.Language.Formula.realize_equivSentence_symm_con, Multiplicative.toAdd_lt, MonoidHom.toAdditiveRight_symm_apply_apply, Equiv.symm_trans_swap_trans, Equiv.optionIsSomeEquiv_apply, TopologicalSpace.IrreducibleCloseds.equivSubtype_apply, isRightRegular_toMul, AddMonoidHom.toMultiplicativeLeft_symm_apply_apply, Fin.succFunEquiv_symm_apply, linearIndependent_equiv, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, WithCStarModule.inner_single_right, FreeAddMonoid.freeAddMonoidCongr_symm_of, Matrix.cRank_submatrix, Quiver.SingleObj.toPrefunctor_id, CategoryTheory.Limits.Cotrident.IsColimit.homIso_symm_apply, CategoryTheory.Discrete.equivOfEquivalence_apply, toColex_inj, isAddRightRegular_toDual, WithLp.equiv_apply, AddEquiv.coe_toEquiv_symm, HahnModule.coeff_smul, UniformFun.precomp_uniformContinuous, parallelepiped_comp_equiv, SSet.S.equivElements_apply_fst, Int.ofAdd_mul, Finsupp.Colex.lt_iff, finAddFlip_apply_mk_left, CategoryTheory.codiscreteEquiv_apply, Nat.equivProdNatSmoothNumbers_apply', CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst, CategoryTheory.ObjectProperty.isLocal.homEquiv_apply, Equiv.mulLeft_symm_apply, ContinuousMultilinearMap.norm_ofSubsingleton_id_le, Equiv.ofRightInverseOfCardLE_apply, LatticeHom.symm_dual_comp, FreeAlgebra.ι_comp_lift, Equiv.divLeft_apply, CategoryTheory.Functor.RepresentableBy.homEquiv_unop_comp, FreeAbelianGroup.lift_comp_apply, gc_upperClosure_coe, Finsupp.equivMapDomain_symm_apply, finSuccEquiv_symm_some, Sym2.coe_lift₂_symm_apply, Multiset.coe_consEquiv_of_eq_of_lt, MulEquiv.submonoidMap_symm_apply, SimpleGraph.Iso.mapNeighborSet_apply_coe, Matrix.kronecker_assoc', UniformOnFun.edist_def', ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_apply, Monoid.CoprodI.lift_of', LinearEquiv.toEquiv_injective, Subgroup.coe_toAddSubgroup_apply, Cubic.equiv_symm_apply_b, DomAddAct.continuous_mk, LinearEquiv.sumPiEquivProdPi_symm_apply, AddEquiv.coe_prodAssoc_symm, isAddLeftRegular_toAdd, WithTop.toDual_symm_apply, SheafOfModules.Presentation.map_relations_I, Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe, WithTop.ofDual_map, Metric.Snowflaking.preimage_toSnowflaking_closedEBall, DomMulAct.comap_mk.symm_nhds, LinearEquiv.symmEquiv_apply_apply, Equicontinuous.isUniformInducing_uniformFun_iff_pi, sInfHom.dual_comp, MultilinearMap.domDomCongrLinearEquiv'_apply, WithTop.map_toDual, finEquivZMultiples_symm_apply, Equiv.Perm.IsCycle.zpowersEquivSupport_apply, CategoryTheory.Localization.homEquiv_apply, Quotient.finChoiceEquiv_apply, ComplexShape.Embedding.homEquiv_symm_apply, Equiv.prodSumDistrib_symm_apply_right, Matrix.adjugate_def, Equiv.permCongr_refl, AddChar.toMonoidHomEquiv_apply, Metric.Snowflaking.preimage_ofSnowflaking_ball, monoidEndToAdditive_symm_apply_apply, SSet.prodStdSimplex.objEquiv_map_apply, Equiv.tprod_eq, Equiv.trans_swap_trans_symm, MonoidHom.apply_mint, ContinuousMultilinearMap.domDomCongr_apply, HahnModule.coeff_single_zero_smul, SimpleGraph.Iso.comap_apply, Equiv.optionSubtype_apply_apply, SSet.stdSimplex.objEquiv_symm_mem_nonDegenerate_iff_mono, Matrix.submatrix_diagonal_equiv, ContinuousLinearEquiv.unitsEquivAut_apply_symm, Affine.Simplex.altitude_reindex, CategoryTheory.conjugateEquiv_comm, QuaternionAlgebra.equivTuple_apply, AddEquiv.toMultiplicativeRight_symm_apply_symm_apply, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three, isLeftRegular_ofDual, RingHom.op_symm_apply_apply, LinearAlgebra.FreeProduct.lift_unique, finSuccEquiv'_symm_some_below, DualNumber.coe_lift_symm_apply, Finset.sigmaAntidiagonalEquivProd_symm_apply_snd_coe, CategoryTheory.Functor.isIso_lanAdjunction_homEquiv_symm_iff, AddMonoidAlgebra.liftMagma_apply_apply, Matrix.cramer_submatrix_equiv, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst, MultilinearMap.ofSubsingletonₗ_apply, List.SortedLE.of_map_ofDual, Equiv.prod_comp, Matrix.mulVecLin_submatrix, BoundedLatticeHom.asBoolRing_apply, QuaternionAlgebra.imK_equivProd_symm_apply, List.SortedGT.of_map_toDual, piFinTwoEquiv_apply, Equiv.piEquivPiSubtypeProd_symm_apply, AddMonoid.Coprod.map_mk_ofList, DFinsupp.Lex.lt_iff_of_unique, List.SortedLT.of_map_toDual, CategoryTheory.OverPresheafAux.unitAuxAux_inv_app_fst, InverseSystem.piSplitLE_eq, finRotate_succ_symm_apply, TrivSqZeroExt.liftEquivOfComm_apply, ComplexShape.Embedding.homEquiv_apply_coe, Matrix.BlockTriangular.transpose, Equiv.sigmaSubtype_symm_apply_coe_snd, Pi.toColex_apply, CategoryTheory.Localization.SmallShiftedHom.equiv_shift, IsGalois.intermediateFieldEquivSubgroup_symm_apply, CategoryTheory.CommSq.right_adjoint, DomMulAct.mk_zpow, Nat.Partition.ofSym_map, Matrix.comp_symm_diagonal, CategoryTheory.OverPresheafAux.unitAuxAux_inv_app_snd_coe, CategoryTheory.Functor.sectionsEquivHom_naturality_symm, UniformConvergenceCLM.isUniformInducing_coeFn, SetTheory.PGame.relabel_moveRight', PartENat.withTopEquiv_top, CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two_assoc, PiTensorProduct.mem_lifts_iff, CliffordAlgebra.toBaseChange_comp_reverseOp, Equiv.preimage_eq_iff_eq_image, ContinuousOn.continuous_restrict_iff_continuous_uniformOnFun, Subgroup.transferTransversal_apply', Equiv.equivCongr_symm, CategoryTheory.Equivalence.congrLeftFunctor_map, Metric.Snowflaking.continuous_toSnowflaking, CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small, Bifunctor.mapEquiv_symm_apply, CategoryTheory.Adjunction.homAddEquiv_symm_neg, invertibleEquivOfLeftInverse_apply, GradedTensorProduct.auxEquiv_tmul, Complex.expMonoidHom_apply, OrderIso.conj_symm_apply, Sum.Lex.inl_lt_inl_iff, OrderIso.sumLexAssoc_apply_inl_inl, Equiv.coe_constVSub, CoalgEquiv.coe_symm_toEquiv, UniformFun.ofFun_prod, FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply, CategoryTheory.ReflQuiv.adj.homEquiv_apply, RootPairing.range_weylGroupToPerm, Finset.Ioi_ofDual, ArchimedeanClass.FiniteResidueField.mk_ne_zero, Diffeomorph.contMDiff_invFun, groupHomology.H1ToTensorOfIsTrivial_H1π_single, WithCStarModule.equiv_smul, MulAction.orbitEquivQuotientStabilizer_symm_apply, CategoryTheory.Bicategory.toNatTrans_mateEquiv, CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_hom, SymAlg.sym_surjective, toLex_vadd, NonemptyFinLinOrd.dual_map, DomMulAct.mk_smul_linearMap_apply, Partition.partscopyEquiv_symm_apply_coe, Submodule.dualAnnihilator_gc, AddMonoidAlgebra.liftNC_single, Topology.WithLowerSet.toLowerSet_le_iff, Equiv.Perm.decomposeOption_symm_sign, Equiv.equiv_subsingleton_dom, Topology.WithGeneratedByTopology.continuous_from_iff, Finsupp.DegLex.single_le_iff, Units.mulLeft_apply, Equiv.ofInjective_apply, Equiv.locallyFinite_comp_iff, CategoryTheory.Localization.SmallHom.equiv_chgUniv, HahnSeries.archimedeanClassOrderIsoWithTop_apply, Order.succ_toMul, SetTheory.PGame.Domineering.shiftRight_symm_apply, DirectSum.decomposeLinearEquiv_apply, prodEquivPiFinTwo_apply, EuclideanSpace.piLpCongrLeft_single, Order.isPredLimit_toDual_iff, bddBelow_preimage_ofDual, CategoryTheory.Limits.Bicone.whisker_π, BddBelow.dual, Submonoid.equivOp_apply_coe, Ideal.associatesEquivIsPrincipal_symm_apply, CategoryTheory.equivYoneda_hom_app, NumberField.conj_basisMatrix, Topology.WithUpperSet.ofUpperSet_le_ofUpperSet, equivIsoIso_inv, CategoryTheory.Limits.Pi.whiskerEquiv_hom, OrderIso.neg_symm_apply, Matrix.submatrix_one_equiv, Orientation.rotation_eq_matrix_toLin, CategoryTheory.unit_mateEquiv_symm, MonotoneOn.dual, OrderAddMonoidHom.inlₗ_apply, toDual_sub, HasDerivAt.hasFDerivAt_equiv, AddEquiv.toMultiplicative_symm_apply_apply, OrderMonoidHom.fstₗ_apply, Filter.tendsto_prodAssoc, Matrix.mul_submatrix_one, WithSeminorms.congr_equiv, CategoryTheory.Iso.homToEquiv_apply, NumberField.Units.abs_det_eq_abs_det, UniformEquiv.piCongrLeft_toEquiv, unitsEquivNeZero_apply_coe, Topology.WithLower.ofLower_le_ofLower, infClosed_preimage_ofDual, continuous_toDual, CategoryTheory.Functor.curryingEquiv_apply_map, IsSimpleOrder.equivBool_symm_apply, MulRingNorm.mulRingNormEquivAbsoluteValue_apply, WithBot.lt_toDual_iff, Monotone.dual, Equiv.finsetSubtypeComm_symm_apply, CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift, FreeMonoid.mrange_lift, BoundedLatticeHom.dual_apply_toFun, Equiv.image_eq_preimage_symm, AddMonoidAlgebra.lift_unique', MulEquiv.toAdditive_symm_apply_apply, CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv, Equiv.sumProdDistrib_symm_apply_left, Antitone.dual_left, ZMod.lift_coe, RootPairing.Equiv.indexHom_apply, CategoryTheory.FunctorToTypes.functorHomEquiv_apply_app, uliftPowersHom_apply_apply, Topology.WithLawson.ofLawson_inj, CartanMatrix.A_two, AddChar.toMonoidHomEquiv_add, Algebra.discr_powerBasis_eq_prod, FreeAddMonoid.lift_eval_of, finSuccEquiv'_above, DirectSum.coe_decompose_mul_add_of_right_mem, measurable_equivCurry_symm, UniformFun.postcomp_uniformContinuous, MulEquiv.multiplicativeAdditive_symm_apply, Equiv.uniqueSigma_symm_apply, SymAlg.sym_mul_self, LieAlgebra.of_add, SetTheory.PGame.moveLeft_neg_toLeftMovesNeg, CategoryTheory.WithTerminal.widePullbackShapeEquiv_inverse_obj, UniformFun.edist_def, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, CategoryTheory.Sieve.overEquiv_symm_generate, FreeAddMonoid.mrange_lift, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_f, Sym.append_comm, CategoryTheory.Equivalence.induced_unitIso, AddMonoidAlgebra.ofMagma_apply, LinearMap.polyCharpolyAux_map_aeval, CartanMatrix.D_two, CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq, WithZero.le_ofAdd_iff, OrderIso.sumLexEmpty_apply_inl, sInfHom.dual_symm_apply_toFun, UniformFun.ofFun_neg, WithBot.toDualTopEquiv_symm_coe, ContinuousMap.piEquiv_apply, OrderIso.sumLexIicIoi_apply_inl, Nat.equivProdNatFactoredNumbers_apply, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, LE.le.ofDual, OrderIso.sumDualDistrib_inl, Matrix.blockTriangular_transpose_iff, Finset.Ici_toDual, Equiv.embeddingEquivOfFinite_symm_apply, CategoryTheory.GradedObject.comapEquiv_inverse, DomAddAct.isQuotientMap_mk_symm, OrderDual.toDual_top, Sum.Lex.lt_def, Equiv.pprodProd_symm_apply, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, isAddRightRegular_ofLex, SSet.stdSimplex.objEquiv_symm_comp, nsmulCoprime_symm_apply, finProdFinEquiv_symm_apply, Topology.lawsonClosed_of_scottClosed, Equiv.symmEquiv_symm_apply_apply, AddEquiv.addSubmonoidMap_symm_apply, MonoidAlgebra.liftMagma_symm_apply, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, AddMonoidAlgebra.liftMagma_symm_apply, WithBot.ofDual_bot, CategoryTheory.ShortComplex.Homotopy.equivSubZero_apply, Sym2.lift_smul_lift, Affine.Simplex.faceOppositeCentroid_reindex, SemidirectProduct.equivProd_apply, Equiv.piCongrFiberwise_apply, Equiv.permCongr_def, AlgEquiv.opComm_apply_symm_apply, IsTranscendenceBasis.comp_equiv, Subgroup.IsComplement.coe_equiv_fst_eq_one_iff_mem, CategoryTheory.Equivalence.induced_inverse_obj, MulEquiv.coe_prodAssoc_symm, Unitization.starLift_apply, Fin.succFunEquiv_apply, finSuccEquiv_eq_some, MvPolynomial.IsSymmetric.rename, CategoryTheory.Sheaf.ΓObjEquivHom_naturality, SimpleGraph.coe_recolorOfEquiv, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, CategoryTheory.HomOrthogonal.matrixDecomposition_apply, Delone.DeloneSet.mapIsometry_apply_packingRadius, CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm, ofMul_one, CategoryTheory.Functor.IsRepresentedBy.uliftYonedaIso_hom, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, CategoryTheory.Bicategory.conjugateIsoEquiv_apply_hom, OrderIso.invENNReal_apply, SetTheory.PGame.Domineering.shiftUp_symm_apply, DirectSum.decompose_zero, groupCohomology.cocyclesOfIsMulCocycle₁_coe, isBot_toDual_iff, CoxeterSystem.lengthParity_simple, small_iff, CategoryTheory.Limits.biproduct.whiskerEquiv_hom, RootPairing.equiv_of_mapsTo_apply, CategoryTheory.Bicategory.conjugateIsoEquiv_symm_apply_hom, SimpleGraph.Iso.boxProdSumDistrib_symm_apply, AddAction.toPermHom_apply_symm_apply, CategoryTheory.MonObj.ofRepresentableBy_mul, edist_ofAdd, CategoryTheory.Limits.Cofork.IsColimit.homIso_natural, Matrix.reindexLinearEquiv_apply, ofLex_inj, CategoryTheory.Limits.Concrete.productEquiv_apply_apply, CategoryTheory.Localization.homEquiv_refl, ContinuousMap.sigmaEquiv_apply, Order.PFilter.mem_mk, AddAut.conj_apply, ofLex_inv, Equiv.Set.Equiv.strictMono_setCongr, HomotopicalAlgebra.AttachCells.reindex_cofan₁, CategoryTheory.Localization.homEquiv_trans, NumberField.mixedEmbedding.logMap_unit_smul, UniformOnFun.lipschitzOnWith_iff, WithZero.logEquiv_apply, Set.BijOn.extendDomain, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', Matrix.compAlgEquiv_symm_apply, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, Additive.toMul_top, CategoryTheory.SingleObj.mapHom_comp, Equiv.prodCongrRight_apply_snd, CategoryTheory.Limits.limitCompYonedaIsoCocone_inv, Equiv.Perm.sign_permCongr, Equiv.Set.sumDiffSubset_apply_inr, CategoryTheory.SimplicialObject.cechNerveEquiv_symm_apply, SupPrime.dual, Equiv.embeddingCongr_apply, QuotientAddGroup.equivIocMod_symm_apply, dist_toMul, Matrix.isUnit_comp_iff, CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv_symm, IsometryEquiv.coe_eq_toEquiv, CategoryTheory.conjugateEquiv_comp_assoc, UniformOnFun.uniformContinuous_restrict, tangentMap_chart_symm, EquivFunctor.mapEquiv.injective, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, Equiv.polishSpace_induced, HahnEmbedding.Partial.coeff_eq_zero_of_mem, CategoryTheory.coyonedaEquiv_coyoneda_map, Diffeomorph.coe_toEquiv, isOfFinAddOrder_ofMul_iff, Matrix.uniqueRingEquiv_symm_apply, SubMulAction.ofFixingSubgroup.append_left, Set.Iic_ofDual, FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf, ofColex_vadd, Finmap.keysLookupEquiv_apply_coe_snd, finTwoArrowEquiv'_symm_apply, nhds_ofDual, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply, PartENat.withTopEquiv_le, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, Order.IsPredPrelimit.dual, CStarMatrix.reindexₗ_apply, CategoryTheory.Limits.coneOfSectionCompYoneda_π, AddAction.toPerm_symm_apply, toMul_nsmul, Sum.Lex.toLexRelIsoLT_coe, AlgEquiv.subalgebraMap_apply_coe, coe_ofLexAddEquiv, Finsupp.lcongr_symm_single, CategoryTheory.Iso.isoCongr_apply, Equiv.Perm.perm_symm_mapsTo_of_mapsTo, WithTop.toDual_le_toDual_iff, Equiv.prodCongrLeft_symm, Orientation.map_neg, CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv, Set.coe_unionEqSigmaOfDisjoint_symm_apply, UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm, Prefunctor.costar_conj_star, exteriorPower.alternatingMapToDual_apply_ιMulti, YoungDiagram.equivListRowLens_apply_coe, Equiv.surjective_comp, sigmaFinsuppEquivDFinsupp_single, Order.isSuccLimit_toDual_iff, CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc, InfTopHom.dual_apply_toFun, ContinuousAlternatingMap.ofSubsingleton_apply_apply, RingHom.liftOfRightInverse_comp, Equiv.ofPreimageEquiv_map, SetSemiring.up_le_up, QuasiconvexOn.dual, isAddRightRegular_ofColex, Monoid.PushoutI.NormalWord.summand_smul_def', CategoryTheory.forgetAdjToOver.homEquiv_symm, FinEnum.down_equiv_symm, DFinsupp.lex_le_iff_of_unique, Equiv.self_comp_symm, Set.Ioo_toDual, Finsupp.equivMapDomain_apply, uliftZMultiplesHom_apply_apply, ofDual_natCast, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, FreeAddMonoid.lift_restrict, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi, ArchimedeanClass.FiniteElement.val_one, PartENat.withTopEquiv_lt, RingEquiv.piCongrLeft_apply, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, IsAtom.dual, ofDual_intCast, CategoryTheory.OverPresheafAux.MakesOverArrow.app, ContinuousMap.piComparison_fac, AddSubsemigroup.equivOp_symm_apply_coe, OrderDual.exists, TensorAlgebra.range_lift, PartENat.withTopEquiv_apply, CoalgEquiv.coe_toEquiv, SymAlg.unsym_bijective, MonoidHom.coe_toAdditive_range, DirectSum.decomposeLinearEquiv_symm_apply, CategoryTheory.Bicategory.mateEquiv_square, Finset.Colex.le_def, Equiv.sumAssoc_symm_apply_inr_inl, FreeMonoid.ofList_singleton, Affine.Simplex.touchpoint_reindex, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, AddHom.mulOp_symm_apply_apply, WType.NatαEquivPUnitSumPUnit_apply, CategoryTheory.Discrete.equivalence_counitIso, AddAction.orbitEquivQuotientStabilizer_symm_apply, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, isAddLeftRegular_toDual, Preord.dual_map, AddMonoidAlgebra.lift_of', Equiv.withBotSubtypeNe_apply, CategoryTheory.OverPresheafAux.OverArrows.app_val, strictAnti_dual_iff, CategoryTheory.Functor.coconeTypesEquiv_apply_ι_app, Set.Iio_ofDual, Ideal.associatesEquivIsPrincipal_apply, LinearEquiv.symmEquiv_symm_apply_apply, equivShrink_lt_equivShrink, IsPGroup.powEquiv_symm_apply, IsometryEquiv.piCongrLeft_apply, WithCStarModule.norm_equiv_le_norm_prod, ContinuousMultilinearMap.iteratedFDerivComponent_apply, Matrix.diagonal_kronecker, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.Subfunctor.range_eq_ofSection, IsometryEquiv.coe_toEquiv, HahnSeries.leadingCoeff_nonneg_iff, CategoryTheory.orderDualEquivalence_counitIso, Metric.Snowflaking.toSnowflaking_comp_ofSnowflaking, OrderIso.sumDualDistrib_symm_inr, EquivLike.apply_coe_symm_apply, Equiv.inv_apply, equivShrink_add, FreeAbelianGroup.mul_def, Matrix.updateCol_submatrix_equiv, Hamming.norm_eq_hammingNorm, Equiv.ulift_symm_down, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux, Finset.Icc_ofDual, Set.ordConnected_dual, Pi.toLex_apply, MulEquiv.toEquiv_injective, CFilter.ofEquiv_val, Setoid.piQuotientEquiv_symm_apply, RingEquiv.op_symm_apply_symm_apply, Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe, infPrime_toDual, FreeAlgebra.lift_unique, DomAddAct.mk_nsmul, Equiv.Perm.perm_inv_on_of_perm_on_finset, AlgEquiv.toRingEquiv_op, CategoryTheory.ShiftedHom.opEquiv_symm_apply_comp, CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit, BotHom.dual_symm_apply_apply, DirectSum.decomposeAlgEquiv_apply, Equiv.funSplitAt_apply, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, finSuccEquiv'_last_apply, OrderHom.equivFunctor_apply, AddMonoidAlgebra.grade.decompose_single, SetSemiring.down_add, NumberField.mixedEmbedding.indexEquiv_apply_isReal, MonoidHom.toAdditive_id, isLeftRegular_ofAdd, Equiv.curry_apply, Quiver.starEquivCostar_symm_apply, Equiv.prodPiEquivSumPi_symm_apply, MulEquiv.symmEquiv_symm_apply_apply, Equiv.ofUnique_apply, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply, CategoryTheory.Limits.Bicone.whisker_ι, Ordinal.type_lift_preimage, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, ContinuousMultilinearMap.nnnorm_ofSubsingleton, UniformOnFun.edist_eq_pi_restrict, Metric.Snowflaking.preimage_toSnowflaking_ball, AddMonoidHom.toMultiplicative_apply_apply, Equiv.emptySum_symm_apply, AddOpposite.opEquiv_symm_apply, CategoryTheory.orderDualEquivalence_functor_obj, MulEquiv.toMultiplicative_toAdditive_apply, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, CategoryTheory.isoOpEquiv_symm_apply, Fin.revOrderIso_symm_apply, CategoryTheory.unit_mateEquiv, CategoryTheory.conjugateEquiv_associator_hom, Equiv.subtypePreimage_symm_apply_coe_pos, CategoryTheory.Bicategory.conjugateEquiv_apply', Set.coe_snd_biUnionEqSigmaOfDisjoint, WithTop.le_ofDual_iff, Finset.Iio_toDual, Function.fromTypes_succ_equiv_apply, Equiv.prodCongrLeft_apply, uniformEquicontinuousOn_iff_uniformContinuousOn, isUpperSet_preimage_ofDual_iff, LieAlgebra.LieEquiv.ofCoboundary_invFun, Metric.Snowflaking.edist_toSnowflaking_toSnowflaking, CategoryTheory.Functor.RepresentableBy.ext_iff, CategoryTheory.Bicategory.mateEquiv_conjugateEquiv_vcomp, AddMonoidHom.fiberEquiv_apply, Matrix.piEquiv_symm_apply, toDual_neg, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, UniformOnFun.edist_def, Equiv.coinduced_symm, HahnSeries.iterateEquiv_apply, Rep.coindResAdjunction_homEquiv_symm_apply, Finset.UV.toColex_compress_lt_toColex, continuous_ofMul, SetSemiring.down_ssubset_down, toColex_mul, Monoid.CoprodI.Word.equivPair_head_smul_equivPair_tail, LocallyConstant.congrLeft_symm_apply, CategoryTheory.Adjunction.homAddEquiv_zero, Equiv.smulRight_symm_apply, monotoneOn_toDual_comp_iff, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, DirectSum.decompose_of_mem_ne, Equiv.coe_refl, WithBot.le_ofDual_iff, toAdd_prod, Pi.lt_toLex_update_self_iff, SupBotHom.symm_dual_id, Subgroup.equivOp_apply_coe, FirstOrder.Language.BoundedFormula.mapTermRelEquiv_apply, Finset.ofDual_min', ofBoolRing_inj, Equiv.ext_iff, CategoryTheory.Localization.SmallShiftedHom.postcompEquiv_symm_apply, finSumFinEquiv_symm_apply_castSucc, NonUnitalRingHom.op_apply_apply, CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false, CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right, ContinuousMap.val_addUnitsLift_symm_apply_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, MulAction.orbitZPowersEquiv_symm_apply', hahnEmbedding_isOrderedModule_rat, Finsupp.lcongr_single, Affine.Simplex.reindex_points, CategoryTheory.typeEquiv_counitIso_hom_app_val_app, FreeRing.lift_of, Sym.equivCongr_symm_apply, Submodule.IsHomogeneous.mem_iff, FreeMagma.lift_symm_apply, SheafOfModules.unitHomEquiv_comp_apply, CategoryTheory.CategoryOfElements.toCostructuredArrow_obj, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_f, SimpleGraph.Iso.boxProdSumDistrib_apply, WithBot.orderIsoPUnitSumLex_toLex, lipschitzOnWith_cfcₙ_fun_of_subset, OrderDual.forall, CategoryTheory.Presheaf.uliftYonedaAdjunction_unit_app_app, StrictAnti.dual, Matrix.det_reindex_self, CategoryTheory.ShiftedHom.opEquiv'_symm_add, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, Equiv.coe_inj, MeasureTheory.LevyProkhorov.toMeasureEquiv_apply, CategoryTheory.Bicategory.conjugateEquiv_adjunction_id, ofBoolRing_mul, AddMonoidHom.fiberEquivKer_symm_apply, Matrix.IsTotallyUnimodular.reindex, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, CliffordAlgebra.even.lift_symm_apply_bilin, Magma.AssocQuotient.lift_comp_of, t1Space_iff_continuous_cofinite_of, AlgEquiv.coe_toEquiv, IsLUB.dual, Monoid.CoprodI.Word.equivPair_smul_same, Equiv.ofRightInverseOfCardLE_symm_apply, isOpenMap_ofMul, UniformFun.lipschitzWith_iff, SSet.stdSimplex.yonedaEquiv_map, CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_apply, DomAddAct.mk_vadd_toLp, Equiv.summable_iff, UniformOnFun.ofFun_prod, Finmap.keysLookupEquiv_symm_apply_keys, Additive.ofMul_eq_bot, sigmaAntidiagonalEquivProd_symm_apply_fst, Equiv.optionEquivSumPUnit_symm_inl, Set.InvOn.extendDomain, CategoryTheory.CatEnrichedOrdinary.homEquiv_comp, Matrix.mul_empty, SetTheory.PGame.add_moveRight_inl, Set.powersetCard.mem_ofFinEmbEquiv_iff_mem_range, MonoidAlgebra.lift_apply, CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app, Algebra.Generators.reindex_val, CategoryTheory.Localization.SmallShiftedHom.precompEquiv_symm_apply, Finset.Iic_ofDual, Hamming.ofHamming_inj, MonomialOrder.degLex_lt_iff, Bundle.TotalSpace.toProd_symm_apply_snd, CategoryTheory.CommSq.left_adjoint, Matrix.adjugate_submatrix_equiv_self, Equiv.Set.insert_symm_apply_inl, ChainComplex.toSingle₀Equiv_symm_apply_f_zero, MonoidAlgebra.lift_mapRangeRingHom_algebraMap, DFinsupp.equivProdDFinsupp_symm_apply, SymAlg.unsym_surjective, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', finSuccEquivLast_last, HahnModule.orderTop_vAdd_le_orderTop_smul, CategoryTheory.Limits.limitCompCoyonedaIsoCone_inv, CategoryTheory.ShiftedHom.opEquiv'_zero_add_symm, finCongr_symm_apply, SetTheory.PGame.add_moveLeft_inr, ofLex_ofNat, FreeAddGroup.range_lift_le, AddEquiv.addMonoidHomCongrRightEquiv_apply, Finset.toDual_sup, CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, Cubic.equiv_symm_apply_c, Equiv.embeddingFinSucc_fst, MonoidAlgebra.uniqueRingEquiv_symm_apply, CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq, RootPairing.rootSpanMem_reflectionPerm_self, QuaternionAlgebra.coe_symm_addEquivProd, AlgEquiv.coe_mk, PiTensorProduct.map_comp_reindex_symm, UniformEquiv.piCongr_toEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, ContinuousMultilinearMap.ofSubsingleton_apply_toMultilinearMap, CategoryTheory.Iso.eHomCongr_comp, ofBoolAlg_top, Filter.prod_assoc, MonoidHom.ext_mint_iff, UniformFun.mem_gen, RootPairing.pairingIn_reflectionPerm, CategoryTheory.PreGaloisCategory.endEquivAutGalois_mul, Fin.cycleRange_symm_succ, Equiv.image_symm_image, Additive.forall, Equiv.Set.rangeInl_apply_inl, Equiv.piCongrLeft_apply_eq_cast, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, Prefunctor.symmetrifyStar, Equiv.Set.rangeInr_symm_apply_coe, CategoryTheory.Oplax.StrongTrans.Modification.equivOplax_apply, Equiv.Set.congr_apply, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj, Pi.toColex_strictMono, CategoryTheory.Functor.representableByUliftFunctorEquiv_apply_homEquiv, WType.equivSigma_symm_apply, BddAbove.dual, CategoryTheory.ShiftedHom.homEquiv_apply, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, Topology.WithScott.ofScott_toScott, UniformOnFun.toFun_sum, LightCondensed.ihomPoints_symm_apply, List.SortedGE.of_map_ofDual, ofColex_pow, finSuccEquiv_eq_none, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_apply_coe, Complex.lift_symm_apply_coe, CategoryTheory.Functor.CorepresentableBy.equivUliftCoyonedaIso_apply, Matrix.piAlgEquiv_symm_apply, FreeAlgebra.lift_symm_apply, UniformOnFun.uniformContinuous_restrict_toFun, UniformOnFun.precomp_uniformContinuous, Orientation.oangle_map, Equiv.Perm.decomposeFin_symm_of_one, DomMulAct.smul_apply, CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_apply_app, Quiver.SingleObj.toPrefunctor_apply_obj, ContinuousAlgHom.prodEquiv_apply, LinearEquiv.symmEquiv_apply_symm_apply, ContinuousMap.equivFnOfDiscrete_symm_apply_apply, Finset.Colex.lt_iff_max'_mem, Primrec.of_equiv_symm, CategoryTheory.Limits.Sigma.ι_reindex_hom, AddCircle.liftIoc_eq_lift_Icc, MeasurableEquiv.coe_sumPiEquivProdPi_symm, Int.toAdd_zpow, ZSpan.quotientEquiv.symm_apply, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, Magma.AssocQuotient.lift_of, AlgCat.free_map, Submodule.torsion_gc, CategoryTheory.uliftCoyonedaEquiv_naturality, isAddRegular_ofMul, finProdFinEquiv_apply_val, AddMonoid.Coprod.lift_apply_mk, FreeMonoid.hom_map_lift, Equiv.arrowProdEquivProdArrow_symm_apply, CategoryTheory.Limits.IsLimit.homEquiv_symm_π_app_assoc, WittVector.liftEquiv_symm_apply_coe, CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff, Equiv.sumSigmaDistrib_apply, Matrix.of_mem_specialOrthogonalGroup_fin_two_iff, nsmulCoprime_zero, Quaternion.imJ_equivProd_symm_apply, UniformFun.toFun_neg, IsometryEquiv.toEquiv_injective, IsCompl.ofDual, ofBoolRing_neg, ContinuousMap.isUniformEmbedding_uniformFunOfFun, Equiv.piOptionEquivProd_apply, Finsupp.coe_equivFunOnFinite_symm, TopHom.symm_dual_comp, InverseSystem.piLTLim_symm_apply, Equiv.prodPUnit_symm_apply, fixingSubmonoid_fixedPoints_gc, FreeAddGroup.lift_symm_apply, InverseSystem.piSplitLE_lt, LocallyConstant.congrRightRingEquiv_symm_apply_apply, ContinuousAffineEquiv.coe_symm_toEquiv, SSet.stdSimplex.objEquiv_toOrderHom_apply, CategoryTheory.Localization.SmallHom.equiv_comp, Equiv.piCongrFiberwise_symm_apply, Equiv.toFun_inducedStructureEquiv, WithTop.toDualBotEquiv_symm_coe, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left, AddMonoidAlgebra.uniqueRingEquiv_symm_apply, Equiv.prodUnique_apply, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply, MonoidHom.eq_liftOfRightInverse, toLex_smul', Prod.Lex.toLex_mono, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.nerve.σ_zero_nerveEquiv_symm, AlgEquiv.toAlgHom_unop, Equiv.setValue_eq, CategoryTheory.Functor.homEquivOfIsRightKanExtension_symm_apply, OrderIso.emptySumLex_apply_inr, DomAddAct.isEmbedding_mk, OnePoint.smul_infty_def, Cardinal.eq, Set.piCongrLeft_comp_restrict, DirectSum.SetLike.IsHomogeneous.mem_iff, Sum.Lex.inl_lt_inr, Topology.WithLower.toLower_le_toLower, OrthonormalBasis.equiv_apply_basis, OrderDual.lt_toDual, Finsupp.mapDomain_equiv_apply, Module.Basis.map_orientation_eq_det_inv_smul, Function.Embedding.optionEmbeddingEquiv_symm_apply, Affine.Simplex.eulerPoint_reindex, CommAlgCat.isoEquivAlgEquiv_symm_apply, BoundedOrderHom.dual_symm_apply_toOrderHom, isAddRegular_ofDual, ofDual_wcovBy_ofDual_iff, ofDual_toAdd_eq_top_iff, CategoryTheory.Adjunction.equivHomsetRightOfNatIso_apply, ContinuousLinearEquiv.arrowCongrEquiv_symm_apply, Equiv.subtypeQuotientEquivQuotientSubtype_symm_mk, StrictAnti.dual_right, AddCircle.equivIoc_coe_eq, infIrred_toDual, Set.up_one, DomMulAct.stabilizerMulEquiv_apply, Set.Ioi_toDual, prodEquivPiFinTwo_symm_apply, CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_symm_apply, isOpenMap_ofDual, Matrix.comp_map_map, Multiset.mapEquiv_apply, AlternatingMap.ofSubsingleton_symm_apply_apply, Similar.index_equiv, PiLp.basis_toMatrix_basisFun_mul, finEquivZPowers_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, AddMagma.FreeAddSemigroup.lift_of, Topology.WithLawson.isClosed_preimage_ofLawson, FinEnum.up_equiv_symm, Equiv.coe_embeddingFinSucc_symm, Matrix.tail_transpose, CategoryTheory.equivYoneda_inv_app, CategoryTheory.uliftCoyonedaEquiv_symm_map_assoc, Finsupp.linearCombination_equivMapDomain, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, PartENat.withTopEquiv_symm_zero, List.sortedGT_map_toDual, AddEquiv.toMultiplicative_symm_apply_symm_apply, SetTheory.PGame.toLeftMovesNim_symm_lt, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, MultilinearMap.ofSubsingleton_symm_apply_apply, CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj, FreeSemigroup.lift_comp_of', AlgebraicGeometry.Spec.homEquiv_apply, StrictMono.dual, Equiv.symm_bijective, Equiv.piCongrRight_apply, Matrix.row_eq_self, CategoryTheory.Adjunction.homAddEquiv_symm_apply, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, AlgHom.toRingHom_unop, MulArchimedeanOrder.of_val, MonoidHom.coe_toAdditive, Function.OfArity.uncurry_two_eq_uncurry, Subsemigroup.coe_toAddSubsemigroup_symm_apply, CompactlyGenerated.isoEquivHomeo_symm_apply, tangentBundleModelSpaceHomeomorph_coe_symm, CategoryTheory.Limits.biproduct.whiskerEquiv_inv_eq_lift, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, DomMulAct.mk_inv, WithZero.toMulBot_coe, Matrix.submatrixEquivInvertibleEquivInvertible_apply, Finset.sum_map_equiv, DomMulAct.isInducing_mk, WithCStarModule.equiv_pi_apply, finEquivMultiples_apply, Equiv.sumCompl_apply_symm_of_pos, CategoryTheory.Limits.Trident.IsLimit.homIso_symm_apply, WithZero.lift'_surjective, LieAlgebra.of_symm_nsmul, Finsupp.Lex.single_antitone, CategoryTheory.codiscreteEquiv_symm_apply_as, Equiv.prodCongrRight_apply_fst, IsometryEquiv.piCongrLeft'_symm_apply, finSuccEquiv'_symm_none, Equiv.Set.sumDiffSubset_symm_apply_of_mem, Quiver.starEquivCostar_apply, ContinuousMap.equivFnOfDiscrete_symm_apply, Matrix.det_mul_column, SetSemiring.down_subset_down, Equiv.natSumNatEquivNat_apply, CategoryTheory.Groupoid.invEquiv_symm_apply, DirectSum.decompose_symm_mul, Additive.ofMul_lt, coe_notMemRangeEquiv, FreeGroupBasis.lift_symm_apply, Finsupp.lex_le_iff_of_unique, Equiv.sumSumSumComm_apply, eVariationOn.comp_ofDual, FreeMonoid.lift_symm_apply, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_apply, Monoid.Coprod.inv_def, CategoryTheory.Functor.CorepresentableBy.homEquiv_comp, ofAdd_sub, Topology.WithLowerSet.isOpen_ofLowerSet_preimage, LatticeHom.dual_comp, CategoryTheory.Adjunction.homAddEquiv_symm_add, antitoneOn_dual_iff, Functor.mapEquiv_symm_apply, CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_f, MulEquiv.symmEquiv_symm_apply_symm_apply, finSuccAboveEquiv_symm_apply_last, CategoryTheory.LocalizerMorphism.equiv_smallHomMap, SetTheory.PGame.moveRight_neg_toRightMovesNeg, toMul_smul, CategoryTheory.conjugateEquiv_symm_comm, OrderIso.equivClosureOperator_symm_apply, AddMonoidHom.coe_toMultiplicative_map, OrderIso.sumLexDualAntidistrib_symm_inl, infIrred_ofDual, Submonoid.powLogEquiv_apply, Orientation.kahler_map, CategoryTheory.Functor.CorepresentableBy.uniqueUpToIso_hom, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, Matrix.reindex_refl_refl, CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left_assoc, CoxeterMatrix.reindex_apply, ofLex_smul', Equiv.subRight_apply, Quiver.SingleObj.toHom_symm_apply, AddEquiv.additiveMultiplicative_symm_apply, Equiv.piCongrLeft_sumInr, Affine.Simplex.signedInfDist_reindex, Equiv.piCongr'_apply, Equiv.Set.image_symm_apply, Filter.prod_assoc_symm, isRightRegular_ofDual, WithTop.ofDual_le_iff, AddSubmonoid.coe_toSubmonoid_symm_apply, Matrix.diagonalInvertibleEquivInvertible_symm_apply, CategoryTheory.CountableCategory.instCountableHomObjAsType, contMDiff_equivTangentBundleProd, toBoolAlg_inj, nnnorm_ofMul, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, Equiv.boolProdEquivSum_symm_apply, CategoryTheory.Bicategory.conjugateEquiv_associator_hom, ZMod.lift_injective, SemilatInfCat.dual_map, AddValuation.toValuation_apply, DomMulAct.smul_Lp_ae_eq, AddEquiv.toEquiv_injective, CategoryTheory.Limits.Sigma.ι_reindex_inv, zmultiplesHom_apply, CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down_assoc, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_obj, Equiv.coe_prodUnique, RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe, finprod_comp_equiv, DirectSum.equivCongrLeft_apply, CategoryTheory.Functor.curryingFlipEquiv_apply_map, Shrink.continuousLinearEquiv_symm_apply, AddCircle.continuous_equivIco_symm, Fin.insertNth_comp_cycleRange_symm, linearIndepOn_equiv, SetTheory.PGame.exists_rightMoves_neg, FreeAbelianGroup.liftMonoid_coe, FreeMagma.lift_comp_of, Subgroup.toAddSubgroup_comap, CategoryTheory.conjugateEquiv_id, Topology.WithGeneratedByTopology.isOpen_iff, Equiv.prodAssoc_symm_apply, Set.OrdConnected.dual, Metric.Snowflaking.uniformEquiv_symm_apply, DomAddAct.coe_mkHomeomorph_symm, Equiv.subtypeUnivEquiv_symm_apply, Equiv.arrowCongr_comp, CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv, isRightRegular_ofColex, uniformity_multiplicative, Equiv.Perm.prod_comp', Abelianization.lift_of, DomAddAct.mk_neg, OrderIso.asBoolAlgAsBoolRing_apply, ofMul_mul, equivShrink_symm_add, SSet.stdSimplex.ofSimplex_yonedaEquiv_δ, AddCircle.continuousAt_equivIoc, OrderDual.instNeBotNhdsWithinIoi, List.sortedLT_map_toDual, CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl, Equiv.psigmaEquivSigmaPLift_apply, Pi.toColex_update_le_self_iff, Matrix.one_fin_three, WithCStarModule.equiv_sub, CompactlySupportedContinuousMap.continuousMapEquiv_symm_apply, Equiv.finsetSubtypeComm_apply_coe, Equiv.setOf_apply_symm_eq_image_setOf, AddEquiv.finsuppUnique_symm_apply_support_val, Matrix.toLin_finTwoProd_toContinuousLinearMap, LightCondensed.ihom_map_val_app, WithCStarModule.equiv_snd, SetTheory.PGame.moveLeft_toLeftMovesNim, Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply, CategoryTheory.Iso.toEquiv_symm_fun, UniformOnFun.uniformContinuous_eval_of_mem_sUnion, Hamming.ofHamming_toHamming, Equiv.divLeft₀_apply, Equiv.sigmaProdDistrib_symm_apply, Shrink.rec_equivShrink, DomAddAct.map_mk_nhds, Continuous.matrix_reindex, Matrix.toSquareBlockProp_def, CategoryTheory.Adjunction.homAddEquiv_neg, Matrix.of_symm_single, CategoryTheory.Bicategory.conjugateEquiv_id, Orientation.areaForm_map, CategoryTheory.Adjunction.homEquiv_symm_id, Equiv.Perm.VectorsProdEqOne.vectorEquiv_symm_apply, FreeAddMonoid.map_symm_apply_map_eq, Equiv.piCongr_symm_apply, pow_ofLex, Equiv.symmEquiv_apply_symm_apply, supClosed_preimage_toDual, Matrix.reindex_mem_rowStochastic, Matrix.single_eq_of_single_single, OrderDual.toDual_eq_top, Matrix.matrixOfPolynomials_blockTriangular, AddChar.toAddMonoidHom_apply, SSet.S.equivElements_apply_snd, CategoryTheory.ShiftedHom.opEquiv'_symm_comp, Set.MapsTo.extendDomain, Equiv.inducedStructure_RelMap, ContinuousMultilinearMap.ofSubsingleton_apply_apply, nnnorm_ofDual, ofBoolAlg_toBoolAlg, TopologicalSpace.gc_generateFrom, Matrix.uniqueAlgEquiv_symm_apply, Matrix.of_col, TopHom.dual_apply_apply, Topology.WithUpperSet.ofUpperSet_inj, Specialization.isUpperSet_ofEquiv_preimage, CategoryTheory.Adjunction.homEquiv_naturality_left_square_iff, Function.Embedding.toEquivRange_symm_apply_self, WithCStarModule.norm_equiv_le_norm_pi, Ideal.associatesEquivIsPrincipal_mul, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm, OrderDual.le_toDual, DomMulAct.mk_mul, UniformEquiv.uniformEquiv_mk_coe, ofLex_vadd', ofAdd_zsmul, RingEquiv.piCongrLeft'_symm_apply, Tuple.eq_sort_iff', UniformOnFun.toFun_sub, WithBot.toDual_lt_iff, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, Nat.card_image_equiv, Equiv.eq_image_iff_symm_image_eq, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Perfection.lift_apply_apply_coe, Equiv.coe_fn_mk, InfTopHom.dual_symm_apply_toFun, Cardinal.extend_function, OrderIso.sumLexIioIci_symm_apply_of_ge, Equiv.permCongr_eq_mul, Equiv.ofPreimageEquiv_apply, Multiplicative.toAdd_bot, ofLex_smul, Matroid.mapEquiv_indep_iff, Ordinal.toPGame_moveLeft, OrderMonoidIso.coe_toEquiv_symm, CategoryTheory.FinCategory.objAsTypeToAsType_obj, CategoryTheory.Bicategory.conjugateEquiv_symm_iso, OrderDual.toDual_lt, HahnSeries.lt_iff, CategoryTheory.WithTerminal.isLimitEquiv_apply_lift_left, finSuccEquivLast_symm_none, Fin2.equivFin_apply, Multiplicative.toAdd_le, AddAction.stabilizerEquivStabilizer_apply, OrderHom.symm_dual_comp, ContinuousLinearEquiv.arrowCongrEquiv_apply, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, OnePoint.not_continuous_cofiniteTopology_of_symm, ArchimedeanOrder.lt_def, ContinuousAlternatingMap.norm_ofSubsingleton_id, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_two_symm, IsExtrFilter.dual, Finset.Colex.toColex_lt_toColex_of_ssubset, CategoryTheory.FreeGroupoid.functorEquiv_symm_apply, SetRel.gc_leftDual_rightDual, Equiv.restrictPreimageFinset_apply_coe, Multiplicative.toAdd_strictMono, Matrix.inv_submatrix_equiv, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, CategoryTheory.mateEquiv_vcomp, Rep.invariantsAdjunction_homEquiv_apply_hom, Traversable.Free.map_eq_map, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le, CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquiv, Algebra.GrothendieckAddGroup.lift_apply, Equiv.eq_conj, Equiv.sumCompl_symm_apply_neg, List.SortedLE.of_map_toDual, Matrix.toLin'_submatrix, Equiv.functionSwap_apply, MulEquiv.toAdditive_symm_apply_symm_apply, Multiset.cast_symm_apply_snd, OrderDual.toDual_comp_ofDual, orderIsoShrink_apply, finSumNatEquiv_symm_apply_add_right, finPiFinEquiv_single, CategoryTheory.yonedaEquiv_naturality, CategoryTheory.Adjunction.homEquiv_apply, Metric.Snowflaking.image_toSnowflaking_closedBall, BotHom.symm_dual_id, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, Prod.Lex.toLex_covBy_toLex_iff, ofDual_sup, Equiv.continuous_symm_iff, HahnModule.of_smul, Matrix.reindex_mem_colStochastic, ContinuousMap.equivBoundedOfCompact_symm_apply, CompactlyGenerated.isoEquivHomeo_apply, Matrix.diagonalInvertibleEquivInvertible_apply, AddSubgroup.coe_toSubgroup_apply, edist_ofMul, AntivaryOn.dual_left, RingEquiv.op_symm_apply_apply, OrderIso.inv_apply, PartENat.withTopEquiv_zero, Equiv.subLeft_apply, sInfHom.symm_dual_comp, AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackId_hom, WithBot.toDual_le_toDual_iff, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply, MulHom.op_apply_apply, ChainComplex.fromSingle₀Equiv_apply, AddEquiv.toAdditive_toMultiplicative_apply, CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply, FirstOrder.Language.Term.relabelEquiv_symm_apply, IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe, Colex.exists, DirectSum.liftRingHom_symm_apply_coe, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, ofDual_sub, Equiv.setCongr_apply, DomAddAct.coe_mkHomeomorph, Set.preimage_equiv_eq_image_symm, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_map, TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply, AlgHom.toRingHom_op, ofColex_eq_one, Finset.Colex.toColex_image_ofColex_strictMono, Module.Basis.toMatrix_reindex, LieAlgebra.of_symm_zero, AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply, Finite.exists_equiv_fin, Equiv.sumArrowEquivProdArrow_apply_fst, finSuccEquiv'_symm_coe_below, Matrix.empty_mul, SymAlg.unsym_eq_one_iff, AddChar.toMonoidHomEquiv_symm_mul, RootPairing.coroot'_reflection, algebraicIndependent_equiv, UniformFun.toFun_add, Metric.Snowflaking.image_ofSnowflaking_emetricClosedBall, MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto, DomAddAct.mk_vadd_mk_aeeqFun, CategoryTheory.Bicategory.mateEquiv_leftUnitor_hom_rightUnitor_inv, fixingAddSubgroup_fixedPoints_gc, Equiv.Set.insert_apply_right, Finset.Ico_orderDual_def, Prefunctor.symmetrifyCostar, Equiv.sigmaSigmaSubtypeEq_symm_apply, CategoryTheory.Bicategory.conjugateEquiv_mateEquiv_vcomp, Finsupp.restrictSupportEquiv_symm_single, Matrix.trace_fin_three_of, monovary_toDual_left, Cardinal.mk_equiv_comm, Equiv.bijOn_symm, finSuccAboveEquiv_apply, CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_symm_apply, RelIso.sumLexComplLeft_apply, Metric.Snowflaking.edist_ofSnowflaking_ofSnowflaking, toWellOrderExtension_strictMono, AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackComp_inv, MulEquiv.toAdditive_apply_symm_apply, sSupHom.symm_dual_comp, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality, Equiv.boolProdNatEquivNat_symm_apply, DFinsupp.toColex_monotone, SimpleGraph.Iso.mapNeighborSet_symm_apply_coe, CategoryTheory.Iso.homCongr_symm_apply, OrderIso.compl_apply, WithTop.ofDual_lt_iff, CategoryTheory.ComposableArrows.arrowEquiv_apply, Equiv.prod_assoc_preimage, finsuppEquivDFinsupp_symm_apply, Metric.Snowflaking.preimage_ofSnowflaking_eball, Matrix.invertibleEquivDetInvertible_apply, IsometryEquiv.coe_symm_toEquiv, Equiv.coe_piCongr_symm, Matrix.reindexAlgEquiv_apply, Hamming.toHamming_zero, AddEquiv.coe_toEquiv, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, CategoryTheory.Functor.partialRightAdjointHomEquiv_symm_comp_assoc, Equiv.coe_optionSubtype_apply_apply, polarCoord_apply, Equiv.prod_assoc_symm_image, TrivSqZeroExt.liftEquivOfComm_symm_apply_coe, WithCStarModule.inner_single_left, SSet.nonDegenerateEquivOfIso_apply_coe, SSet.S.le_iff_nonempty_hom, MeasurableEquiv.coe_toEquiv_symm, ContinuousMultilinearMap.domDomCongrEquiv_apply, AddCircle.continuousAt_equivIco, PartENat.withTopEquiv_symm_le, Finpartition.IsEquipartition.exists_partsEquiv, AddConstEquiv.coe_toEquiv, Matrix.det_matrixOfPolynomials, Metric.Snowflaking.uniformContinuous_toSnowflaking, finSuccEquiv'_succAbove, ofColex_sub, Set.uIoo_ofDual, RingEquiv.sumArrowEquivProdArrow_apply, Matrix.of_row, PowerBasis.liftEquiv'_apply_coe, DFA.accepts_reindex, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right, Cubic.equiv_apply_coe, HNNExtension.NormalWord.unitsSMulEquiv_symm_apply, Polynomial.toMatrix_sylvesterMap, CategoryTheory.MonoidalClosed.curryHomEquiv'_symm_apply, isAddLeftRegular_ofMul, GradedAlgebra.proj_apply, CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app, toDual_bihimp, CategoryTheory.map_yonedaEquiv, coe_toLexMulEquiv, Shrink.continuousLinearEquiv_apply, Metric.Snowflaking.image_toSnowflaking_closedEBall, CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux_symm_apply, Matrix.of_symm_apply, CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight, Finsupp.lex_lt_iff, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, List.sortedGE_map_toDual, CategoryTheory.eHomEquiv_comp, Matrix.dualNumberEquiv_apply, MonoidHom.ext_mnat_iff, OrderIso.subLeft_symm_apply, toAdd_div, OrderAddMonoidHom.fstₗ_apply, AlgEquiv.opComm_symm_apply_apply, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber, CategoryTheory.Functor.partialLeftAdjointHomEquiv_symm_comp_assoc, AddSubgroup.quotientEquivProdOfLE'_apply, UniformOnFun.isClosed_setOf_continuous, Finset.symInsertEquiv_apply_snd_coe, bddAbove_preimage_ofDual, Matrix.toLin_finTwoProd, toMul_eq_one, SheafOfModules.pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, norm_toDual, Equiv.Set.sumCompl_apply_inr, orderIsoShrink_symm_apply, BialgEquiv.coe_symm_toEquiv, CategoryTheory.Functor.FullyFaithful.isoEquiv_symm_apply, isAddRegular_ofLex, Equiv.mulRight₀_symm_apply, CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app, CategoryTheory.conjugateIsoEquiv_apply_hom, ofDual_symmDiff, Topology.WithLower.ofLower_inj, Prod.Lex.toLex_strictMono, DomMulAct.mk_pow, Algebra.adjoin_eq_range_freeAlgebra_lift, Fin.equiv_iff_eq, ContinuousMultilinearMap.piEquiv_symm_apply, StarAlgHom.prodEquiv_symm_apply, PartialEquiv.transEquiv_apply, isAddRegular_toColex, Function.Embedding.antisymm, FreeAddMagma.lift_symm_apply, ofDual_inv, AddCircle.openPartialHomeomorphCoe_symm_apply, continuousOn_cfcₙ_setProd, isMaxFilter_dual_iff, CategoryTheory.Localization.structuredArrowEquiv_symm_apply, QuaternionAlgebra.coe_linearEquivTuple, HahnModule.of_sub, Nat.factorizationEquiv_inv_apply, Topology.WithLower.isOpen_preimage_ofLower, Matrix.mul_fin_two, FreeLieAlgebra.lift_symm_apply, AlgEquiv.opComm_symm_apply_symm_apply, AddEquiv.symmEquiv_apply_apply, CategoryTheory.Limits.Sigma.whiskerEquiv_inv, WithZero.lift_unique, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, derivationToSquareZeroEquivLift_apply_coe_apply, FirstOrder.Language.LEquiv.onTerm_apply, CategoryTheory.CommSq.instHasLift_1, DirectSum.decomposeAddEquiv_symm_apply, DomAddAct.symm_mk_nsmul, ExteriorAlgebra.lift_unique, Monoid.CoprodI.lift_symm_apply, ContinuousLinearMap.prodEquiv_apply, Equiv.sumAssoc_symm_apply_inr_inr, ofMul_prod, toMul_multiset_sum, Topology.WithGeneratedByTopology.continuous_equiv, HahnModule.of_add, CategoryTheory.Sieve.overEquiv_symm_top, Topology.WithUpperSet.toUpperSet_ofUpperSet, Rep.homEquiv_symm_apply_hom, FreeAddMonoid.comp_lift, GradedRing.projZeroRingHom_apply, CategoryTheory.conjugateIsoEquiv_apply_inv, DFA.eval_reindex, MulAutMultiplicative_apply_symm_apply, CStarMatrix.neg_of, CategoryTheory.Limits.Types.limitEquivSections_apply, isLeftRegular_toDual, Submonoid.coe_toAddSubmonoid_symm_apply, Sym.oneEquiv_apply, CategoryTheory.Subobject.leInfCone_π_app_none, fixingSubgroup_fixedPoints_gc, UniformFun.uniformContinuous_eval, Topology.WithLowerSet.ofLowerSet_le_ofLowerSet, CoxeterSystem.reindex_simple, Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe, Submonoid.coe_toAddSubmonoid_apply, Quiver.SingleObj.pathEquivList_symm_nil, Equiv.equivCongr_refl, Real.expMonoidHom_apply, Finset.Colex.singleton_le_singleton, BoundedLatticeHom.dual_comp, DFA.reindex_apply_step, sigmaFinsuppEquivDFinsupp_apply, antivaryOn_toDual_right, CategoryTheory.Iso.homToEquiv_symm_apply, AlgHom.prodEquiv_apply, CategoryTheory.unitCompPartialBijective_symm_natural, Topology.WithLower.toLower_ofLower, Subgroup.IsComplement.equiv_mul_right_of_mem, CategoryTheory.Functor.sectionsEquivHom_apply_app, ContinuousMultilinearMap.toUniformOnFun_toFun, Order.pred_toAdd, Finset.Colex.toColex_lt_toColex, Matrix.det_mul_row, NonemptyInterval.toLex_mono, Equiv.range_eq_univ, Equiv.dvd_apply, Finsupp.sumFinsuppEquivProdFinsupp_symm_inl, MonotoneOn.dual_right, CategoryTheory.Iso.homFromEquiv_apply, OrderDual.toDual_bot, isRegular_toDual, SymAlg.sym_inj, DirectSum.decompose_symm_zero, SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, Equiv.sumArrowEquivProdArrow_apply_snd, Complex.toMatrix_conjAe, LT.lt.dual, Additive.toMul_eq_bot, Equiv.preimage_image, FreeAddMonoid.ofList_flatten, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst, CategoryTheory.Localization.Construction.objEquiv_apply, measurable_piEquivPiSubtypeProd_symm, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, AddAction.toPermHom_apply_apply, Matrix.invOf_submatrix_equiv_eq, AffineBasis.reindex_apply, Multiset.coeEquiv_symm_apply_fst, Matrix.submatrix_mul_transpose_submatrix, Matrix.cons_vecMul, Finset.Colex.toColex_image_le_toColex_image, Cardinal.out_lift_equiv, EquivLike.self_comp_coe_symm, Finset.Colex.toColex_sdiff_lt_toColex_sdiff', MonomialOrder.lex_lt_iff, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal, AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_apply_coe, subtypeOrEquiv_symm_inr, CategoryTheory.MonoidalClosed.homEquiv_apply_eq, Equiv.algebraMap_def, CategoryTheory.Limits.coneOfSectionCompCoyoneda_π, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, PresentedGroup.equivPresentedGroup_symm_apply_of, DirectSum.decomposeAddEquiv_apply, Topology.WithLower.toLower_lt_toLower, CategoryTheory.conjugateEquiv_whiskerLeft, Module.Ray.map_apply, Equiv.sigmaSumDistrib_apply, CochainComplex.fromSingle₀Equiv_symm_apply_f_zero, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, Finset.ofDual_inf', Module.Ray.map_neg, stdSimplexEquivIcc_apply_coe, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe, AlgEquiv.piCongrLeft_symm_apply, Unitization.lift_range_le, FreeAbelianGroup.lift_comp, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, Matrix.det_fin_one_of, Finsupp.restrictSupportEquiv_apply, FreeAddMonoid.lift_of_comp_eq_map, UpperHalfPlane.val_J, Equiv.piCongrLeft_apply_apply, CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down, measurable_piCurry_symm, Equiv.bijOn_image, Equiv.piCurry_apply, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, Subgroup.IsComplement.mk''_rightQuotientEquiv, WithCStarModule.equiv_symm_add, ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv_apply, finSigmaFinEquiv_one, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly, CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_apply, Matrix.vecMulVec_cons, ModularGroup.coe_T, IsLowerSet.toDual, Equiv.instCanLiftForallCoeBijective, DomAddAct.mk_zero, Equiv.equivPUnit_apply, Finsupp.curryEquiv_symm_apply, CategoryTheory.conjugateIsoEquiv_symm_apply_inv, Matrix.comp_symm_transpose, SSet.stdSimplex.spineId_vertex, Subgroup.transferFunction_apply, List.equivSigmaTuple_apply_snd, CategoryTheory.SimplicialObject.cechNerveEquiv_apply, rootsOfUnityEquivNthRoots_apply, List.sortedLE_map_ofDual, OrderHom.dual_apply_coe, Equiv.divLeft₀_symm_apply, CategoryTheory.Functor.LeibnizAdjunction.adj_unit_app_right, Fin.equivSubtype_symm_apply, Finset.Colex.toColex_empty, UniformFun.lipschitzOnWith_ofFun_iff, LinearAlgebra.FreeProduct.lift_algebraMap, Subgroup.quotientEquivProdOfLE'_apply, RelIso.preimage_apply, HahnModule.support_smul_subset_vadd_support, Matrix.cons_vecMul_cons, Equiv.boolProdEquivSum_apply, FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv, HahnSeries.orderTop_abs, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, LinearIsometryEquiv.piLpCongrLeft_single, DFA.evalFrom_reindex, Setoid.piQuotientEquiv_apply, Equiv.isTrivialRelation_comp, CategoryTheory.Adjunction.homEquiv_naturality_left_symm, CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π_assoc, OrderIso.sumLexIioIci_apply_inl, finSuccEquiv'_eq_none, SymAlg.unsym_mul_self, Equiv.sumComm_apply, Equiv.Perm.equivUnitsEnd_symm_apply_apply, Sum.Lex.inr_mono, Equiv.comp_symm_eq, Matrix.charpoly.univ_map_eval₂Hom, ContinuousMultilinearMap.nnnorm_ofSubsingleton_id, Matrix.det_fin_two_of, InfHom.symm_dual_id, CategoryTheory.Groupoid.isoEquivHom_symm_apply_inv, Equiv.piCongrLeft'_symm_apply, AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply, SheafOfModules.relationsOfIsCokernelFree_s, FreeAbelianGroup.lift_add_apply, WithTop.orderIsoSumLexPUnit_symm_inr, CategoryTheory.ShiftedHom.opEquiv_symm_apply, AddChar.toAddMonoidHomEquiv_zero, Specialization.ofEquiv_specializes_ofEquiv, StrictConvexOn.dual, CategoryTheory.Limits.Concrete.prodEquiv_apply_snd, Monoid.CoprodI.Word.equivPair_head, CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str, UniformConvergenceCLM.uniformSpace_eq, FirstOrder.Language.Theory.CompleteType.mem_typeOf, AddSubgroup.toSubgroup'_closure, Equiv.Finset.union_inr, Subgroup.IsComplement'.QuotientMulEquiv_symm_apply, Topology.WithUpper.isOpen_def, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left, Algebra.discr_powerBasis_eq_prod'', CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε, Matrix.diagonal_unique, CategoryTheory.Presheaf.freeYonedaHomEquiv_comp_assoc, FreeAddGroup.lift_eq_sum_map, AlgebraicGeometry.affineOpensRestrict_symm_apply_coe, CategoryTheory.Adjunction.homEquiv_counit, Matrix.ofNat_kronecker, Topology.WithLower.continuous_toLower, Finsupp.mapDomain.toLinearMap_linearEquiv, Affine.Simplex.mongePlane_reindex, AddCommMonCat.equivalence_counitIso, Orientation.reindex_apply, UniformOnFun.toFun_add, Hamming.dist_eq_hammingDist, SymAlg.sym_eq_zero_iff, Equiv.addLeft_symm_apply, OrderIso.sumDualDistrib_inr, CategoryTheory.ShiftedHom.opEquiv'_apply, SSet.S.equivElements_symm_apply_simplex, CochainComplex.toSingle₀Equiv_apply, TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply, grade_ofDual, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, CompleteLatticeHom.dual_apply_toFun, CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_apply, PiTensorProduct.map_reindex, IsExtrOn.dual, Finset.symInsertEquiv_apply_fst, CategoryTheory.isoOpEquiv_apply, uliftZPowersHom_apply_apply, CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, Equiv.optionSubtypeNe_some, Equiv.symmEquiv_symm_apply_symm_apply, WithCStarModule.equiv_fst, InverseSystem.globalEquiv_naturality, SSet.stdSimplex.mem_nonDegenerate_iff_mono, CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str, Metric.Snowflaking.edist_def, Orientation.rightAngleRotation_map, Finsupp.Colex.single_le_iff, IsUpperSet.toDual, antivary_toDual_left, OrderDual.toDual_eq_bot, AddSubgroup.quotientEquivProdOfLE'_symm_apply, RootPairing.Hom.coroot_coweightMap_apply, PartENat.withTopEquiv_symm_coe, Equiv.simpleGraph_apply, SymAlg.unsym_sub, WithTop.ofDual_symm_apply, CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation, CategoryTheory.Presheaf.coconeOfRepresentable_ι_app, ContinuousAlternatingMap.nnnorm_ofSubsingleton, LinearAlgebra.FreeProduct.lift_symm_apply, DomMulAct.isOpenEmbedding_mk_symm, Multiset.cast_apply_snd, IsCyclic.mulAutMulEquiv_symm_apply_apply, RootPairing.reflectionPerm_inv, Order.isSuccPrelimit_toDual_iff, Equiv.injective, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit, Nat.equivProdNatFactoredNumbers_apply', Set.dual_ordConnected_iff, Submonoid.toAddSubmonoid'_closure, Action.diagonalSuccIsoTensorDiagonal_hom_hom, CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm_assoc, Monoid.Foldr.ofFreeMonoid_apply, equivShrink_inv, Antivary.dual_right, QuotientAddGroup.equivIcoMod_zero, HahnModule.of_symm_zero, OrderIso.sumLexAssoc_apply_inr, UniformFun.ofFun_sub, Topology.WithUpper.toUpper_le_toUpper, Equiv.Perm.self_trans_inv, QuaternionAlgebra.imJ_equivProd_symm_apply, CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_obj, OrderDual.ofDual_toDual, CategoryTheory.conjugateEquiv_adjunction_id_symm, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv_symm_apply, Sym.coe_cast, finRotate_symm_lt_iff_ne_zero, WeakDual.CharacterSpace.equivAlgHom_coe, MulEquiv.withZero_symm_apply_apply, OrderHom.dual_symm_apply_coe, Equiv.optionSubtypeNe_none, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, HahnModule.of_zero, CliffordAlgebra.lift_comp_ι, DirectSum.decompose_mul, Subgroup.IsComplement.equiv_mul_right, isOpenMap_ofAdd, Metric.Snowflaking.preimage_ofSnowflaking_emetricBall, NumberField.Units.logEmbeddingEquiv_apply, MulEquiv.op_symm_apply_symm_apply, equicontinuousAt_iff_continuousAt, UniformOnFun.toFun_inv, AddEquiv.toMultiplicativeLeft_symm_apply_apply, CategoryTheory.ShrinkHoms.comp_def, finSumNatEquiv_symm_apply_of_ge, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, WithBot.toDual_symm_apply, NonemptyInterval.toLex_lt_toLex, Matrix.mulVecLin_reindex, Equiv.surjective, MvPolynomial.isSymmetric_rename, Circle.expHom_apply, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, CategoryTheory.Limits.WalkingPair.swap_apply_left, CategoryTheory.Localization.SmallShiftedHom.precompEquiv_apply, SSet.yonedaEquiv_comp, AlgEquiv.op_symm_apply_apply, SSet.op_map, Function.fromTypes_zero_equiv_apply, ContinuousAlgEquiv.cast_apply, DomMulAct.symm_mk_inv, CategoryTheory.ObjectProperty.isColocal.homEquiv_apply, UniformOnFun.ofFun_mul, FirstOrder.Language.BoundedFormula.mapTermRelEquiv_symm_apply, Sum.Lex.not_inr_le_inl, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, Equiv.Perm.subtypeEquivSubtypePerm_symm_apply, DomMulAct.coe_mkHomeomorph, RootPairing.reflectionPerm_eq_of_pairing_eq_zero', CategoryTheory.Limits.CofanTypes.equivOfIsColimit_apply, FreeMonoid.smul_def, Ideal.associatesEquivIsPrincipal_map_zero, MeasureTheory.continuous_diracProbaEquivSymm, Monoid.CoprodI.of_leftInverse, Equiv.piCurry_symm_apply, AddSubsemigroup.toSubsemigroup_closure, Equiv.Set.sumDiffSubset_apply_inl, FreeAddMonoid.map_apply_map_symm_eq, DualNumber.lift_apply_inl, PadicInt.continuousAddCharEquiv_symm_apply, Finset.Colex.le_iff_sdiff_subset_lowerClosure, MonoidHom.op_apply_apply, AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd, QuotientAddGroup.equivIcoMod_coe, CategoryTheory.OverPresheafAux.MakesOverArrow.of_arrow, Equiv.optionSubtype_symm_apply_apply_some, CategoryTheory.Functor.flippingEquiv_apply_obj_map, Filter.HasBasis.comp_equiv, Matrix.cons_mulVec, ContinuousMultilinearMap.domDomCongrEquiv_symm_apply, Equiv.Perm.mul_refl, ContinuousMultilinearMap.norm_ofSubsingleton, SSet.OneTruncation₂.nerveHomEquiv_apply, Multiplicative.exists, ofAdd_nsmul, FintypeCat.uSwitchEquiv_symm_naturality, Matrix.mul_fin_three, Orientation.map_apply, CStarMatrix.uniformEmbedding_ofMatrix, Quaternion.imI_equivProd_symm_apply, UniformOnFun.uniformSpace_eq_inf_precomp_of_cover, DirectSum.decompose_coe, CategoryTheory.Discrete.equivOfEquivalence_symm_apply, CoxeterSystem.lengthParity_eq_ofAdd_length, CategoryTheory.ShrinkHoms.inverse_map, Submodule.setSemiring_smul_def, MulEquiv.coe_toEquiv, Finset.Iic_toDual, SymAlg.sym_comp_unsym, HVertexOperator.coeff_comp, Algebra.TensorProduct.liftEquiv_symm_apply_coe, CoxeterMatrix.reindexGroupEquiv_symm_apply_simple, CompleteLatticeHom.dual_comp, Equiv.Set.sumCompl_apply_inl, Equiv.funUnique_symm_apply, Metric.Snowflaking.dist_ofSnowflaking_ofSnowflaking, SheafOfModules.conjugateEquiv_pullbackId_hom, NumberField.mixedEmbedding.indexEquiv_apply_isComplex_snd, Setoid.prodQuotientEquiv_apply, Ordinal.to_leftMoves_one_toPGame_symm, CategoryTheory.PreGaloisCategory.endEquivAutGalois_π, AddMonoidHom.toMultiplicativeLeft_apply_apply, CategoryTheory.Meq.equiv_symm_eq_apply, CategoryTheory.Presieve.extension_iff_amalgamation, DualNumber.lift_op_smul, Finset.Colex.cons_le_cons, BotHom.symm_dual_comp, toMul_list_sum, zmultiplesHom_symm_apply, FreeMonoid.lift_apply, Rack.act'_symm_apply, DirectSum.decompose_one, UniformOnFun.edist_eq_restrict_sUnion, Matrix.comp_diagonal, Monovary.dual, PEquiv.transpose_toMatrix_toPEquiv_apply, CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀Inv, finTwoArrowEquiv'_sum_eq, isRegular_toMul, Finset.finsetCongr_piAntidiag_eq_antidiag, ofLex_mul, OrderIso.smulRightDual_symm_apply, toColex_zero, CategoryTheory.MonoidalClosed.curryHomEquiv'_apply, FreeLieAlgebra.lift_of_apply, Cubic.equiv_symm_apply_d, norm_toMul, DomMulAct.symm_mk_mul, Finsupp.DegLex.le_iff, Equiv.one_def, Equiv.coe_sigmaUnique, HVertexOperator.coeff_apply_apply, Equiv.Perm.decomposeOption_symm_apply, CategoryTheory.Bicategory.mateEquiv_apply, UniformFun.uniformContinuous_toFun, Metric.Snowflaking.isBounded_preimage_toSnowflaking_iff, SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes, Algebra.discr_powerBasis_eq_prod', Equiv.prodCongrRight_symm, WithCStarModule.equiv_symm_fst, QuaternionAlgebra.imI_equivProd_symm_apply, BotHom.dual_comp, CategoryTheory.eHomEquiv_comp_assoc, antitone_comp_ofDual_iff, CategoryTheory.Pi.equivalenceOfEquiv_inverse, Matrix.det_submatrix_equiv_self, Metric.Snowflaking.image_ofSnowflaking_closedBall, Homeomorph.homeomorph_mk_coe_symm, groupHomology.mkH1OfIsTrivial_apply, Equiv.vadd_def, freeGroupEquivCoprodI_apply, Subgroup.transferTransversal_apply'', AddMonoidHom.mulOp_symm_apply_apply, Representation.ofMulDistribMulAction_apply_apply, Sum.Lex.le_def, FreeAddMonoid.toList_ofList, Equiv.listUniqueEquiv_apply, Ici_orderDual_def, SSet.Subcomplex.PairingCore.ancestralRel_iff, Multiplicative.forall, Fin.appendEquiv_symm_apply, CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition'_assoc, zpowersHom_ker_eq, HVertexOperator.of_coeff_apply, Function.OfArity.curryEquiv_apply, UniformOnFun.toFun_mul, CategoryTheory.conjugateEquiv_adjunction_id, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, CircleDeg1Lift.translationNumber_translate, AddSubgroup.quotientEquivProdOfLE_apply, Finset.symInsertEquiv_symm_apply_coe, CategoryTheory.coyonedaEquiv_symm_map, Matrix.compRingEquiv_apply, CategoryTheory.PreZeroHypercover.interFst_h₀, toColex_div, Equiv.embeddingCongr_apply_trans, CategoryTheory.Adjunction.homEquiv_naturality_right_square, LinearAlgebra.FreeProduct.lift_apply, PowerBasis.liftEquiv'_symm_apply_apply, PiTensorProduct.lift_comp_reindex_symm, CategoryTheory.PreOneHypercover.inter_p₁, DirectSum.decompose_mul_add_right, QuasiconcaveOn.dual, Finsupp.optionEquiv_symm_apply, Pi.le_toColex_update_self_iff, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_map, Quiver.starEquivCostar_symm_apply_snd, Finsupp.equivFunOnFinite_symm_single, Topology.IsQuotientMap.liftEquiv_apply, Equiv.withTopSubtypeNe_apply, Subgroup.toAddSubgroup'_closure, SymAlg.sym_smul, finSuccEquiv'_symm_some, Multiplicative.ofAdd_mono, Equiv.subset_symm_image, Equiv.piFinsetUnion_left, HahnEmbedding.Partial.eval_eq_truncLT, ofMul_toMul, Equiv.div_def, FreeMonoid.ofList_flatten, PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal, WithTop.toDual_map, Equiv.coe_fn_injective, Equiv.prodShear_apply, PresheafOfModules.freeYonedaEquiv_comp, Nat.toAdd_pow, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq, Equiv.comp_injective, Equiv.preimage_piEquivPiSubtypeProd_symm_pi, Module.Basis.toMatrix_reindex', AddMonCat.equivalence_functor_map, DomAddAct.vadd_apply, Unitization.starLift_range_le, HahnModule.coeff_smul_left, AddSubsemigroup.equivOp_apply_coe, UniformFun.toFun_inv, Sym2.lift_mk, HahnSeries.finiteArchimedeanClassOrderIso_apply, FirstOrder.Language.LEquiv.onBoundedFormula_apply, isMaxOn_dual_iff, finFunctionFinEquiv_apply_val, Hamming.toHamming_inj, Order.pred_ofMul, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc, UniformOnFun.isUniformEmbedding_toFun_finite, Finsupp.equivFunOnFinite_symm_sum, SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero, Equiv.sigmaPreimageEquiv_symm_apply_fst, FreeAddMonoid.countP_apply, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal, toLex_eq_zero, BotHom.dual_id, MonoidHom.coe_toAdditiveRight, FormalMultilinearSeries.changeOriginIndexEquiv_apply_snd, UniformOnFun.postcomp_isUniformEmbedding, FreeAbelianGroup.lift_neg_apply, Hamming.ofHamming_neg, MonoidAlgebra.lift_def, Matroid.mapEquiv_isBasis_iff, MulEquiv.coe_toEquiv_symm, Equiv.ofLeftInverseOfCardLE_symm_apply, Equiv.transPartialEquiv_apply, Finset.Nat.sigmaAntidiagonalTupleEquivTuple_apply, UniformFun.ofFun_sum, MonomialOrder.lex_le_iff, Equiv.ringEquiv_apply, Equiv.piCongrLeft'_symm_apply_apply, ContinuousLinearMap.isUniformEmbedding_toUniformOnFun, InfClosed.dual, Matrix.submatrix_mul_equiv, CategoryTheory.Sieve.overEquiv_generate, isTop_ofDual_iff, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, FreeAddMonoid.ofList_comp_toList, isMin_ofDual_iff, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, CategoryTheory.Enriched.FunctorCategory.homEquiv_comp_assoc, AddMonoidHom.eq_liftOfRightInverse, Equiv.biInf_comp, toBoolRing_inj, Functor.mapEquiv_apply, stdSimplexEquivIcc_symm_apply_coe, Additive.exists, Metric.Snowflaking.ediam_preimage_toSnowflaking, Equiv.image_preimage, Equiv.pprodEquivProdPLift_symm_apply, LinearEquiv.symmEquiv_symm_apply_symm_apply, CategoryTheory.evalEquiv_symm_apply, IsSublattice.dual, Matrix.of_sub_of, Metric.Snowflaking.preimage_ofSnowflaking_emetricClosedBall, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_apply_app, SSet.Subcomplex.PairingCore.equivII_apply_coe, continuousOn_cfc_nnreal_setProd, TopHom.dual_comp, MonoidHom.liftOfRightInverse_comp, Quiver.SingleObj.pathEquivList_cons, Prod.Lex.prodUnique_apply, UniformFun.toFun_sum, Matrix.charpoly_reindex, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, CategoryTheory.Functor.Elements.initialOfRepresentableBy_snd, DomMulAct.isOpenEmbedding_mk, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one, WithCStarModule.equivL_symm_apply, UniformFun.ofFun_add, Metric.Snowflaking.homeomorph_symm_apply, isAddLeftRegular_ofLex, AddSubgroup.equivOp_apply_coe, Equiv.sigmaFiberEquiv_symm_apply_fst, CategoryTheory.Functor.CorepresentableBy.ext_iff, FreeAbelianGroup.lift_apply_of, zpowersEquivZPowers_apply, CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp, DomMulAct.isQuotientMap_mk, isClosedMap_toMul, FreeAddMagma.lift_of, ContinuousMap.unitsLift_symm_apply_apply_inv', MulEquiv.op_symm_apply_apply, RootPairing.reflectionPerm_eq_of_pairing_eq_zero, DualNumber.lift_comp_inlHom, CartanMatrix.A_one, comp_equiv_dotProduct_comp_equiv, DomMulAct.isEmbedding_mk_symm, IsCoatom.dual, MulEquiv.Monoid.End_apply, coe_notMemRangeEquiv_symm, YoungDiagram.equivListRowLens_symm_apply, List.equivSigmaTuple_apply_fst, FreeAbelianGroup.liftAddEquiv_apply_apply, CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left, AddMonoidAlgebra.decomposeAux_eq_decompose, UniformEquiv.piCongr_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left, Matrix.kroneckerTMul_assoc, HahnEmbedding.Partial.evalCoeff_eq, CategoryTheory.Functor.flippingEquiv_apply_map_app, IsCompl.dual, ofDual_bihimp, CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply, Abelianization.lift_symm_apply, Setoid.quotientKerEquivOfRightInverse_symm_apply, PiTensorProduct.map_comp_reindex_eq, WeakDual.CharacterSpace.equivAlgHom_symm_coe, toLex_div, CategoryTheory.Localization.Construction.objEquiv_symm_apply, Finset.map_ofDual_min, Multiset.consEquiv_symm_none, CategoryTheory.Functor.homEquivOfIsRightKanExtension_apply_app, CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str, CategoryTheory.Functor.CoconeTypes.IsColimit.equiv_apply, ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le, Unitization.lift_apply_apply, CategoryTheory.Limits.IsLimit.homEquiv_symm_naturality, OrderIso.divLeft_symm_apply, Equiv.self_comp_ofInjective_symm, CategoryTheory.conjugateIsoEquiv_symm_apply_hom, Subgroup.quotientEquivSigmaZMod_symm_apply, MonoidHom.toAdditiveLeft_symm_apply_apply, Equiv.addEquiv_symm_apply, MonoidHom.toHomPerm_apply_apply, MvPolynomial.IsSymmetric.antitone_supDegree, Valuation.toValuation_ofValuation, toColex_pow, Finmap.keysLookupEquiv_symm_apply_lookup, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, Zsqrtd.lift_injective, Cubic.equiv_symm_apply_a, isMinFilter_dual_iff, isSublattice_preimage_toDual, OrderDual.isCobounded_preimage_ofDual, SupIrred.dual, toDual_eq_one, CategoryTheory.Adjunction.homAddEquiv_apply, Interval.dual_map, ofDual_add, isLeftRegular_ofLex, EquicontinuousOn.isInducing_uniformOnFun_iff_pi, MvPolynomial.degreeOf_eq_natDegree, Equiv.prodPProd_symm_apply, CompHausLike.isoEquivHomeo_apply, uniformContinuous_ofAdd, SimpleGraph.hasseDualIso_symm_apply, UniformEquiv.uniformEquiv_mk_coe_symm, isAddLeftRegular_toColex, supPrime_ofDual, Finset.restrict_comp_piCongrLeft, FreeAddGroup.lift_of_apply, Equiv.subtypeEquivCodomain_symm_apply_ne, UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv, CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_id, Encodable.encode_ofEquiv, toDual_symmDiff, dist_ofMul, Equiv.functionSwap_symm_apply, Equiv.Perm.decomposeOption_apply, Finsupp.optionEquiv_apply, StrictConcaveOn.dual, toDual_smul, CategoryTheory.Adjunction.homEquiv_naturality_right_square_assoc, CategoryTheory.Under.postAdjunctionRight_counit_app_right, optionProdEquiv_mk_none, TopologicalSpace.Compacts.equiv_apply, isRightRegular_ofAdd, PadicInt.continuousAddCharEquiv_apply, CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom, monotone_comp_ofDual_iff, Matrix.coe_ofLinearEquiv_symm, CategoryTheory.unitCompPartialBijectiveAux_symm_apply, DirectSum.liftRingHom_apply, Finite.card_eq, CliffordAlgebra.GradedAlgebra.lift_ι_eq, WithConv.symm_equiv_apply, UniformOnFun.ofFun_add, MonoidAlgebra.mapDomainAddEquiv_apply, Monoid.Coprod.lift_apply_mk, FreeAddSemigroup.lift_of_add, ofDual_sSup, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc, Subgroup.IsComplement.rightQuotientEquiv_apply, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe, AddCommMonCat.equivalence_inverse_map, CategoryTheory.Localization.SmallShiftedHom.equiv_mk₀, Multiset.coeEquiv_symm_apply_snd_val, SimpleGraph.Iso.mapEdgeSet_apply, Sum.Lex.inr_top, isAddRegular_toDual, AddMonoidAlgebra.lift_def, Subgroup.IsComplement'.QuotientMulEquiv_apply, Perfection.lift_symm_apply, CategoryTheory.Bicategory.Adjunction.homEquiv₁_symm_apply, CategoryTheory.Bicategory.toNatTrans_conjugateEquiv, CategoryTheory.Discrete.equivalence_inverse, CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm, equivShrink_smul, Equiv.extend_apply, MvPolynomial.leadingCoeff_toLex, CategoryTheory.Equivalence.induced_functor, isAddRightRegular_toAdd, SetSemiring.down_up, Equiv.isOpenMap_symm_iff, UniformFun.ofFun_toFun, FreeAddMonoid.hom_map_lift, OneOneEquiv.of_equiv, HahnSeries.leadingCoeff_neg_iff, Equiv.sigmaFiberEquiv_symm_apply_snd_coe, InverseSystem.invLimEquiv_symm_apply_coe, ComplexShape.Embedding.AreComplementary.equiv_inr, DirectSum.coe_decompose_mul_of_left_mem_zero, AddConstMap.coe_conjNeg_apply, Prod.Lex.toLex_le_toLex, Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_ne, Partition.partscopyEquiv_apply_coe, Primrec.of_equiv_iff, CategoryTheory.Limits.Cofork.IsColimit.homIso_symm_apply, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one, ModularGroup.coe_T_zpow, Algebra.GrothendieckGroup.lift_apply, Set.graphOn_prod_prodMap, IsMin.toDual, equivShrink_le_equivShrink, FirstOrder.Language.Term.relabelEquiv_apply, CategoryTheory.Localization.SmallHom.equiv_shift, CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_symm_apply_coe, MonoidHom.coe_toAdditive'', OrderHom.equivFunctor_symm_apply, FreeGroup.freeGroupCongr_apply, Matrix.uniqueEquiv_apply, Equiv.Perm.sameCycle_extendDomain, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, DirectSum.coe_decompose_mul_of_right_mem_of_le, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, Subgroup.IsComplement.equiv_fst_eq_mul_inv, Function.OfArity.curry_two_eq_curry, FreeGroup.lift_mk, Equiv.sumArrowEquivProdArrow_symm_apply_inl, LieAlgebra.of_symm_add, MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_apply, AffineEquiv.map_vadd', MvPowerSeries.lexOrder_le_of_coeff_ne_zero, Combinatorics.Subspace.reindex_isMono, Equiv.apply_eq_iff_eq, ofDual_vadd', CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc, CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_apply, FreeMonoid.ofList_comp_toList, CategoryTheory.opEquiv_symm_apply, Metric.Snowflaking.image_toSnowflaking_image_ofSnowflaking, CategoryTheory.ObjectProperty.galoisConnection_isLocal, Monoid.CoprodI.lift_word_ping_pong, Set.RightInvOn.extendDomain, isRegular_ofDual, CategoryTheory.ShrinkHoms.functor_map, Fin.revPerm_symm_apply, CategoryTheory.orderDualEquivalence_inverse_obj, Quaternion.equivTuple_symm_apply, Unitization.starLift_symm_apply, CategoryTheory.MonoidalClosed.ofEquiv_curry_def, Equiv.forall_congr_right, Matrix.diagonal_fin_three, ContinuousMultilinearMap.curryFinFinset_symm_apply, equivTangentBundleProd_symm_apply_proj, measurable_piCurry, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, TensorAlgebra.lift_unique, CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app, CategoryTheory.Abelian.Ext.homEquiv₀_symm_apply, edist_toDual, ofColex_neg, DirectSum.sum_support_decompose, toDual_iInf, Finsupp.toLex_monotone, CStarMatrix.of_zero, CategoryTheory.Bicategory.conjugateEquiv_symm_apply', OnePoint.equivProjectivization_apply_coe, Equiv.subRight_symm_apply, Matrix.comp_symm_apply, Finsupp.equivFunOnFinite_single, Subgroup.IsComplement.leftQuotientEquiv_apply, RootPairing.Equiv.id_indexEquiv_symm_apply, NumberField.Units.finrank_mul_regulator_eq_det, ofAdd_eq_one, Matrix.rank_submatrix_le, Function.fromTypes_cons_equiv_apply, SupHom.dual_symm_apply_toFun, DomMulAct.mk_one, LinearAlgebra.FreeProduct.lift_comp_ι, Delone.DeloneSet.mapIsometry_apply_coveringRadius, CategoryTheory.nerve.functorOfNerveMap_obj, CategoryTheory.Adjunction.homAddEquiv_symm_sub, Matrix.transpose_empty_rows, CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm, UniformOnFun.isUniformInducing_pi_restrict, RingHom.op_apply_apply, Equiv.smulRight_apply, AddChar.toAddMonoidHomEquiv_apply, equiv_lpPiLp_norm, MulEquiv.monoidHomCongrRightEquiv_symm_apply, MulEquiv.subgroupMap_symm_apply, Quiver.SingleObj.toPrefunctor_symm_comp, Sum.Lex.toLexRelIsoLT_symm_coe, WithZero.lift'_zero, Matrix.piEquiv_apply, WithTop.toDual_le_iff, UniformOnFun.uniformContinuous_ofFun_toFun, ofLex_div, Equiv.mulRight_symm_apply, Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe, Finsupp.Colex.single_lt_iff, Equiv.sigmaProdDistrib_apply, UniformEquiv.piCongrLeft_apply_apply, Monoid.CoprodI.lift_comp_of', Equiv.sumIsRight_symm_apply_coe, Equiv.sigmaSubtype_apply, Submodule.span.ringHom_apply, UniformOnFun.edist_le, CategoryTheory.Limits.Sigma.ι_reindex_hom_assoc, nnnorm_toAdd, Equiv.sumPiEquivProdPi_apply, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, FreeMonoid.countP_apply, equivShrink_neg, FirstOrder.Language.LEquiv.onSentence_symm_apply, MultilinearMap.curryFinFinset_symm_apply, DirectSum.coe_decompose_mul_of_right_mem_zero, Multiplicative.ext_iff, Equiv.image_symm_apply_coe, CategoryTheory.Iso.eHomCongr_inv_comp, OrderDual.ofDual_lt_ofDual, FreeMonoid.freeMonoidCongr_symm_of, Matrix.invertibleEquivDetInvertible_symm_apply, Sum.Lex.toLex_strictMono, Prod.Lex.prodLexCongr_apply, OrderDual.ofDual_comp_toDual, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp, CategoryTheory.Localization.homEquiv_map, Equiv.Perm.SameCycle.symm_apply_left, Matrix.comp_map_transpose, RootPairing.indexNeg_neg, TrivSqZeroExt.liftEquiv_symm_apply_coe, subtypeOrEquiv_apply, Equiv.boolNot_symm_apply, Trunc.finChoiceEquiv_symm_apply, Subsemigroup.equivOp_apply_coe, RootPairing.chainBotCoeff_reflectionPerm_left, DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff, Matrix.submatrixEquivInvertibleEquivInvertible_symm_apply, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_apply, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, finSumNatEquiv_symm_apply_of_lt, CStarMatrix.of_add_of, FreeMagma.lift_comp_of', GradedAlgebra.mem_support_iff, MonoidHom.fiberEquiv_apply, Topology.lawsonOpen_iff_scottOpen_of_isUpperSet, monotoneOn_dual_iff, FinBddDistLat.dual_map, Equiv.mulEquiv_symm_apply, Monoid.Coprod.map_mk_ofList, Finsupp.Lex.lt_iff, CategoryTheory.conjugateEquiv_comp, Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem, Finsupp.DegLex.monotone_degree, Metric.Snowflaking.image_toSnowflaking_ball, CategoryTheory.map_shrinkYonedaEquiv, AlgEquiv.sumArrowEquivProdArrow_apply, PEquiv.mul_toMatrix_toPEquiv, SimpleGraph.Iso.connectedComponentEquiv_apply, Equiv.Perm.SameCycle.extendDomain, Equiv.image_apply_coe, EquivFunctor.mapEquiv_symm_apply, FreeMonoid.count_apply, Quiver.SingleObj.toPrefunctor_symm_apply, Finpartition.IsEquipartition.exists_partPreservingEquiv, toDual_sup, Equiv.Perm.perm_inv_mapsTo_iff_mapsTo, Equiv.Perm.perm_symm_on_of_perm_on_finite, RootPairing.Base.IsPos.reflectionPerm, addMonoidEndToMultiplicative_apply_apply, WithTop.ofDual_top, Equiv.toOrderIsoSet_apply, Equiv.Perm.sameCycle_symm_apply_left, Finsupp.equivFunOnFinite_symm_eq_sum, AlgEquiv.funUnique_symm_apply, List.sym2_eq_sym_two, nhds_ofAdd, Equiv.conj_apply, CategoryTheory.Adjunction.homEquiv_apply_eq, CategoryTheory.yonedaEquiv_symm_map, toDual_iSup, CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation, FreeMonoid.map_symm_apply_map_eq, CategoryTheory.Cat.Hom.equivFunctor_apply, Equiv.psigmaEquivSigmaPLift_symm_apply, WithTop.lt_ofDual_iff, IsTop.toDual, Magma.AssocQuotient.lift_symm_apply, Equiv.optionSubtypeNe_apply, finite_iff_exists_equiv_fin, toDual_ofNat, MulChar.coe_equivToUnitHom, CategoryTheory.CartesianMonoidalCategory.homEquivToProd_apply, PEquiv.toMatrix_toPEquiv_apply, Equiv.rightInverse_symm, SymAlg.sym_one, ofColex_toColex, Equiv.coe_trans, FreeAddMonoid.toList_cons, Multiplicative.monoidHom_ext_iff, Rep.coinvariantsAdjunction_homEquiv_apply_hom, LinearEquiv.piCongrLeft'_apply, isRegular_toColex, Equiv.ofUnique_symm_apply, WithCStarModule.equiv_symm_pi_apply, Equiv.prodSumDistrib_symm_apply_left, Equiv.optionSubtype_symm_apply_symm_apply, toDual_div, NonemptyInterval.snd_dual, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, CategoryTheory.Bicategory.conjugateEquiv_iso, finSuccAboveOrderIso_symm_apply_ne_last, FreeAbelianGroup.lift_neg, powersEquivPowers_apply, CategoryTheory.Bicategory.conjugateEquiv_comm, NumberField.Units.regulator_eq_det', FreeNonUnitalNonAssocAlgebra.lift_of_apply, Concept.swapEquiv_symm_apply, CategoryTheory.uliftCoyonedaEquiv_symm_map, HasStrictDerivAt.hasStrictFDerivAt_equiv, Specialization.toEquiv_ofEquiv, Equiv.extendSubtype_apply_of_mem, CategoryTheory.TwoSquare.lanBaseChange_app, IsSymmetricAlgebra.equiv_toAlgHom, Sum.Lex.inr_lt_inr_iff, ModularGroup.coe_S, ofDual_mul, IsometryEquiv.coe_mk, Matrix.vecMul_cons, DomAddAct.isClosedEmbedding_mk, Metric.Snowflaking.continuous_ofSnowflaking, CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe, Matrix.compLinearEquiv_apply, CategoryTheory.Sheaf.ΓObjEquivSections_naturality, CategoryTheory.yonedaEquiv_symm_naturality_left, Invertible.mulRight_symm_apply, Affine.Simplex.height_reindex, CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply, Set.Ici_toDual, UniformOnFun.uniformContinuous_eval_of_mem, Set.Icc_toDual, RelIso.coe_fn_toEquiv, SSet.Subcomplex.Pairing.exists_or, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, UniformFun.uniformSpace_eq_inf_precomp_of_cover, Subgroup.IsComplement.equiv_mul_left, Metric.PiNatEmbed.toPiNatEquiv_symm_apply, Function.Embedding.toEquivRange_apply, CategoryTheory.PreZeroHypercover.isoMk_inv_h₀, sSupHom.dual_id, DirectSum.decompose_symm_of, Finset.orderIsoColex_symm_apply, OrderDual.isCobounded_preimage_toDual, OrderIso.sumLexDualAntidistrib_symm_inr, Finsupp.Lex.single_le_iff, QuaternionAlgebra.equivProd_apply, Preorder.piCongrLeft_comp_restrictLe, Matroid.mapEquiv_eq_map, CharacterModule.homEquiv_apply_apply, IncidenceAlgebra.mu_toDual, CategoryTheory.Functor.CoconeTypes.isColimit_iff, Equiv.sigmaPUnit_symm_apply_fst, CategoryTheory.Bicategory.conjugateEquiv_whiskerLeft, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, toBoolRing_top, CategoryTheory.mateEquiv_counit, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset, FreeGroup.lift_eq_prod_map, UniformOnFun.toFun_smul, RootPairing.pairing_reflectionPerm, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor', nhds_toDual, CategoryTheory.Functor.flippingEquiv_apply_obj_obj, AddSubmonoid.closure_eq_mrange, Diffeomorph.toEquiv_coe_symm, CategoryTheory.yonedaEquiv_symm_naturality_right, Equiv.optionEquivSumPUnit_coe, SheafOfModules.pushforwardSections_unitHomEquiv, Equiv.sigmaPreimageEquiv_apply, RelIso.preimage_symm_apply, Monoid.CoprodI.lift_comp_of, continuous_toMul, CategoryTheory.mateEquiv_square, UniformOnFun.ofFun_smul, RootPairing.EmbeddedG2.ofPairingInThree_long, Matroid.mapSetEquiv_indep_iff, UniformFun.dist_def, FreeAbelianGroup.liftMonoid_symm_coe, StrictMonoOn.dual_right, Ctop.ofEquiv_val, Equiv.subtypePreimage_symm_apply_coe_neg, CategoryTheory.Localization.SmallShiftedHom.equiv_apply, toColex_eq_one, DomMulAct.symm_mk_zpow, Monoid.CoprodI.lift_range_le, PartialFun.Iso.mk_hom, CategoryTheory.PreZeroHypercover.isoMk_inv_s₀, OrderIso.sumLexDualAntidistrib_inr, Matrix.mulVec_cons, stdSimplexEquivIcc_one, Equiv.Set.union_apply_right, Cardinal.mk_equiv_eq_arrow_of_eq, Matrix.comp_symm_single, Matrix.head_transpose, RootPairing.coroot_reflectionPerm, SetSemiring.mul_def, Ctop.Realizer.ofEquiv_F, Finsupp.snd_sumFinsuppEquivProdFinsupp, WithCStarModule.equivL_apply, CategoryTheory.Functor.partialLeftAdjointHomEquiv_comp_symm, Set.image_equiv_eq_preimage_symm, RootPairing.isFixedPt_reflectionPerm_iff, Equiv.prodShear_symm_apply, AddEquiv.op_symm_apply_apply, Equiv.apply_ofInjective_symm, FinEnum.equiv_down, RingEquiv.nonUnitalSubsemiringMap_apply_coe, SSet.stdSimplex.objEquiv_symm_apply, AddAut.neg_conj_apply, CompleteLatticeHom.symm_dual_comp, measurable_equivCurry, UniformFun.toFun_mul, AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe, OrderAddMonoidHom.inrₗ_apply, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, MonoidHom.coe_toMultiplicative, NonemptyInterval.toDualProd_apply, isRegular_ofLex, Submonoid.powLogEquiv_symm_apply, InverseSystem.piLTLim_apply, CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_equiv, Ordinal.toLeftMovesToPGame_symm_lt, Equiv.symm_image_image, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, Algebra.traceForm_toMatrix_powerBasis, toDual_ratCast, MvPolynomial.rename_hsymm, SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one_assoc, CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift, UniformFun.postcomp_isUniformEmbedding, Metric.Snowflaking.image_ofSnowflaking_image_toSnowflaking, UniformOnFun.toFun_prod, Equiv.Perm.IsCycleOn.extendDomain, SkewMonoidAlgebra.lift_def, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, SymAlg.unsym_sym, CategoryTheory.Functor.CoconeTypes.IsColimit.equiv_symm_ι_apply, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, Metric.Snowflaking.image_ofSnowflaking_emetricBall, RootPairing.coroot'_reflectionPerm, Equiv.ringEquiv_symm_apply, finFunctionFinEquiv_apply, DirectSum.decompose_neg, equivShrink_symm_mul, RingEquiv.piFinTwo_apply, Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe, UniformConvergenceCLM.isUniformEmbedding_coeFn, CategoryTheory.uliftYonedaEquiv_symm_map_assoc, Finset.prod_map_equiv, Topology.WithLowerSet.ofLowerSet_toLowerSet, SetTheory.PGame.moveLeft_nim, AddMonoidHom.coe_toMultiplicative'', finFunctionFinEquiv_single, DomMulAct.mk_smul_monoidHom_apply, Matrix.coe_ofLinearEquiv, ofDegLex_add, Dense.orderDual, ofLex_eq_zero, CategoryTheory.Functor.curryingEquiv_symm_apply_obj_map, CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux, HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_mk, Set.Finite.subtypeEquivToFinset_symm_apply_coe, Equiv.uniqueProd_apply, OrderDual.ofDual_inj, AlgEquiv.prodCongr_symm_apply, Algebra.GrothendieckAddGroup.lift_symm_apply, FinBoolAlg.dual_map, DomAddAct.isEmbedding_mk_symm, UniformFun.lipschitzOnWith_iff, equivEquivIso_inv, Equiv.Set.union_symm_apply_right, Setoid.quotientEquivClasses_mk_eq, Matrix.posSemidef_submatrix_equiv, Homeomorph.coe_toEquiv, PerfectionMap.lift_apply, grade_toDual, OrderIso.asBoolAlgAsBoolRing_symm_apply, Subgroup.IsComplement.equiv_snd_eq_inv_mul, nonempty_equiv_of_countable, Set.matrix_eq_pi, toBoolAlg_one, Prod.Lex.lt_iff, AddUnits.addLeft_apply, continuousOn_cfcₙ_nnreal_setProd, strictMonoOn_comp_ofDual_iff, SheafOfModules.generatorsOfIsCokernelFree_s, rootsOfUnityEquivNthRoots_symm_apply, StrictMonoOn.dual, Equiv.Set.univPi_apply_coe, Fin.appendEquiv_apply, SSet.Truncated.HomotopyCategory.descOfTruncation_obj_mk, Cardinal.mk_equiv_of_lift_eq, Monoid.CoprodI.lift_injective_of_ping_pong, AlgHom.op_symm_apply_apply, Hamming.toHamming_neg, powersMulHom_symm_apply, SymAlg.unsym_neg, Monoid.PushoutI.NormalWord.summand_smul_def, Equiv.sigmaCongrRight_apply, toBoolAlg_ofBoolAlg, SkewMonoidAlgebra.equivMapDomain_eq_mapDomain, AddMonoidAlgebra.of'_eq_of, SemidirectProduct.equivProd_symm_apply_left, ofAdd_toDual_eq_zero_iff, FreeMonoid.ofList_map, EquivLike.coe_coe, OrderDual.ofDual_eq_top, isCoatom_dual_iff_isAtom, Finsupp.DegLex.lt_def, Set.MapsTo.exists_equiv_extend_of_card_eq, Equiv.Perm.val_inv_equivUnitsEnd_apply, Additive.addMonoidHom_ext_iff, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app, Function.update_apply_equiv_apply, Matrix.transpose_reindex, AddCircle.liftIco_eq_lift_Icc, Prod.Lex.prodLexAssoc_apply, Monoid.foldrM.ofFreeMonoid_apply, Complex.isUniformEmbedding_equivRealProd, Unitization.lift_apply, CategoryTheory.Limits.biproduct.reindex_hom, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, toDual_natCast, Equiv.piEquivPiSubtypeProd_apply, CircleDeg1Lift.translate_pow, CategoryTheory.Arrow.equivSigma_apply_snd_fst, ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap, strictMono_toDual_comp_iff, CovBy.ofDual, ofDual_vadd, Opposite.equivToOpposite_symm_coe, toDual_add, Equiv.optionEquivSumPUnit_some, Matrix.coe_ofAddEquiv, FreeGroup.range_lift_le, EisensteinSeries.gammaSetDivGcdEquiv_eq, FreeSemigroup.lift_of_mul, CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_φ, LT.lt.ofDual, LieAlgebra.of_symm_smul, Equiv.multipliable_iff, Module.Basis.orientation_map, FreeMonoid.toList_one, Finset.Colex.toColex_le_toColex_of_subset, Subsemigroup.toAddSubsemigroup'_closure, Finset.ofDual_max', CategoryTheory.Adjunction.homEquiv_naturality_right, HahnEmbedding.Partial.apply_of_mem_stratum, OrderIso.dual_symm_apply, CategoryTheory.Functor.IsRepresentedBy.iff_exists_representableBy, AddValuation.ofValuation_apply, MvPolynomial.mapEquivMonic_symm_map_algebraMap, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, CategoryTheory.CosimplicialObject.cechConerveEquiv_apply, Matrix.reindex_updateCol, CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map, CategoryTheory.Bicategory.conjugateEquiv_symm_apply, HNNExtension.NormalWord.unitsSMulEquiv_apply, Multiset.coe_consEquiv_of_ne, CategoryTheory.Meq.equiv_apply, DirectSum.decompose_symm_sum, RootPairing.Hom.id_indexEquiv_apply, List.Nodup.getEquiv_symm_apply_val, Equiv.sumCompl_symm_apply_of_neg, NumberField.Units.regOfFamily_eq_det', AddSubgroup.toSubgroup_comap, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, ofDual_covBy_ofDual_iff, OrderIso.coe_toEquiv, Equiv.coe_subtypeEquivCodomain, finSumEquivOfFinset_inl, Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, Finset.prod_comp_equiv, ContinuousMultilinearMap.curryFinFinset_apply, Fin.equivSubtype_apply, bddAbove_preimage_toDual, AddSubgroup.coe_toSubgroup_symm_apply, ofDual_div, Matrix.blockTriangular_single', BddLat.dual_map, OrderIso.sumLexDualAntidistrib_inl, DomAddAct.isClosedEmbedding_mk_symm, Filter.map_equiv_symm, Units.mulRight_apply, SkewMonoidAlgebra.equivMapDomain_single, Equiv.Set.sumCompl_symm_apply_compl, MonovaryOn.dual, Order.coheight_ofDual, QuaternionAlgebra.coe_addEquivTuple, Equiv.subtypePreimage_symm_apply_coe, Equiv.image_eq_iff_bijOn, AlgebraicGeometry.coe_opensRestrict_apply_coe, Equiv.prodCongrRight_apply, SetSemiring.down_zero, FreeSemigroup.lift_comp_of, List.Nodup.getEquivOfForallMemList_apply, MulArchimedeanOrder.le_def, Equiv.pprodCongr_apply, DirectSum.decompose_add, Equiv.image_symm_eq_preimage, UniformEquiv.piCongrLeft_apply, ModuleCat.freeHomEquiv_symm_apply, ValuationSubring.primeSpectrumEquiv_apply, WithZero.val_logOrderIso_symm_apply, equivShrink_symm_inv, CategoryTheory.CommSq.LiftStruct.opEquiv_apply, IsMinOn.dual, Preorder.piCongrLeft_comp_frestrictLe, SeparationQuotient.liftNormedAddGroupHomEquiv_symm_apply_coe, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, FreeMonoid.toList_comp_ofList, Finsupp.sumFinsuppEquivProdFinsupp_apply, SymAlg.sym_mul_sym, Finsupp.Colex.lt_iff_of_unique, UniformOnFun.ofFun_neg, RootPairing.reflection_reflectionPerm, AlgEquiv.piCongrLeft'_symm_apply, multiplesHom_apply, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, PartENat.withTopEquiv_symm_lt, Equiv.extendSubtype_apply_of_not_mem, ContinuousMap.addUnitsLift_symm_apply_apply_neg', AlternatingMap.domDomCongr_apply, Equiv.sumEmpty_apply_inl, Equiv.sigmaEquivProd_apply, finAddFlip_apply_natAdd, Equiv.curry_symm_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right, MulChar.apply_mem_rootsOfUnity, toLex_smul, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe, Metric.Snowflaking.preimage_ofSnowflaking_closedEBall, CategoryTheory.ExponentiableMorphism.homEquiv_apply_eq, MonoidHom.toAdditiveRight_apply_apply, piFinTwoEquiv_symm_apply, DirectSum.decompose_sum, WithZero.toMulBot_symm_bot, Finset.ofDual_sup, HVertexOperator.comp_apply, cmpLE_toDual, Equiv.sigmaSubtype_symm_apply_coe_fst, CategoryTheory.Localization.homEquiv_isoOfHom_inv, CategoryTheory.Localization.homEquiv_id, toLex_one, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two_assoc, PartENat.withTopEquiv_symm_top, finAddFlip_apply_castAdd, FreeAddMonoid.ofList_singleton, HahnSeries.leadingCoeff_nonpos_iff, ModuleCat.homEquiv_extendScalarsId, UniformOnFun.lipschitzWith_restrict, ofAdd_neg, Equiv.symm_image_subset, Orientation.map_positiveOrientation_of_isEmpty, toBoolRing_symmDiff, PrimitiveSpectrum.gc, Equiv.optionSubtypeNe_symm_self, coe_toLexAddEquiv, Quotient.finChoiceEquiv_symm_apply, Orthonormal.equiv_apply, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, Finmap.keysLookupEquiv_apply_coe_fst, CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, toDual_covBy_toDual_iff, CategoryTheory.Bicategory.conjugateIsoEquiv_symm_apply_inv, IsMax.ofDual, CategoryTheory.Subfunctor.Subpresheaf.ofSection_eq_range, Combinatorics.Subspace.reindex_apply, Finsupp.restrictSupportEquiv_symm_apply_coe, Metric.Snowflaking.preimage_toSnowflaking_emetricBall, ofMul_eq_zero, CategoryTheory.Limits.Trident.IsLimit.homIso_natural, equivShrink_symm_one, CategoryTheory.Pi.equivalenceOfEquiv_functor, Equiv.sigmaPUnit_apply, MulEquiv.monoidHomCongrLeftEquiv_symm_apply, Shrink.linearEquiv_apply, Equiv.piUnique_symm_apply, CategoryTheory.CatEnrichedOrdinary.homEquiv_id, CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app, AddAutAdditive_symm_apply_apply, CategoryTheory.Presheaf.freeYonedaHomEquiv_symm_comp_assoc, Metric.Snowflaking.dist_toSnowflaking_toSnowflaking, Subgroup.IsComplement.equiv_fst_eq_self_iff_mem, Ideal.associatesEquivIsPrincipal_map_one, ofDual_zero, finEquivPowers_symm_apply, CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply, IsSimpleOrder.equivBool_apply, SupPrime.ofDual, List.SortedGE.of_map_toDual, Equiv.piUnique_apply, List.Nodup.getEquivOfForallMemList_symm_apply_val, OrderIso.sumLexIioIci_apply_inr, CategoryTheory.GradedObject.comapEquiv_functor, nndist_toAdd, Traversable.toList_spec, Hamming.toHamming_ofHamming, SetSemiring.up_down, PresentedGroup.equivPresentedGroup_apply_of, toDual_inf, DirectSum.decompose_smul, Equiv.algEquiv_symm_apply, OrthonormalBasis.repr_reindex, Topology.WithLower.ofLower_lt_ofLower, ContinuousMap.isUniformEmbedding_equivBoundedOfCompact, NormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe, TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply, Cardinal.mk_equiv_eq_zero_iff_lift_ne, MonoidHom.liftOfRightInverse_comp_apply, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism, EquivLike.coe_symm_comp_self, DFinsupp.equivFunOnFintype_symm_single, ofAdd_image_multiples_eq_powers_ofAdd, AddAction.toPerm_apply, Equiv.prod_assoc_symm_preimage, OrderIso.sumLexIioIci_symm_apply_of_lt, CategoryTheory.Abelian.Ext.mk₀_homEquiv₀_apply, ofDual_eq_zero, Additive.toMul_eq_top, WeierstrassCurve.Affine.Point.toClass_apply, CategoryTheory.Adjunction.homEquiv_id, Circle.argEquiv_apply_coe, strictAntiOn_dual_iff, CommGrpCat.toAddCommGrp_map, Module.Basis.reindex_apply, WType.NatαEquivPUnitSumPUnit_symm_apply, FreeAddSemigroup.lift_comp_of', Finset.Nat.antidiagonalEquivFin_apply_val, CategoryTheory.Adjunction.homEquiv_naturality_left, WCovBy.fst_ofLex, CategoryTheory.Functor.IsRepresentedBy.representableBy_homEquiv_apply, monovaryOn_toDual_left, toBoolRing_bot, CategoryTheory.orderDualEquivalence_inverse_map, Function.FromTypes.curryEquiv_apply, Equiv.coe_uniqueProd, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Module.Basis.repr_reindex_apply, Finset.sum_comp_equiv, Tuple.proj_equiv₁', Additive.foMul_strictMono, Equiv.setCongr_symm_apply, Matrix.adjugate_fin_two_of, Matrix.kroneckerMap_diagonal_left, ofColex_zero, cmp_ofDual, CategoryTheory.Limits.Cotrident.IsColimit.homIso_apply_coe, CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom, HahnSeries.iterateEquiv_symm_apply, Matrix.transposeInvertibleEquivInvertible_apply, Matroid.mapEquiv_isBase_iff, Matrix.one_fin_two, PerfectionMap.equiv_apply, WithBot.ofDual_le_ofDual_iff, measurable_piCongrLeft, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right, CategoryTheory.discreteEquiv_apply, WithZero.logEquiv_unitsMk0, SetTheory.PGame.moveRight_toRightMovesNim, WithZero.val_inv_logOrderIso_symm_apply, OrderIso.sumLexAssoc_apply_inl_inr, DomAddAct.isQuotientMap_mk, comp_equiv_symm_dotProduct, Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul, UniqueFactorizationMonoid.normalizedFactorsEquiv_apply, toAdd_list_sum, MonoidAlgebra.lift_single, UniformOnFun.zero_apply, CategoryTheory.Limits.Multifork.toSections_fac, equivShrink_symm_neg, WithCStarModule.equiv_symm_zero, Finset.orderIsoColex_apply, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv_naturality_three, Order.height_toDual, WithTop.toDual_apply_coe, SimpleGraph.locallyLinear_comap, finFunctionFinEquiv_symm_apply_val, UniformOnFun.toFun_zero, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map, Equiv.ofFiberEquiv_symm_apply, finSuccEquiv'_symm_some_above, Module.Basis.orientation_reindex, Finset.Colex.insert_lt_insert, Metric.Snowflaking.image_toSnowflaking_emetricBall, IndexedPartition.equivQuotient_index, SimpleGraph.Iso.mapEdgeSet_symm_apply, toAdd_inv, Finset.Ico_toDual, ComplexShape.Embedding.AreComplementary.desc.aux_trans, Antivary.dual, Metric.Snowflaking.ediam_image_toSnowflaking, ConcaveOn.dual, ofBoolAlg_compl, Equiv.congr_arg, AddSubmonoid.toSubmonoid'_closure, SSet.Subcomplex.PairingCore.pairing_p_symm_equivI, MonoidHom.coe_toAdditive', strictAnti_comp_ofDual_iff, Algebra.PreSubmersivePresentation.reindex_map, Finsupp.Lex.lt_iff_of_unique, Sum.Lex.toLex_mono, MonoidHom.coe_toAdditive_ker, AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, CategoryTheory.Cat.Hom.equivFunctor_symm_apply, RootPairing.root_reflectionPerm, DomAddAct.comap_mk_nhds, RingHom.equivRatAlgHom_symm_apply, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, WithTop.coe_toDualBotEquiv, GradedRing.proj_apply, Equiv.Set.sumCompl_symm_apply_of_notMem, Finsupp.DegLex.single_strictAnti, finSuccEquivLast_symm_some, Equiv.Perm.set_support_symm_eq, RootPairing.Equiv.indexEquiv_inv, MvPolynomial.mapEquivMonic_symm_map, Equiv.toFun_inducedStructureEquiv_Symm, toColex_smul', CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, Quaternion.norm_toLp_equivTuple, Equiv.boolProdNatEquivNat_apply, CategoryTheory.CartesianMonoidalCategory.homEquivToProd_symm_apply, DomAddAct.symm_mk_zero, Set.Definable.image_comp_equiv, DomMulAct.mk_smul_mk_aeeqFun, WithLp.equiv_symm_apply_ofLp, DegLex.exists_iff, Matrix.trace_fin_two_of, toBoolAlg_mul, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_one, equivShrink_symm_smul, SSet.stdSimplex.face_singleton_compl, Equiv.subLeft_involutive, CategoryTheory.Functor.partialRightAdjointHomEquiv_map_comp, Matrix.compAddEquiv_symm_apply, Fintype.finsetEquivSet_symm_apply, Fin.snocEquiv_symm_apply, Finset.sigmaAntidiagonalEquivProd_apply, Nat.equivProdNatSmoothNumbers_apply, Finsupp.domLCongr_single, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, FirstOrder.Language.Formula.realize_equivSentence_symm, Equiv.ofPreimageEquiv_symm_apply, WithBot.map_toDual, ContinuousAlternatingMap.ofSubsingleton_symm_apply_apply, Pi.toLex_strictMono, equivShrink_bot, FirstOrder.Language.Formula.realize_equivSentence, Topology.WithGeneratedByTopology.isClosed_iff, Minimal.dual, finSuccEquiv'_last_apply_castSucc, FreeGroup.map_eq_lift, StrictAntiOn.dual_right, NonemptyInterval.toLex_le_toLex, FreeGroup.lift_of_apply, Finset.sigmaAntidiagonalEquivProd_symm_apply_fst, Multiplicative.ofAdd_image_nsmul, CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_symm_apply, finSumNatEquiv_apply_right, Subgroup.IsComplement.quotientGroupMk_leftQuotientEquiv, Finset.Colex.ofColex_bot, AddSubmonoid.equivOp_symm_apply_coe, CategoryTheory.Equivalence.inducedFunctorOfEquiv, RootPairing.equiv_of_mapsTo_symm_apply, isOpenMap_toDual, Sym2.lift_map_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, ofLex_zero, AddSubgroup.IsComplement.leftQuotientEquiv_apply, ArchimedeanClass.FiniteElement.ext_iff, Trunc.finChoiceEquiv_apply, MulEquiv.symmEquiv_apply_symm_apply, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', Matrix.compAddEquiv_apply, MultilinearMap.ofSubsingletonₗ_symm_apply, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual, Additive.mem_toAddSubgroup, UniversalEnvelopingAlgebra.lift_ι_apply', CategoryTheory.shrinkYonedaEquiv_symm_map, uniformContinuous_toAdd, CategoryTheory.Sieve.overEquiv_iff, addMonoidEndToMultiplicative_symm_apply_apply, Equiv.toIso_inv, SymAlg.unsym_one, WithOne.lift_unique, Filter.comap_equiv_symm, Submonoid.closure_eq_mrange, Monoid.PushoutI.NormalWord.cons_toList, CategoryTheory.map_coyonedaEquiv, CategoryTheory.Adjunction.homEquiv_symm_apply, AddEquiv.toMultiplicativeLeft_apply_apply, RingQuot.eq_liftAlgHom_comp_mkAlgHom, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, CategoryTheory.Functor.Initial.limitConeOfComp_isLimit, GradedRing.proj_recompose, AddEquiv.op_apply_symm_apply, Equiv.Perm.decomposeFin_symm_apply_zero, OrderDual.toDual_ofDual, LocallyConstant.congrLeft_apply, MultilinearMap.ofSubsingleton_apply_apply, toDegLex_add, SimpleGraph.Iso.map_apply, AlgebraicGeometry.Spec.homEquiv_symm_apply, SimpleGraph.Iso.comap_symm_apply, Finsupp.Colex.single_strictMono, DyckWord.equivTree_apply, SetTheory.PGame.toRightMovesNim_symm_lt, DomMulAct.mk_smul_addMonoidHom_apply, SymAlg.mul_def, isRegular_ofColex, QuaternionAlgebra.coe_symm_addEquivTuple, CategoryTheory.map_yonedaEquiv', DFinsupp.sigmaFinsetFunEquiv_apply_fst, Pi.toColex_update_lt_self_iff, nhds_toMul, AddChar.coe_toMonoidHomEquiv_symm, LinearIsometryEquiv.coe_prodAssoc, hahnEmbedding_isOrderedAddMonoid, CategoryTheory.CategoryOfElements.toCostructuredArrow_map, toDual_one, FreeAddGroup.range_lift_eq_closure, Finset.Iio_ofDual, Multiplicative.toAdd_top, DFinsupp.Lex.lt_iff, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, CategoryTheory.Functor.homEquivOfIsLeftKanExtension_apply_app, Pi.basisFun_det_apply, Shrink.algEquiv_symm_apply, Int.divModEquiv_symm_apply, Topology.WithLower.ofLower_toLower, toLex_neg, Order.coheight_toDual, AddCommGrpCat.toCommGrp_map, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, UniformFun.ofFun_mul, Ideal.IsHomogeneous.mem_iff, Finset.Ici_ofDual, Sum.Lex.not_inr_lt_inl, DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def, Matrix.blockTriangular_reindex_iff, Abelianization.equivOfComm_symm_apply, Matrix.isUnit_comp_symm_iff, Equiv.eq_symm_apply, RingEquiv.prodCongr_symm_apply, CategoryTheory.Bicategory.mateEquiv_apply', nsmulCoprime_apply, UniformOnFun.lipschitzWith_one_ofFun_toFun', Equiv.setSubtypeComm_symm_apply, CategoryTheory.nerve.edgeMk_surjective, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.comp_homEquiv_symm_assoc, DomAddAct.isInducing_mk_symm, ContinuousMultilinearMap.norm_ofSubsingleton_id, CategoryTheory.Over.postAdjunctionLeft_counit_app_left, FreeAddMonoid.toList_nil, Set.opEquiv_symm_apply, CategoryTheory.Localization.SmallShiftedHom.postcompEquiv_apply, Complex.equivRealProd_apply_le, CategoryTheory.Adjunction.equivHomsetRightOfNatIso_symm_apply, Topology.WithLowerSet.toLowerSet_specializes_toLowerSet, QuotientAddGroup.equivIocMod_coe, CategoryTheory.Bicategory.conjugateEquiv_comp, Equiv.Perm.inv_trans_self, Fin.insertNth_apply_cycleRange_symm, isLeftRegular_toColex, Finsupp.lcongr_apply_apply, TopHom.dual_id, CategoryTheory.Limits.Sigma.ι_reindex_inv_assoc, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm, CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_three_assoc, HahnSeries.leadingCoeff_abs, CategoryTheory.Limits.Types.colimitEquivColimitType_apply, SemidirectProduct.equivProd_symm_apply_right, Topology.WithUpperSet.isOpen_ofUpperSet_preimage, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, SymAlg.unsym_inj, Equiv.sumCompl_symm_apply_of_pos, Subsemigroup.coe_toAddSubsemigroup_apply, IsMaxFilter.dual, Delone.DeloneSet.mapIsometry_apply_carrier, Equiv.some_removeNone_iff, OnePoint.equivProjectivization_apply_infinity, Multiplicative.ofAdd_top, CategoryTheory.Equivalence.essSurjInducedFunctor, isOpenMap_toMul, CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map, CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit, measurable_piEquivPiSubtypeProd, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, Finsupp.equivFunOnFinite_symm_apply_apply, Algebra.Generators.Hom.equivAlgHom_apply_coe, circleEquivGen_apply, ZLattice.covolume_eq_det, coe_ofLexLinearEquiv, SetTheory.PGame.toLeftMovesNim_one_symm, equivShrink_sub, Equiv.listUniqueEquiv_symm_apply, InfIrred.ofDual, MulArchimedeanOrder.val_of, MultilinearMap.domDomCongr_apply, ofDual_smul', HahnModule.of_symm_sub, CategoryTheory.ShiftedHom.opEquiv'_add_symm, uniformEquicontinuous_iff_uniformContinuous, FreeSemigroup.lift_of, MonoidAlgebra.lift_of, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, CStarMatrix.toCLM_apply_single_apply, Set.Ico_ofDual, CategoryTheory.Functor.functorHomEquiv_symm_apply_app_app, MonoidHom.coe_toMultiplicative_ker, nndist_ofDual, WithBot.orderIsoPUnitSumLex_bot, Equiv.piCongrLeft'_apply, Finset.toDual_sup', Metric.Snowflaking.homeomorph_apply, CategoryTheory.colimitYonedaHomEquiv_π_apply, MulEquiv.withZero_symm_apply_symm_apply, CategoryTheory.Equivalence.induced_counitIso, UniformFun.isClosed_setOf_continuous, Set.powersetCard.ofFinEmbEquiv_apply, AddChar.coe_toAddMonoidHomEquiv_symm, AddSubgroup.equivOp_symm_apply_coe, BoundedContinuousFunction.isInducing_coeFn, OrderDual.ofDual_top, IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero, OrderIso.dualDual_symm_apply, PowerBasis.liftEquiv_apply_coe, invertibleEquivOfLeftInverse_symm_apply, CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply, Set.PartiallyWellOrderedOn.ProdLex_iff, DFinsupp.domLCongr_apply, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', CategoryTheory.uliftCoyonedaEquiv_comp, CategoryTheory.Quiv.equivOfIso_apply, RootPairing.Hom.id_indexEquiv_symm_apply, CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, Equiv.pprodEquivProd_symm_apply, MeasurableEquiv.piFinSuccAbove_symm_apply, Prod.Lex.le_iff', Fin2.equivFin_symm_apply, CategoryTheory.CatEnrichedOrdinary.Hom.base_id, CategoryTheory.yonedaEquiv_symm_app_apply, hahnEmbedding_isOrderedModule, MulEquiv.piMultiplicative_symm_apply, AntitoneOn.dual, MvPolynomial.renameSymmetricSubalgebra_apply_coe, FreeNonUnitalNonAssocAlgebra.lift_comp_of, Equiv.divRight₀_apply, CategoryTheory.Arrow.equivSigma_symm_apply_right, sInfHom.symm_dual_id, ofMul_uzpow, UniformFun.ofFun_inv, CategoryTheory.tensorLeftHomEquiv_symm_naturality, DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe, CategoryTheory.nerve.homEquiv_symm_apply, Sum.Lex.inl_le_inr, WithBot.ofDual_apply_bot, Set.mem_image_equiv, Algebra.discr_reindex, MeasurableEquiv.piFinSuccAbove_apply, AddMonoid.Coprod.con_neg_add_cancel, MvPolynomial.coe_mapEquivMonic_comp, Matrix.comp_one, Topology.WithLawson.toLawson_ofLawson, Ordinal.toPGame_moveLeft', SheafOfModules.unitHomEquiv_apply_coe, stdSimplexEquivIcc_zero, uniformity_additive, SymAlg.unsym_eq_zero_iff, Matrix.conjTranspose_reindex, CategoryTheory.mateEquiv_apply, ComplexShape.Embedding.AreComplementary.desc'_inr, continuous_ofAdd, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, CategoryTheory.Limits.IsLimit.homEquiv_apply, Function.Embedding.optionEmbeddingEquiv_apply_fst, CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc, LocallyConstant.congrRight_symm_apply, CategoryTheory.ShiftedHom.opEquiv_symm_comp, SupHom.dual_apply_toFun, UniformFun.lipschitzWith_eval, CompactlySupportedContinuousMap.continuousMapEquiv_apply_toFun, OrderDual.ofDual_eq_bot, SkewMonoidAlgebra.lift_symm_apply, CategoryTheory.Adjunction.homEquiv_naturality_left_square_assoc, RingHom.asBoolAlg_toFun, AddEquiv.op_apply_apply, AffineEquiv.constVAddHom_apply, CategoryTheory.Limits.compYonedaSectionsEquiv_symm_apply_coe, Sum.Lex.inl_le_inl_iff, Equiv.piCongrSet_symm_apply, MonoidAlgebra.lift_unique', CategoryTheory.yonedaEquiv_comp, Equiv.apply_eq_iff_eq_symm_apply, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, CategoryTheory.unitCompPartialBijective_symm_apply, RootPairing.reflectionPerm_eq_iff_smul_coroot, Ordinal.type_preimage, ofMul_div, Function.fromTypes_nil_equiv_symm_apply, MeasureTheory.SignedMeasure.toJordanDecompositionEquiv_symm_apply, uliftZMultiplesHom_symm_apply, Metric.Snowflaking.isBounded_image_toSnowflaking_iff, CategoryTheory.Localization.structuredArrowEquiv_apply, LieAlgebra.of_nsmul, Pi.toLex_monotone, SetTheory.PGame.moveLeft_neg, Equiv.psigmaEquivSigma_symm_apply bridge: CategoryTheory.Limits.WalkingPair.equivBool_apply_right, CategoryTheory.Limits.WalkingPair.equivBool_apply_left

---

← Back to Index