mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.inhabitedThinSkeleton : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [Inhabited C] → Inhabited (CategoryTheory.ThinSkeleton C)
-- Mathlib.Algebra.BigOperators.Finprod
AddMonoidHom.map_finsum_of_injective : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (g : M →+ N),
  Function.Injective ⇑g → ∀ (f : α → M), g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
-- Mathlib.Logic.Basic
exists_exists_and_eq_and : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : α → Prop} {q : β → Prop},
  (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a)
-- Mathlib.Computability.Reduce
ManyOneDegree.of_eq_of : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {β : Type v} [inst_2 : Primcodable β]
  [inst_3 : Inhabited β] {p : α → Prop} {q : β → Prop}, ManyOneDegree.of p = ManyOneDegree.of q ↔ ManyOneEquiv p q
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.sub_nonneg_ae : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddGroup β]
  [inst_1 : LE β] [AddRightMono β] (f g : α → β), 0 ≤ᵐ[μ] g - f ↔ f ≤ᵐ[μ] g
-- Mathlib.Probability.Martingale.Upcrossing
/-- `upperCrossingTime a b f N n` is the first time before time `N`, `f` reaches
above `b` after `f` reached below `a` for the `n - 1`-th time.  -/
MeasureTheory.upperCrossingTime : {Ω : Type u_1} → {ι : Type u_2} → [inst : Preorder ι] → [OrderBot ι] → [InfSet ι] → ℝ → ℝ → (ι → Ω → ℝ) → ι → ℕ → Ω → ι
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Any zero object identifies to the cokernel of a given epimorphisms.  -/
CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (c : CategoryTheory.Limits.CokernelCofork f) →
            CategoryTheory.Epi f → CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Limits.IsColimit c
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.seqToTerm : Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Algebra.Notation.Support
Pi.support_single_subset : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] {i : ι} {a : M},
  Function.support (Pi.single i a) ⊆ {i}
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor'_obj : ∀ {I : Type u_1} {B : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x : CategoryTheory.LocallyDiscrete I),
  F.toPseudofunctor'.obj x = F.obj x.as
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_sub : ∀ {a b : UInt8}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeMapConeInv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D}
  (H : CategoryTheory.Functor D C) [inst_3 : H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)),
  CategoryTheory.Functor.mapConeMapConeInv H c =
    (CategoryTheory.Limits.Cone.functorialityEquivalence F H.asEquivalence).counitIso.app c
-- Mathlib.Data.List.DropRight
List.rtakeWhile_reverse : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.rtakeWhile p l.reverse = (List.takeWhile p l).reverse
-- Mathlib.Order.Monotone.Union
/-- If `f` is strictly antitone both on `s` and `t`, with `s` to the left of `t` and the center
point belonging to both `s` and `t`, then `f` is strictly antitone on `s ∪ t`  -/
StrictAntiOn.union : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {c : α},
  StrictAntiOn f s → StrictAntiOn f t → IsGreatest s c → IsLeast t c → StrictAntiOn f (s ∪ t)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_degree_le_one : ∀ {R : Type u_1} [inst : DivisionSemiring R] {f : Polynomial R}, f.degree ≤ 1 → f.Splits
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Turn a morphism in `SemiNormedGrp` back into a `NormedAddGroupHom`.  -/
SemiNormedGrp.Hom.hom : {M N : SemiNormedGrp} → M.Hom N → NormedAddGroupHom M.carrier N.carrier
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.coeOrderAddMonoidHom_apply : ∀ (M : Type u_2) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (m : M),
  (DivisibleHull.coeOrderAddMonoidHom M) m = ↑m
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.num.sizeOf_spec : ∀ (i : ℕ), sizeOf (Nat.Internal.SOM.Expr.num i) = 1 + sizeOf i
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_ofFn : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {f : (i : ℕ) → α → i < n → β},
  as.mapFinIdx f = Vector.ofFn fun i => f (↑i) as[i] ⋯
-- Mathlib.CategoryTheory.Shift.Induced
/-- When the target category of a functor `F : C ⥤ D` is equipped with
the induced shift, this is the compatibility of `F` with the shifts on
the categories `C` and `D`.  -/
CategoryTheory.Functor.CommShift.ofInduced : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (F : CategoryTheory.Functor C D) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                (s : A → CategoryTheory.Functor D D) →
                  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F) →
                    [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] →
                      [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] → F.CommShift A
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- `ratNorm q`, for a `p`-adic number `q` is the `p`-adic norm of `q`, as rational number.

The lemma `padicNormE.eq_ratNorm` asserts `‖q‖ = ratNorm q`.  -/
Padic.ratNorm : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℚ_[p] → ℚ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- We can turn any colimit cocone over a discrete collection of objects into a bicone.  -/
CategoryTheory.Limits.Bicone.ofColimitCocone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f : J → C} →
          {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} →
            CategoryTheory.Limits.IsColimit t → CategoryTheory.Limits.Bicone f
-- Mathlib.Data.Int.ModEq
Int.modEq_one : ∀ {a b : ℤ}, a ≡ b [ZMOD 1]
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instNontrivialAtPrime : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] (𝒜 : ι → σ) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] [GradedRing 𝒜]
  (𝔭 : Ideal A) [inst_6 : 𝔭.IsPrime], Nontrivial (HomogeneousLocalization.AtPrime 𝒜 𝔭)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {D₁ D₂ : F.DescentData f} →
                (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i) →
                  autoParam
                      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
                        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
                        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom i₁))
                            (D₂.hom q f₁ f₂ ⋯ ⋯) =
                          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
                            ((F.map f₂.op.toLoc).toFunctor.map (hom i₂)))
                      CategoryTheory.Pseudofunctor.DescentData.Hom.comm._autoParam →
                    D₁.Hom D₂
-- Batteries.Data.Stream
_private.Batteries.Data.Stream.0.Std.Stream.drop.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Http.Data.Status
Std.Http.Status.nonAuthoritativeInformation.sizeOf_spec : sizeOf Std.Http.Status.nonAuthoritativeInformation = 1
-- Mathlib.Computability.Encoding
Computability.Encoding.mk : {α : Type u} →
  {Γ : Type v} →
    (encode : α → List Γ) →
      (decode : List Γ → Option α) → (∀ (x : α), decode (encode x) = some x) → Computability.Encoding α Γ
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.finset : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [MeasurableSingletonClass α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Finset α} {f : α → E},
  MeasureTheory.IntegrableOn f (↑s) μ
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.relStructCastSuccEquivMulStruct_symm_apply_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin n}
  (h : SSet.PtSimplex.MulStruct SSet.RelativeMorphism.const f g i),
  (SSet.PtSimplex.relStructCastSuccEquivMulStruct.symm h).map = h.map
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Data.Set.Lattice
Set.iUnion_symmDiff_iUnion_subset : ∀ {α : Type u_1} {ι : Sort u_5} {f g : ι → Set α}, symmDiff (⋃ n, f n) (⋃ n, g n) ⊆ ⋃ n, symmDiff (f n) (g n)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeLimitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (a : α),
  (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- The type of sections which generate a sheaf of modules.  -/
SheafOfModules.GeneratingSections : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Type (max (u + 1) u')
-- Mathlib.Topology.Defs.Sequences
SeqCompactSpace.isSeqCompact_univ : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : SeqCompactSpace X], IsSeqCompact Set.univ
-- Std.Data.DTreeMap.Internal.WF.Defs
_private.Std.Data.DTreeMap.Internal.WF.Defs.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.symm_symm : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  e.symm.symm = e
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toRingCatIso_inv : ∀ {R S : Type u} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S), e.toRingCatIso.inv = RingCat.ofHom ↑e.symm
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category with finite biproducts and finite limits has countable AB4\* if sequential limits are
exact.
 -/
CategoryTheory.CountableAB4Star.of_countableAB5Star : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C] [CategoryTheory.HasExactLimitsOfShape ℕᵒᵖ C]
  [inst_6 : CategoryTheory.Limits.HasCountableProducts C], CategoryTheory.CountableAB4Star C
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff_le_left : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {t : Set α}, s.sdiff t ≤ s
-- Mathlib.Algebra.Ring.Associator
AddMonoidHom.associator.eq_1 : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R],
  AddMonoidHom.associator = AddMonoidHom.mulLeft₃ - AddMonoidHom.mulRight₃
-- Mathlib.Data.Countable.Defs
not_uncountable_iff : ∀ {α : Sort u}, ¬Uncountable α ↔ Countable α
-- Lean.Elab.Tactic.SolveByElim
/-- Allow elaboration of `ApplyRulesConfig` arguments to tactics.

Note: does not generate a `(config := ...)` option due to the fields in the `omit`
clause, which are all function-valued and have no `EvalExpr` instances.
 -/
Lean.Elab.Tactic.SolveByElim.elabApplyRulesConfig : Lean.Syntax →
  optParam Lean.Meta.SolveByElim.ApplyRulesConfig { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.SolveByElim.ApplyRulesConfig
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
separatesPointsOfOpensMeasurableSpaceOfT0Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] [T0Space α],
  MeasurableSpace.SeparatesPoints α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDHashMap.Const.ofList l).getKeyD k fallback = fallback
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearMap.coe_withLpMap : ∀ (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [inst : Semiring K] [inst_1 : Semiring K']
  {σ : K →+* K'} [inst_2 : AddCommGroup V] [inst_3 : Module K V] [inst_4 : AddCommGroup V'] [inst_5 : Module K' V']
  (f : V →ₛₗ[σ] V'), ⇑(LinearMap.withLpMap p f) = WithLp.map p ⇑f
-- Mathlib.Analysis.Convex.Intrinsic
AffineIsometry.intrinsicFrontier_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : MetricSpace P] [inst_6 : PseudoMetricSpace Q] [inst_7 : NormedAddTorsor V P]
  [inst_8 : NormedAddTorsor W Q] (φ : P →ᵃⁱ[𝕜] Q) (s : Set P),
  intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.srange_eq_map : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
  NonUnitalRingHom.srange f = NonUnitalSubsemiring.map f ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ [Inhabited α] {k : α} {f : β → β} (hc : (Std.DHashMap.Internal.Raw₀.Const.modify m k f).contains k = true),
      (Std.DHashMap.Internal.Raw₀.Const.modify m k f).getKey k hc = k
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.addZeroNeOne : Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Std.Time.Format.DateFormat
/-- Locale-specific symbols used for formatting and parsing text fields.
 -/
Std.Time.DateFormat.symbols : Std.Time.DateFormat → Std.Time.DateFormatSymbols
-- Init.Data.Nat.Basic
Nat.succ_mul : ∀ (n m : ℕ), n.succ * m = n * m + m
-- Mathlib.Order.Category.LinOrd
/-- Turn a morphism in `LinOrd` back into a `OrderHom`.  -/
LinOrd.Hom.hom : {X Y : LinOrd} → X.Hom Y → ↑X →o ↑Y
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A P : C} {p₀ p₁ : P ⟶ A} {ι : A ⟶ P}
  {ι_p₀ :
    autoParam (CategoryTheory.CategoryStruct.comp ι p₀ = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₀._autoParam}
  {ι_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp ι p₁ = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₁._autoParam}
  {P_1 : C} {p₀_1 p₁_1 : P_1 ⟶ A} {ι_1 : A ⟶ P_1}
  {ι_p₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι_1 p₀_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₀._autoParam}
  {ι_p₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι_1 p₁_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₁._autoParam},
  { P := P, p₀ := p₀, p₁ := p₁, ι := ι, ι_p₀ := ι_p₀, ι_p₁ := ι_p₁ } =
      { P := P_1, p₀ := p₀_1, p₁ := p₁_1, ι := ι_1, ι_p₀ := ι_p₀_1, ι_p₁ := ι_p₁_1 } →
    P = P_1 ∧ p₀ ≍ p₀_1 ∧ p₁ ≍ p₁_1 ∧ ι ≍ ι_1
-- Mathlib.Computability.Primrec.List
/-- `List.takeWhile` is primitive recursive.  -/
Primrec.list_takeWhile : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Bool}, Primrec p → Primrec (List.takeWhile p)
-- Mathlib.ModelTheory.LanguageMap
/-- The composition of two language homomorphisms.  -/
FirstOrder.Language.LHom.comp : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} → {L'' : FirstOrder.Language} → (L' →ᴸ L'') → (L →ᴸ L') → (L →ᴸ L'')
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor `F` preserves finite products if it preserves all from `Discrete J` for `Fintype J`.
We require this for `J = Fin n` in the definition,
then generalize to `J : Type u` in the instance.  -/
CategoryTheory.Limits.PreservesFiniteCoproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRight_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (X : CategoryTheory.Functor E C),
  e.congrRight.unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp X.rightUnitor.inv
      (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.hom) (X.associator e.functor e.inverse).hom)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.coe_inf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M}, ↑(p ⊓ q) = ↑p ∩ ↑q
-- Init.Data.SInt.Bitwise
Int16.toInt32_and : ∀ (a b : Int16), (a &&& b).toInt32 = a.toInt32 &&& b.toInt32
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.eq_1 : ∀ (n : ℕ), SSet.boundary n = { obj := fun x => {s | ¬Function.Surjective ⇑(SSet.stdSimplex.asOrderHom s)}, map := ⋯ }
-- Mathlib.GroupTheory.Index
Subgroup.index_eq_zero_iff_infinite : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 0 ↔ Infinite (G ⧸ H)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_neg : ∀ {R : Type u_1} [inst : Ring R] (p : Polynomial R), (-p).mirror = -p.mirror
-- Mathlib.Data.List.Chain
List.IsChain.isChain_cons : ∀ {α : Type u_3} {R : α → α → Prop} {l : List α} {v : α},
  List.IsChain R l → (∀ (lne : l ≠ []), R v (l.head lne)) → List.IsChain R (v :: l)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- A set `S` of labels supports machine `M` if all the `goto`
statements in the functions in `S` refer only to other functions
in `S`.  -/
Turing.TM1.Supports : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → [Inhabited Λ] → (Λ → Turing.TM1.Stmt Γ Λ σ) → Finset Λ → Prop
-- Mathlib.SetTheory.Lists
Lists'.instInhabited : {α : Type u_1} → [Inhabited α] → (b : Bool) → Inhabited (Lists' α b)
-- Mathlib.Data.Set.Lattice
Set.biInter_and : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι → Prop) (q : ι → ι' → Prop)
  (s : (x : ι) → (y : ι') → p x ∧ q x y → Set α),
  ⋂ x, ⋂ y, ⋂ (h : p x ∧ q x y), s x y h = ⋂ x, ⋂ (hx : p x), ⋂ y, ⋂ (hy : q x y), s x y ⋯
-- Mathlib.Combinatorics.Quiver.Covering
/-- Constructor for `Quiver.Costar`. Defined to be `Sigma.mk`.  -/
Quiver.Costar.mk : {U : Type u_1} → [inst : Quiver U] → {u v : U} → (u ⟶ v) → Quiver.Costar v
-- Mathlib.CategoryTheory.ObjectProperty.Comma
CategoryTheory.ObjectProperty.instSmallCommaCommaOfLocallySmall : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (P₁ : CategoryTheory.ObjectProperty C₁)
  (P₂ : CategoryTheory.ObjectProperty C₂) [CategoryTheory.ObjectProperty.Small.{w, v_1, u_1} P₁]
  [CategoryTheory.ObjectProperty.Small.{w, v_2, u_2} P₂] [CategoryTheory.LocallySmall.{w, v_3, u_3} D],
  CategoryTheory.ObjectProperty.Small.{w, max v_1 v_2, max (max u_1 u_2) v_3}
    (CategoryTheory.ObjectProperty.comma F₁ F₂ P₁ P₂)
-- Mathlib.Analysis.SpecificLimits.Normed
summable_norm_pow_mul_geometric_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] (k : ℕ) {r : R}, ‖r‖ < 1 → Summable fun n => ‖↑n ^ k * r ^ n‖
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.infsep_of_nontrivial : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} (hsf : s.Finite) (hs : s.Nontrivial),
  s.infsep = ⋯.toFinset.inf' ⋯ (Function.uncurry dist)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.mk_apply_of_mem : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {s : Finset ι}
  {f : (i : ↑↑s) → β ↑i} {n : ι} (hn : n ∈ s), ((DirectSum.mk β s) f) n = f ⟨n, hn⟩
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  CategoryTheory.Subfunctor.range (CategoryTheory.CategoryStruct.id F) = ⊤
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instMonoδ : ∀ {n : ℕ} {i : Fin (n + 2)}, CategoryTheory.Mono (SimplexCategory.δ i)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow : ∀ {k : ℕ},
  3 ≤ k →
    Even k →
      ∀ (z : UpperHalfPlane),
        ∑' (v : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) v z =
          2 * riemannZeta ↑k +
            2 * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) *
              ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Inv` across an `Equiv`  -/
Equiv.Inv : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Inv β] → Inv α
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.ι`.

---

The embedding of the category of `κ`-directed
partially ordered types in the category of partially
ordered types.  -/
CategoryTheory.CardinalFilteredPoset.ι : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] → CategoryTheory.Functor (CategoryTheory.CardinalDirectedPoset κ) PartOrdEmb
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoGT_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (x : α), e.toRelIsoGT x = e x
-- Mathlib.RingTheory.Fintype
orderOf_lt_card : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] [Nontrivial M₀] [Finite M₀] (a : M₀), orderOf a < Nat.card M₀
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) '' Set.Ico b c = Set.Ico (b / a) (c / a)