mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate.0.SSet.ιNormalizedChainComplex_eq_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) (x : X.obj (Opposite.op { len := n }))
  (hx : x ∈ X.nonDegenerate n), X.ιNormalizedChainComplex x = CategoryTheory.Limits.Sigma.ι (fun x => R) ⟨x, hx⟩
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.instNormedStarGroup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : StarAddMonoid β]
  [inst_3 : NormedStarGroup β], NormedStarGroup (BoundedContinuousFunction α β)
-- Mathlib.Data.Nat.Log
/-- An auxiliary definition for `Nat.clog`.

For `n > 1`, `b > 1`, `n ≤ b ^ fuel`, returns `(b ^ clog b n / n, clog b n - 1)`.
 -/
Nat.clog.go : ℕ → ℕ → ℕ → ℕ × ℕ
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.isLatticeTheoretic : Lean.Elab.PartialFixpointType → Bool
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The annihilator of a set `H` of units mod `n`: the subgroup of Dirichlet characters
of level `n` that send every element of `H` to `1`.  -/
DirichletCharacter.annihilator : (R : Type u_1) → [inst : CommMonoidWithZero R] → {n : ℕ} → Set (ZMod n)ˣ → Subgroup (DirichletCharacter R n)
-- Batteries.Data.UnionFind.Basic
/-- Root of a union-find node. Returns input if index is out of bounds.  -/
Batteries.UnionFind.rootD : Batteries.UnionFind → ℕ → ℕ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_eq_sInf_lsub : ∀ (o : Ordinal.{u}), o.cof = sInf {a | ∃ ι f, Ordinal.lsub f = o ∧ Cardinal.mk ι = a}
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Sort u_2) (a₂ : α)
  (c₂ sibling : Batteries.PairingHeapImp.Heap α)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil)
  (h_2 :
    (a₂ : α) →
      (c₂ sibling : Batteries.PairingHeapImp.Heap α) →
        motive Batteries.PairingHeapImp.Heap.nil (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling))
  (h_3 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling) Batteries.PairingHeapImp.Heap.nil)
  (h_4 :
    (a₁ : α) →
      (c₁ sibling : Batteries.PairingHeapImp.Heap α) →
        (a₂ : α) →
          (c₂ sibling_1 : Batteries.PairingHeapImp.Heap α) →
            motive (Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling)
              (Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1)),
  (match Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling with
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.nil, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling => h_2 a₂ c₂ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.nil => h_3 a₁ c₁ sibling
    | Batteries.PairingHeapImp.Heap.node a₁ c₁ sibling, Batteries.PairingHeapImp.Heap.node a₂ c₂ sibling_1 =>
      h_4 a₁ c₁ sibling a₂ c₂ sibling_1) =
    h_2 a₂ c₂ sibling
-- Mathlib.Data.Fintype.Card
/-- `card α` is the number of elements in `α`, defined when `α` is a fintype.  -/
Fintype.card : (α : Type u_4) → [Fintype α] → ℕ
-- Mathlib.Order.Partition.Finpartition
/-- The sum of a set-valued function over restricted partition parts equals the sum over original
parts with `f (· ⊓ b)`, provided `f ⊥ = 0` (so bottom terms don't contribute).  -/
Finpartition.sum_restrict : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a b : α} (P : Finpartition a)
  (hb : b ≤ a) {M : Type u_2} [inst_3 : AddCommMonoid M] (f : α → M),
  f ⊥ = 0 → ∑ p ∈ (P.restrict hb).parts, f p = ∑ q ∈ P.parts, f (q ⊓ b)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.natCast_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℕ), (↑n).toProd.1 = ↑n
-- Mathlib.Algebra.Order.Field.Basic
div_le_one_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.ExceptT.bindCont.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.smul_dirac_apply : ∀ {α : Type u_1} (a : ENNReal) (b : α) (s : Set α),
  (a • MeasureTheory.OuterMeasure.dirac b) s = s.indicator (fun x => a) b
-- Init.Data.List.Range
List.zipIdx_eq_nil_iff : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.zipIdx i = [] ↔ l = []
-- Mathlib.GroupTheory.Exponent
/-- **Alias** of the reverse direction of `Monoid.exponent_pos`. -/
Monoid.ExponentExists.exponent_pos : ∀ {G : Type u} [inst : Monoid G], Monoid.ExponentExists G → 0 < Monoid.exponent G
-- Mathlib.Algebra.DirectSum.Module
/-- Linear isomorphism obtained by separating the term of index `none` of a direct sum over
`Option ι`.  -/
DirectSum.lequivProdDirectSum : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {α : Option ι → Type w} →
        [inst_1 : (i : Option ι) → AddCommMonoid (α i)] →
          [inst_2 : (i : Option ι) → Module R (α i)] →
            (DirectSum (Option ι) fun i => α i) ≃ₗ[R] α none × DirectSum ι fun i => α (some i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.ofList l cmp).getKey? k = none
-- Mathlib.CategoryTheory.Sites.Adjunction
/-- An adjunction `adj : G ⊣ F` with `F : D ⥤ E` and `G : E ⥤ D` induces an adjunction
between `Sheaf J D` and `Sheaf J E`, in contexts where one can sheafify `D`-valued presheaves,
and postcomposing with `F` preserves the property of being a sheaf.  -/
CategoryTheory.Sheaf.adjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {E : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
              {F : CategoryTheory.Functor D E} →
                {G : CategoryTheory.Functor E D} →
                  [inst_3 : CategoryTheory.HasWeakSheafify J D] →
                    [inst_4 : J.HasSheafCompose F] →
                      (G ⊣ F) → (CategoryTheory.Sheaf.composeAndSheafify J G ⊣ CategoryTheory.sheafCompose J F)
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.induction_on : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] [Nonempty ι] [IsDirectedOrder ι]
  {C : AddCommGroup.DirectLimit G f → Prop} (z : AddCommGroup.DirectLimit G f),
  (∀ (i : ι) (x : G i), C ((AddCommGroup.DirectLimit.of G f i) x)) → C z
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.centeredArc_zero : Circle.centeredArc 0 = ∅
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousEvalConst.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {X : outParam (Type u_3)} [inst : FunLike F α X]
  [inst_1 : TopologicalSpace F] [inst_2 : TopologicalSpace X],
  (∀ (x : α), Continuous fun f => f x) → ContinuousEvalConst F α X
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.termZ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_div_cancel_right : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α}, IsUnit b → ∀ (a : α), a * b / b = a
-- Mathlib.Data.EReal.Operations
/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the second variable, see `EReal.toENNReal_mul'`.  -/
EReal.toENNReal_mul : ∀ {x y : EReal}, 0 ≤ x → (x * y).toENNReal = x.toENNReal * y.toENNReal
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_iSup_of_directed : ∀ {M : Type u_2} [inst : Add M] {ι : Sort u_3} {S : ι → AddSubsemigroup M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_rpow_funMulInvSnorm_eq_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ},
  0 < p →
    ∀ {f : α → ENNReal},
      ∫⁻ (a : α), f a ^ p ∂μ ≠ 0 → ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤ → ∫⁻ (c : α), ENNReal.funMulInvSnorm f p μ c ^ p ∂μ = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concatRec_concat : ∀ {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1}
  (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
  (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) {u v w : V}
  (p : G.Walk u v) (h : G.Adj v w),
  SimpleGraph.Walk.concatRec Hnil Hconcat (p.concat h) = Hconcat p h (SimpleGraph.Walk.concatRec Hnil Hconcat p)
-- Mathlib.Combinatorics.Schnirelmann
/-- **Alias** of `schnirelmannDensity_setOfPred_modeq_one`. -/
schnirelmannDensity_setOf_modeq_one : ∀ {m : ℕ}, schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_prodMk_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e₀ : E)
  (f₀ : F), HasFDerivAt (fun e => (e, f₀)) (ContinuousLinearMap.inl 𝕜 E F) e₀
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instIsTopologicalAddGroupTangentSpace : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_1} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (_x : M), IsTopologicalAddGroup (TangentSpace I _x)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous chains
$$\dots \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A \to 0$$
which calculates the group homology of `A`.  -/
groupHomology.inhomogeneousChains : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ChainComplex (ModuleCat k) ℕ
-- Mathlib.Analysis.CStarAlgebra.Spectrum
_private.Mathlib.Analysis.CStarAlgebra.Spectrum.0.termσ : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.FoldingRangeParams
-- Mathlib.Dynamics.OmegaLimit
mapsTo_omegaLimit : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (s : Set α) {α' : Type u_5} {β' : Type u_6}
  [inst_1 : TopologicalSpace β'] {f : Filter τ} {ϕ : τ → α → β} {ϕ' : τ → α' → β'} {ga : α → α'} {s' : Set α'},
  Set.MapsTo ga s s' →
    ∀ {gb : β → β'},
      (∀ (t : τ) (x : α), gb (ϕ t x) = ϕ' t (ga x)) →
        Continuous gb → Set.MapsTo gb (omegaLimit f ϕ s) (omegaLimit f ϕ' s')
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isLocalizing_tilde : ∀ {R : CommRingCat} (M : ModuleCat ↑R),
  AlgebraicGeometry.IsLocalizing (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M))
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.arrowCongrSL_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  {H : Type u_8} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_30 : RingHomIsometric σ₁₂]
  [inst_31 : RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : ⋯), ⋯
-- Mathlib.Algebra.Module.ZLattice.Covolume
_private.Mathlib.Algebra.Module.ZLattice.Covolume.0.ZLattice.covolume.frontier_equivFun : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {ι : Type u_2} [inst_2 : Finite ι]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] (b : Module.Basis ι ℝ E)
  (s : Set E), frontier (⇑b.equivFun '' s) = ⇑b.equivFun '' frontier s
-- Mathlib.Algebra.Group.Action.Defs
IsScalarTower.mk : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} [inst : SMul M N] [inst_1 : SMul N α] [inst_2 : SMul M α],
  (∀ (x : M) (y : N) (z : α), (x • y) • z = x • y • z) → IsScalarTower M N α
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_subset_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s t : Set α}, s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.step.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      [inst : Inhabited Γ] →
        (motive : Turing.TM1.Cfg Γ Λ σ → Sort u_4) →
          (x : Turing.TM1.Cfg Γ Λ σ) →
            ((var : σ) → (Tape : Turing.Tape Γ) → motive { l := none, var := var, Tape := Tape }) →
              ((l : Λ) → (v : σ) → (T : Turing.Tape Γ) → motive { l := some l, var := v, Tape := T }) → motive x
-- Lean.Declaration
Lean.RecursorVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (all : List Lean.Name) (numParams numIndices numMotives numMinors : ℕ)
  (rules : List Lean.RecursorRule) (k isUnsafe : Bool) (toConstantVal_1 : Lean.ConstantVal) (all_1 : List Lean.Name)
  (numParams_1 numIndices_1 numMotives_1 numMinors_1 : ℕ) (rules_1 : List Lean.RecursorRule) (k_1 isUnsafe_1 : Bool),
  ({ toConstantVal := toConstantVal, all := all, numParams := numParams, numIndices := numIndices,
        numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe } =
      { toConstantVal := toConstantVal_1, all := all_1, numParams := numParams_1, numIndices := numIndices_1,
        numMotives := numMotives_1, numMinors := numMinors_1, rules := rules_1, k := k_1, isUnsafe := isUnsafe_1 }) =
    (toConstantVal = toConstantVal_1 ∧
      all = all_1 ∧
        numParams = numParams_1 ∧
          numIndices = numIndices_1 ∧
            numMotives = numMotives_1 ∧ numMinors = numMinors_1 ∧ rules = rules_1 ∧ k = k_1 ∧ isUnsafe = isUnsafe_1)
-- Mathlib.Data.Fin.Fin2
Fin2.last.eq_def : ∀ (x : ℕ),
  Fin2.last =
    match x with
    | 0 => Fin2.fz
    | n.succ => Fin2.last.fs
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.mul_lt_one_of_le_of_lt`.  -/
Right.mul_lt_one_of_le_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b : α}, a ≤ 1 → b < 1 → a * b < 1
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
/-- The condition that `P : ObjectProperty C` consists of `κ`-presentable objects
and that any object of `C` is a `κ`-filtered colimit of objects satisfying `P`.
(This notion is particularly relevant when `C` is locally `w`-small and `P` is
essentially `w`-small, see `HasCardinalFilteredGenerators`, which appears in
the definitions of locally presentable and accessible categories.)  -/
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Mathlib.Data.DFinsupp.Defs
/-- `DFinsupp.filter` as an `AddMonoidHom`.  -/
DFinsupp.filterAddMonoidHom : {ι : Type u} →
  (β : ι → Type v) →
    [inst : (i : ι) → AddZeroClass (β i)] → (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i
-- Mathlib.Analysis.LocallyConvex.Basic
absorbs_iff_norm : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
  Absorbs 𝕜 A B ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The identity functor is also the identity on monoid objects.  -/
CategoryTheory.Functor.mapMonIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.Functor.id C).mapMon ≅ CategoryTheory.Functor.id (CategoryTheory.Mon C)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.inr_comp_pushoutSymmetry_hom_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.Limits.pushout g f) Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushoutSymmetry f g).hom Q) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl g f) Q) h
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_smul : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] [inst_4 : DecidableEq α] (p : ENNReal)
  (i : α) (c : 𝕜) (a : E i), lp.single p i (c • a) = c • lp.single p i a
-- Init.Data.List.Count
List.countP_filterMap : ∀ {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → Option β} {l : List α},
  List.countP p (List.filterMap f l) = List.countP (fun a => (Option.map p (f a)).getD false) l
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Constructor for morphisms `X ⟶ Y` between `2`-truncated simplicial sets from
the data of maps on `0`- and `1`-simplices when `Y` is strict Segal.  -/
SSet.Truncated.liftOfStrictSegal : {X Y : SSet.Truncated 2} →
  (f₀ :
      X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
        Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })) →
    (f₁ :
        X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
          Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })) →
      (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
          f₀
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
              (f₁ x)) →
        (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
            f₀
                ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                  x) =
              (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                (f₁ x)) →
          (∀ (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ }))
              (y : Y.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
              f₁
                    ((CategoryTheory.ConcreteCategory.hom
                        (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op))
                      x) =
                  (CategoryTheory.ConcreteCategory.hom
                      (Y.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op))
                    y →
                f₁
                      ((CategoryTheory.ConcreteCategory.hom
                          (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op))
                        x) =
                    (CategoryTheory.ConcreteCategory.hom
                        (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op))
                      y →
                  f₁
                      ((CategoryTheory.ConcreteCategory.hom
                          (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
                        x) =
                    (CategoryTheory.ConcreteCategory.hom
                        (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_12✝ _proof_15✝).op))
                      y) →
            (∀ (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
                f₁
                    ((CategoryTheory.ConcreteCategory.hom
                        (X.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op))
                      x) =
                  (CategoryTheory.ConcreteCategory.hom
                      (Y.map (SimplexCategory.Truncated.σ₂ 0 _proof_13✝ _proof_11✝).op))
                    (f₀ x)) →
              Y.StrictSegal → (X ⟶ Y)
-- Batteries.Tactic.Trans
Batteries.Tactic.TransRelation.app.inj : ∀ {rel rel_1 : Lean.Expr},
  Batteries.Tactic.TransRelation.app rel = Batteries.Tactic.TransRelation.app rel_1 → rel = rel_1
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
/-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m` except `0` and `1`.  -/
strictConvexOn_zpow : ∀ {m : ℤ}, m ≠ 0 → m ≠ 1 → StrictConvexOn ℝ (Set.Ioi 0) fun x => x ^ m
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_ball : ∀ {ι : Type u_1} [inst : Fintype ι] (a : ι → ℝ) {r : ℝ},
  0 < r → MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.eq_inf_of_isPrime_inf : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Finset ι} {f : ι → Ideal R},
  (s.inf f).IsPrime → ∃ i ∈ s, f i = s.inf f
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a : α), UpperSet.Ici a = { carrier := Set.Ici a, upper' := ⋯ }
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.below.superset : ∀ {α : Type u_2} {g : Set (Set α)} {motive : (a : Set α) → Filter.CountableGenerateSets g a → Prop} {s t : Set α}
  (a : Filter.CountableGenerateSets g s) (a_1 : s ⊆ t),
  Filter.CountableGenerateSets.below a → motive s a → Filter.CountableGenerateSets.below ⋯
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus : profiniteToCompHaus.ReflectsEffectiveEpis
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.nnnorm_mk : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (p : E), ‖SeparationQuotient.mk p‖₊ = ‖p‖₊