mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A.eq_1 : ∀ (n : ℕ), CartanMatrix.A n = Matrix.of fun i j => if i = j then 2 else if ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i then -1 else 0
-- Mathlib.Analysis.Fourier.AddCircle
/-- For a function on `ℝ`, the Fourier coefficients of `f` on `[a, b]` are defined as the
Fourier coefficients of the unique periodic function agreeing with `f` on `Ioc a b`.  -/
fourierCoeffOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → {a b : ℝ} → a < b → (ℝ → E) → ℤ → E
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M},
  BddBelow s → BddBelow t → BddBelow (s + t)
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
ZMod.eisenstein_lemma_aux : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [Fact (p % 2 = 1)] {a : ℕ},
  a % 2 = 1 →
    ↑a ≠ 0 →
      {x ∈ Finset.Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}.card ≡ ∑ x ∈ Finset.Ico 1 (p / 2).succ, x * a / p [MOD 2]
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.smul_continuousOn : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → 𝕜}
  {g : ℝ → E} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [IsBoundedSMul 𝕜 E],
  IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => f x • g x) μ a b
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.exists_eval₂_eq_zero_of_injective : ∀ {k : Type u} [inst : Field k] {R : Type u_1} [inst_1 : Semiring R] [IsAlgClosed k] (f : R →+* k),
  Function.Injective ⇑f → ∀ (p : Polynomial R), p.degree ≠ 0 → ∃ x, Polynomial.eval₂ f x p = 0
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.add_congr.wr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Add α] [Lean.Grind.ToInt.Add α i],
  i.isFinite = true → ∀ {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = i.wrap b' → ↑(a + b) = i.wrap (a' + b')
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.unitHomEquiv_comp_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M N : SheafOfModules R} (f : SheafOfModules.unit R ⟶ M) (p : M ⟶ N),
  N.unitHomEquiv (CategoryTheory.CategoryStruct.comp f p) = SheafOfModules.sectionsMap p (M.unitHomEquiv f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.starAlgHom_id : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S] [inst_6 : StarRing S]
  [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S] [inst_10 : Ring A]
  [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S] {a : A}
  {φ : C(↑(spectrum S a), S) →⋆ₐ[S] A} {f : C(S, R)} (h : SpectrumRestricts a ⇑f),
  φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a →
    (SpectrumRestricts.starAlgHom φ h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
-- Mathlib.Data.Nat.Factorial.SuperFactorial
_private.Mathlib.Data.Nat.Factorial.SuperFactorial.0.Nat.factorial.match_1.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
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_nil : ∀ {m n : ℤ}, n ≤ m + 1 → (m<...n).toArray = #[]
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkIds : Aesop.MVarClusterRef → Lean.CoreM Unit
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
List.prod_map_le_pow_length₀ : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {F : Type u_2} {L : Type u_3} [inst_4 : FunLike F L R] {f : F} {r : R} {t : List L},
  (∀ x ∈ t, 0 ≤ f x) → (∀ x ∈ t, f x ≤ r) → (List.map (⇑f) t).prod ≤ r ^ t.length
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.norm_eq_one_iff' : ∀ {x : ℂ}, ‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-Real.pi) Real.pi, Complex.exp (↑θ * Complex.I) = x
-- Lean.Level
Lean.instInhabitedLMVarIdMap : {α : Type} → Inhabited (Lean.LMVarIdMap α)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {U : CategoryTheory.Comonad C}
  {c c' : CategoryTheory.Cokleisli U} {x y : c.Hom c'}, x = y ↔ x.of = y.of
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Weekday.Ordinal
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.comp_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G H : CategoryTheory.LaxMonoidalFunctor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : CategoryTheory.Functor C D}
  (h : H.toFunctor ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β).hom h =
    CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp β.hom h)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.isIso_iff_isIso_yoneda_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.yoneda.map f).app (Opposite.op c))
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNegEquiv.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M),
  S.leftNegEquiv hS =
    { toFun := (↑S.fromCommLeftNeg).toFun, invFun := fun x => ⟨↑(-IsAddUnit.addUnit ⋯), ⋯⟩, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.mk.sizeOf_spec : ∀ {X : SSet.Truncated 1} {n : ℕ}
  (vertex : Fin (n + 1) → X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Path₁._proof_1 }))
  (arrow : Fin n → X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Path₁._proof_2 }))
  (arrow_src :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.castSucc)
  (arrow_tgt :
    ∀ (i : Fin n),
      (CategoryTheory.ConcreteCategory.hom
            (X.map
              (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) SSet.Truncated.Path₁._proof_1
                  SSet.Truncated.Path₁._proof_5).op))
          (arrow i) =
        vertex i.succ),
  sizeOf { vertex := vertex, arrow := arrow, arrow_src := arrow_src, arrow_tgt := arrow_tgt } = 1
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt8HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_map : ∀ {α β β₂ γ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β] [inst_1 : Monad n]
  [inst_2 : Std.Internal.Do.Assertion Pred] [inst_3 : Std.Internal.Do.Assertion EPred]
  [inst_4 : Std.Internal.Do.WPMonad n Pred EPred] [Std.Iterators.Finite α Id] [inst_6 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄ forIn it init fun out acc => g (f out) acc ⦃ Q; eQ ⦄ → ⦃ P ⦄ forIn (Std.Iter.map f it) init g ⦃ Q; eQ ⦄
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.foldl.match_1.eq_2 : ∀ {σ : Sort u_3} {α : Type u_1} (motive : σ → RBTree.RBNode.Stream α → Sort u_2) (b : σ) (v : α) (r : RBTree.RBNode α)
  (tail : RBTree.RBNode.Stream α) (h_1 : (b : σ) → motive b RBTree.RBNode.Stream.nil)
  (h_2 :
    (b : σ) →
      (v : α) →
        (r : RBTree.RBNode α) → (tail : RBTree.RBNode.Stream α) → motive b (RBTree.RBNode.Stream.cons v r tail)),
  (match b, RBTree.RBNode.Stream.cons v r tail with
    | b, RBTree.RBNode.Stream.nil => h_1 b
    | b, RBTree.RBNode.Stream.cons v r tail => h_2 b v r tail) =
    h_2 b v r tail
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjObjFinite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C),
  ContinuousSMul (CategoryTheory.Aut (F.obj X)) (F.obj X).obj
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.exists_measurable_nonneg : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : Preorder β]
  [inst_1 : Zero β] {mβ : MeasurableSpace β} {f : α → β},
  AEMeasurable f μ → (∀ᵐ (t : α) ∂μ, 0 ≤ f t) → ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᵐ[μ] g
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.OrderedListType.all : List Lean.Doc.Parser.OrderedListType
-- Mathlib.Condensed.Light.Functors
/-- The functor from `LightProfinite.{u}` to `LightCondSet.{u}` given by the Yoneda sheaf.  -/
lightProfiniteToLightCondSet : CategoryTheory.Functor LightProfinite LightCondSet
-- Aesop.Frontend.RuleExpr
_private.Aesop.Frontend.RuleExpr.0.Aesop.Frontend.RuleExpr.foldBranchesM.go : {σ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [Monad m] → (σ → Aesop.Frontend.Feature → m σ) → σ → Array σ → Aesop.Frontend.RuleExpr → m (Array σ)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.instInhabitedSimpCongrTheorems : Inhabited Lean.Meta.SimpCongrTheorems
-- Mathlib.Data.TypeVec
TypeVec.toSubtype_of_subtype_assoc : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (p : α.Arrow (TypeVec.repeat n Prop))
  (f : β.Arrow (TypeVec.Subtype_ p)), TypeVec.comp (TypeVec.toSubtype p) (TypeVec.comp (TypeVec.ofSubtype p) f) = f
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzWith_iff_norm_sub_le`. -/
LipschitzWith.norm_sub_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {C : NNReal}, LipschitzWith C f → ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.minpoly_eq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial R}
  (h : IsAdjoinRootMonic S f) [IsDomain R] [IsDomain S] [Module.IsTorsionFree R S] [IsIntegrallyClosed R],
  Irreducible f → minpoly R h.root = f
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift_inl : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (fn : N →* H) (fg : G →* H)
  (h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) (n : N),
  (SemidirectProduct.lift fn fg h) (SemidirectProduct.inl n) = fn n
-- Mathlib.ModelTheory.Order
FirstOrder.Language.model_partialOrder : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : PartialOrder M]
  [L.OrderedStructure M], M ⊨ L.partialOrderTheory
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.sum_map_app : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₀}
  {D : J → Type u₁} [inst_1 : (j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] {X X' : (i : I) → C i} (f : X ⟶ X')
  (Y : (j : J) → D j) (s : I ⊕ J),
  ((CategoryTheory.Pi.sum C).map f).app Y s =
    match s with
    | Sum.inl i => f i
    | Sum.inr j => CategoryTheory.CategoryStruct.id (Y j)
-- Mathlib.Algebra.Category.ModuleCat.InjectiveDimension
ModuleCat.hasInjectiveDimensionLE_iff_of_linearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N)
  (n : ℕ), CategoryTheory.HasInjectiveDimensionLE M n ↔ CategoryTheory.HasInjectiveDimensionLE N n
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- If we have a large enough set of elements in `R^ι`, then there will be a pair
whose remainders are close together. We'll show that all sets of cardinality
at least `cardM bS adm` elements satisfy this condition.

The value of `cardM` is not at all optimal: for specific choices of `R`,
the minimum cardinality can be exponentially smaller.
 -/
ClassGroup.cardM : {R : Type u_1} →
  {S : Type u_2} →
    [inst : EuclideanDomain R] →
      [inst_1 : CommRing S] →
        [IsDomain S] →
          [inst_3 : Algebra R S] →
            {abv : AbsoluteValue R ℤ} →
              {ι : Type u_5} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R S → abv.IsAdmissible → ℕ
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instSub : (R : Type u) → (X : Type v) → [inst : CommRing R] → Sub (FreeLieAlgebra R X)
-- Std.Async.Process
/-- Sets the scheduling priority of a process.
 -/
Std.IO.Process.setPriority : Std.IO.Process.PId → Int64 → IO Unit
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.beqModel : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [(k : α) → BEq (β k)] → List ((a : α) × β a) → List ((a : α) × β a) → Bool
-- Mathlib.Control.Fold
Monoid.foldrM.get : {m : Type u → Type u} → [inst : Monad m] → {α : Type u} → Monoid.foldrM m α → α → m α
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    f 0 = 0 →
      (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
        ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {X Y : CategoryTheory.Center C} {f : X.fst ⟶ Y.fst}
  {comm :
    autoParam
      (∀ (U : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f U) (Y.snd.β U).hom =
          CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f))
      CategoryTheory.Center.Hom.comm._autoParam}
  {f_1 : X.fst ⟶ Y.fst}
  {comm_1 :
    autoParam
      (∀ (U : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f_1 U) (Y.snd.β U).hom =
          CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f_1))
      CategoryTheory.Center.Hom.comm._autoParam},
  { f := f, comm := comm } = { f := f_1, comm := comm_1 } → f = f_1
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.mergeWithGrindAllowed : Std.HashSet Lean.Name
-- Mathlib.Tactic.SuppressCompilation
/-- Replacing `def` and `instance` by `noncomputable def` and `noncomputable instance`, designed
to disable the compiler in a given file or a given section.
This is a hack to work around https://github.com/leanprover-community/mathlib4/issues/7103.  -/
elabSuppressCompilationDecl : Lean.Elab.Command.CommandElab
-- Mathlib.RingTheory.Support
Module.mem_support_mono : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p q : PrimeSpectrum R}, p ≤ q → p ∈ Module.support R M → q ∈ Module.support R M
-- Mathlib.Data.EReal.Operations
EReal.top_mul_coe_of_neg : ∀ {x : ℝ}, x < 0 → ⊤ * ↑x = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImage.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.ImageFactorisation f), CategoryTheory.Limits.HasImage f
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.isPosSemidef_covarianceBilinDual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : BorelSpace E], (ProbabilityTheory.covarianceBilinDual μ).toBilinForm.IsPosSemidef
-- Init.Prelude
Bind.mk : {m : Type u → Type v} → ({α β : Type u} → m α → (α → m β) → m β) → Bind m
-- Mathlib.Data.Nat.Factorization.Induction
induction_on_primes : ∀ {motive : ℕ → Prop},
  motive 0 → motive 1 → (∀ (p a : ℕ), Nat.Prime p → motive a → motive (p * a)) → ∀ (n : ℕ), motive n
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- A 2-truncated simplicial set `S` has an underlying refl quiver `SSet.OneTruncation₂ S`.  -/
SSet.OneTruncation₂.reflQuiver : (S : SSet.Truncated 2) → CategoryTheory.ReflQuiver (SSet.OneTruncation₂ S)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.mk : {α : Type u_6} →
  [toPartialOrder : PartialOrder α] →
    (ωSup : OmegaCompletePartialOrder.Chain α → α) →
      (∀ (c : OmegaCompletePartialOrder.Chain α) (i : ℕ), c i ≤ ωSup c) →
        (∀ (c : OmegaCompletePartialOrder.Chain α) (x : α), (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x) →
          OmegaCompletePartialOrder α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- If the measurable set `A` is norm-stable in the sense that
`normAtAllPlaces⁻¹ (normAtAllPlaces '' A) = A`, then its volume can be computed via an integral
over `normAtAllPlaces '' A`.
 -/
NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral : ∀ {K : Type u_1} [inst : Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)} [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtAllPlaces ⁻¹' NumberField.mixedEmbedding.normAtAllPlaces '' A = A →
    MeasurableSet A →
      MeasureTheory.volume A =
        2 ^ NumberField.InfinitePlace.nrRealPlaces K *
            ENNReal.ofReal (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
          ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in NumberField.mixedEmbedding.normAtAllPlaces '' A,
            ∏ w, ENNReal.ofReal (x ↑w)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.hasRightLiftingProperty_πObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {X Y A B : C} (i : A ⟶ B),
  I i → ∀ (f : X ⟶ Y), CategoryTheory.HasLiftingProperty i (CategoryTheory.SmallObject.πObj I κ f)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.iso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) Q.iso.hom =
      CategoryTheory.CategoryStruct.comp P.iso.hom ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ)
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- `Opens.map f` and `OpenNhds.map f` form a commuting square (up to natural isomorphism)
with the inclusion functors into `Opens X`.  -/
TopologicalSpace.OpenNhds.inclusionMapIso : {X Y : TopCat} →
  (f : X ⟶ Y) →
    (x : ↑X) →
      (TopologicalSpace.OpenNhds.inclusion ((CategoryTheory.ConcreteCategory.hom f) x)).comp
          (TopologicalSpace.Opens.map f) ≅
        (TopologicalSpace.OpenNhds.map f x).comp (TopologicalSpace.OpenNhds.inclusion x)
-- Mathlib.Topology.Separation.Hausdorff
/-- **Local identity principle** for continuous maps: Two continuous maps into a Hausdorff space
agree in a punctured neighborhood of a non-isolated point iff they agree in a neighborhood.  -/
ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {x : X}
  {f g : X → Y},
  ContinuousAt f x → ContinuousAt g x → ∀ [(nhdsWithin x {x}ᶜ).NeBot], f =ᶠ[nhdsWithin x {x}ᶜ] g ↔ f =ᶠ[nhds x] g
-- Std.Internal.Parsec.ByteArray
/-- Parses until a predicate is satisfied (exclusive), up to a given limit.
 -/
Std.Internal.Parsec.ByteArray.takeUntilUpTo : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Mathlib.Algebra.Order.SuccPred
Order.le_one_iff : ∀ {α : Type u_1} {x : α} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α]
  [NeZero 1], x ≤ 1 ↔ x = 0 ∨ x = 1
-- Mathlib.Data.ENNReal.Basic
ENNReal.instLE : LE ENNReal
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.of_inter_subset : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α],
  (∀ ⦃d : Set α⦄,
      d ∈ D →
        d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s) →
    DirSupInaccOn D s
-- Mathlib.Tactic.Linter.HaveLetLinter
/-- a monadic version of `Lean.Elab.InfoTree.foldInfo`.
Used to infer types inside a `CommandElabM`.  -/
_private.Mathlib.Tactic.Linter.HaveLetLinter.0.Mathlib.Linter.haveLet.InfoTree.foldInfoM : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [Monad m] → (Lean.Elab.ContextInfo → Lean.Elab.Info → α → m α) → α → Lean.Elab.InfoTree → m α
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isSuccLimit_of_isPrincipal_add : ∀ {o : Ordinal.{u}}, 1 < o → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o → Order.IsSuccLimit o
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.empty_mulVec : ∀ {α : Type u} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n'] (A : Matrix (Fin 0) n' α)
  (v : n' → α), A.mulVec v = ![]
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- A quiver is an arborescence when there is a unique path from the default vertex
to every other vertex.  -/
Quiver.Arborescence : (V : Type u) → [Quiver V] → Type (max u v)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_const_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {c : β}, MeasureTheory.HasFiniteIntegral (fun x => c) μ ↔ c = 0 ∨ MeasureTheory.IsFiniteMeasure μ
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instSetLike : {K : Type u} → [inst : Field K] → SetLike (ValuationSubring K) K
-- Mathlib.Order.Basic
LT.lt.gt_or_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a < b → ∀ (c : α), a < c ∨ c < b
-- Mathlib.Topology.Algebra.Monoid.FunOnFinite
FunOnFinite.continuous_map : ∀ (M : Type u_1) [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {X : Type u_2} {Y : Type u_3}
  [inst_3 : Finite X] [inst_4 : Finite Y] (f : X → Y), Continuous (FunOnFinite.map f)
-- Mathlib.Analysis.Normed.Group.Constructions
Prod.normedCommGroup.eq_1 : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedCommGroup E] [inst_1 : NormedCommGroup F],
  Prod.normedCommGroup =
    { toNorm := Prod.seminormedGroup.toNorm, toGroup := Prod.seminormedGroup.toGroup, mul_comm := ⋯,
      toPseudoMetricSpace := Prod.seminormedGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_descQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c) {T : C} (φ : S.X₂ ⟶ T),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = φ
-- Aesop.Tracing
Aesop.TraceOption.mk.sizeOf_spec : ∀ (traceClass : Lean.Name) (option : Lean.Option Bool),
  sizeOf { traceClass := traceClass, option := option } = 1 + sizeOf traceClass + sizeOf option