mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- If `‖φ‖` is eventually bounded by `c`, and `u =ᶠ[l] φ * v`, then we have `IsBigOWith c u v l`.
This does not require any assumptions on `c`, which is why we keep this version along with
`IsBigOWith_iff_exists_eq_mul`.  -/
Asymptotics.isBigOWith_of_eq_mul : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {c : ℝ} {l : Filter α} {u v : α → R} (φ : α → R),
  (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) → u =ᶠ[l] φ * v → Asymptotics.IsBigOWith c l u v
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- Sum of a list of elements in an `AddSubgroup` is in the `AddSubgroup`.  -/
AddSubgroup.list_sum_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {l : List G}, (∀ x ∈ l, x ∈ K) → l.sum ∈ K
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_id : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ),
  CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap ⋯ = CategoryTheory.CategoryStruct.id D.top
-- Mathlib.Data.Fintype.Card
Fintype.card_prop : Fintype.card Prop = 2
-- Mathlib.Data.UInt
/-- To use this instance, use `open scoped UInt8.CommRing`.

See the module docstring for an explanation -/
UInt8.instCommRing : CommRing UInt8
-- Mathlib.Topology.Order.LiminfLimsup
Monotone.liminf_nhdsLT_eq_iSup₂_of_exists_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β},
  Monotone f → ∀ (a : α), (∃ b, b < a) → Filter.liminf f (nhdsWithin a (Set.Iio a)) = ⨆ r, ⨆ (_ : r < a), f r
-- Mathlib.Data.W.Basic
/-- Given `β : α → Type*`, `WType β` is the type of finitely branching trees where nodes are labeled by
elements of `α` and the children of a node labeled `a` are indexed by elements of `β a`.
 -/
WType : {α : Type u_1} → (α → Type u_2) → Type (max u_1 u_2)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a positive constant, `fun x ↦ r * f x` tends to infinity along a filter
if and only if `f` tends to infinity along the same filter.  -/
Filter.tendsto_const_mul_atTop_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
-- ProofWidgets.Component.PenroseDiagram
/-- Add an instruction `i` to the substance program.  -/
ProofWidgets.Penrose.DiagramBuilderM.addInstruction : String → ProofWidgets.Penrose.DiagramBuilderM Unit
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.inclusionPathAux.eq_2 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x b : B) (p : Quiver.Path a b) (f : b ⟶ x),
  CategoryTheory.FreeBicategory.inclusionPathAux (p.cons f) =
    (CategoryTheory.FreeBicategory.inclusionPathAux p).comp (CategoryTheory.FreeBicategory.Hom.of f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_insertManyIfNew! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β}
  (h : t.Balanced), ↑(t.insertMany l h) = ↑(t.insertMany! l)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (self : CategoryTheory.CommMon C), CategoryTheory.IsCommMonObj self.X
-- Mathlib.Order.Comparable
IncompRel.not_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], IncompRel (fun x1 x2 => x1 ≤ x2) a b → ¬a < b
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.Arrow C)
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.left)]
  [inst_4 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight X₃.right)]
  [inst_5 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.left)]
  [inst_6 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₂.hom X₃.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂.left X₃.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft X₁.right)],
  CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator X₁ X₂ X₃ =
    CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.associator X₁ X₂ X₃
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Limits.HasPullbacks (CategoryTheory.Limits.FormalCoproduct C)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- The `R`-linear equivalence between additive morphisms `A →+ B` and `ℕ`-linear morphisms `A →ₗ[ℕ] B`.
 -/
addMonoidHomLequivNat : {A : Type u_9} →
  {B : Type u_10} →
    (R : Type u_11) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid A] → [inst_2 : AddCommMonoid B] → [inst_3 : Module R B] → (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β] {f : Option β → Option β},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.alter m k f) k = (f (Std.ExtDHashMap.Const.get? m k)).get!
-- Mathlib.Algebra.Homology.Embedding.Restriction
ComplexShape.Embedding.restrictionFunctor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : e.IsRelIff]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : HomologicalComplex C c'} (φ : X ⟶ Y),
  (e.restrictionFunctor C).map φ = HomologicalComplex.restrictionMap φ e
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The type of bounded continuous functions, with the uniform distance, is a pseudometric space.  -/
BoundedContinuousFunction.instPseudoMetricSpace : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → PseudoMetricSpace (BoundedContinuousFunction α β)
-- Std.Data.DTreeMap.Internal.Balancing
/-- Rebalances a tree after at most one element was added to the right subtree. Uses balancing
information to show that some cases are impossible.
 -/
Std.DTreeMap.Internal.Impl.balanceR : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size → Std.DTreeMap.Internal.Impl α β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.w_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X),
  CategoryTheory.CategoryStruct.comp (F.map (φ.fst.app x)) (S'.iso.hom.app x) =
    CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (G.map (φ.snd.app x))
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instFinite_1 : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {S : Type u_3}
  [inst_2 : Ring S] [inst_3 : Module R S] (v : Valuation S Γ₀) [Module.Finite R S], Module.Finite R (WithVal v)
-- Lean.Attributes
Lean.AttributeImpl.toAttributeImplCore : Lean.AttributeImpl → Lean.AttributeImplCore
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap.eq_1 : ∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : DivisionRing β] (a : α),
  LinearOrderedField.cutMap β a = Rat.cast '' {t | ↑t < a}
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeForwardRule.injEq : ∀ (r₁ : Aesop.ForwardRule) (r₂ : Aesop.UnsafeRule) (r₁_1 : Aesop.ForwardRule) (r₂_1 : Aesop.UnsafeRule),
  (Aesop.BaseRuleSetMember.unsafeForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.unsafeForwardRule r₁_1 r₂_1) =
    (r₁ = r₁_1 ∧ r₂ = r₂_1)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [IsDomain R] {P : Ideal R} [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [Module.IsTorsionFree R S] [IsDomain S] [inst_6 : P.IsPrime],
  Module.IsTorsionFree (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry.mk.inj : ∀ {name : Lean.Name} {info : Lean.Meta.MatcherInfo} {name_1 : Lean.Name} {info_1 : Lean.Meta.MatcherInfo},
  { name := name, info := info } = { name := name_1, info := info_1 } → name = name_1 ∧ info = info_1
-- Mathlib.Data.List.Lex
List.Lex.decidableRel : {α : Type u} → [DecidableEq α] → (r : α → α → Prop) → [DecidableRel r] → DecidableRel (List.Lex r)
-- Mathlib.Topology.Order.AtTopBotIxx
map_coe_atBot_of_Ioo_subset : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {a : X},
  s ⊆ Set.Ioi a →
    (∀ b' > a, ∃ b > a, Set.Ioo a b ⊆ s) →
      autoParam (Order.IsPredPrelimit a) map_coe_atBot_of_Ioo_subset._auto_1 →
        Filter.map Subtype.val Filter.atBot = nhdsWithin a (Set.Ioi a)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_sub_left : ∀ {a : ENNReal}, a ≠ ⊤ → Continuous fun x => a - x
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The parallelepiped formed from the standard basis for `ι → ℝ` is `[0,1]^ι`  -/
Module.Basis.parallelepiped_basisFun : ∀ (ι : Type u_1) [inst : Fintype ι], (Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype.eq_2 : ∀ (n_2 : ℕ) (P_2 : Fin (n_2 + 1) → Prop) (inst_2 : DecidablePred P_2) (i_2 : ℕ) (hi : i_2 + 1 < n_2 + 1)
  (hp : P_2 ⟨i_2 + 1, hi⟩),
  Fin.encodeSubtype P_2 ⟨⟨i_2.succ, hi⟩, hp⟩ =
    match Fin.encodeSubtype (fun i => P_2 i.succ) ⟨⟨i_2, ⋯⟩, hp⟩ with
    | ⟨k, hk⟩ =>
      if h0 : P_2 0 then
        have this := ⋯;
        Fin.cast this ⟨k + 1, ⋯⟩
      else
        have this := ⋯;
        Fin.cast this ⟨k, hk⟩
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_C : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} (x : R),
  (AdjoinRoot.mk f) (Polynomial.C x) = (AdjoinRoot.of f) x
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.List.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Reinterpret an affine equivalence as a continuous affine equivalence in finite dimension.  -/
AffineEquiv.toContinuousAffineEquiv : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type w} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                [CompleteSpace 𝕜] →
                  {PE : Type u_1} →
                    {PF : Type u_2} →
                      [inst_6 : MetricSpace PE] →
                        [inst_7 : NormedAddTorsor E PE] →
                          [inst_8 : MetricSpace PF] →
                            [inst_9 : NormedAddTorsor F PF] → [FiniteDimensional 𝕜 E] → (PE ≃ᵃ[𝕜] PF) ≃ (PE ≃ᴬ[𝕜] PF)
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.mk.inj : ∀ {𝕜 : Type u_4} {F : Type u_5} {inst : RCLike 𝕜} {inst_1 : AddCommGroup F} {inst_2 : Module 𝕜 F}
  {toCore : PreInnerProductSpace.Core 𝕜 F} {definite : ∀ (x : F), inner 𝕜 x x = 0 → x = 0}
  {toCore_1 : PreInnerProductSpace.Core 𝕜 F} {definite_1 : ∀ (x : F), inner 𝕜 x x = 0 → x = 0},
  { toCore := toCore, definite := definite } = { toCore := toCore_1, definite := definite_1 } → toCore = toCore_1
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_Ioc_toReal : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  a ≤ b → (MeasureTheory.volume (Set.univ.pi fun i => Set.Ioc (a i) (b i))).toReal = ∏ i, (b i - a i)
-- Mathlib.Topology.Algebra.FilterBasis
/-- A topological additive group with a basis of `𝓝 0` satisfying the axioms of `ModuleFilterBasis`
is a topological module.

This lemma is mathematically useless because one could obtain such a result by applying
`ModuleFilterBasis.continuousSMul` and use the fact that group topologies are characterized
by their neighborhoods of 0 to obtain the `ContinuousSMul` on the pre-existing topology.

But it turns out it's just easier to get it as a byproduct of the proof, so this is just a free
quality-of-life improvement.  -/
ContinuousSMul.of_basis_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {ι : Type u_3} [IsTopologicalRing R] [inst_5 : TopologicalSpace M] [IsTopologicalAddGroup M]
  {p : ι → Prop} {b : ι → Set M},
  (nhds 0).HasBasis p b →
    (∀ {i : ι}, p i → ∃ V ∈ nhds 0, ∃ j, p j ∧ V • b j ⊆ b i) →
      (∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ Set.MapsTo (fun x => x₀ • x) (b j) (b i)) →
        (∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ b i) → ContinuousSMul R M
-- Init.Data.Int.Gcd
Int.lcm_dvd_mul_self_left_iff_dvd_mul : ∀ {k n m : ℕ}, (↑k).lcm ↑n ∣ k * m ↔ n ∣ k * m
-- Mathlib.Data.Finset.Prod
Finset.product_eq_sprod : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, s.product t = s ×ˢ t
-- Init.Data.UInt.Lemmas
USize.ofNat_div : ∀ {a b : ℕ},
  a < 2 ^ System.Platform.numBits →
    b < 2 ^ System.Platform.numBits → USize.ofNat (a / b) = USize.ofNat a / USize.ofNat b
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_π_zero_assoc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁)
  {Z : SSet} (h : (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨0, SSet.horn₃₂.desc.multicofork_π_zero._proof_1⟩) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 0).inv f₀) h
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.shift_comm_assoc : ∀ {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₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A)
  {Z : CategoryTheory.Functor C D} (h : F₂.comp (CategoryTheory.shiftFunctor D a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₂ a).hom h)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryCoproductCocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w))
  (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).ι.app x =
    match x.as with
    | CategoryTheory.Limits.WalkingPair.left => CategoryTheory.FunctorToTypes.coprod.inl
    | CategoryTheory.Limits.WalkingPair.right => CategoryTheory.FunctorToTypes.coprod.inr
-- Mathlib.Data.EReal.Inv
EReal.natCast_div_le : ∀ (m n : ℕ), ↑(m / n) ≤ ↑m / ↑n
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- Note we use `↑i = 0` instead of `i = 0` as `Fin 0` has no `0`.
This means that we cannot state this with `Pi.single` as we did with `Matrix.circulant_single`.  -/
Matrix.Fin.circulant_ite : ∀ (α : Type u_5) [inst : Zero α] [inst_1 : One α] (n : ℕ), (Matrix.circulant fun i => if ↑i = 0 then 1 else 0) = 1
-- Mathlib.Order.Closure
ClosureOperator.instOrderHomClass : ∀ (α : Type u_1) [inst : Preorder α], OrderHomClass (ClosureOperator α) α α
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.functorOfMonoidHom_obj : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  {X : Type u_1} [inst_3 : Monoid X] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T) →* X) (x : G),
  (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f).obj x = ()
-- Mathlib.Topology.UniformSpace.Basic
closure_eq_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] (s : Set (α × α)),
  closure s = ⋂ V ∈ {V | V ∈ uniformity α ∧ SetRel.IsSymm V}, (SetRel.comp V s).comp V
-- Mathlib.Analysis.Complex.Norm
Complex.instNorm : Norm ℂ
-- Mathlib.Algebra.Ring.Hom.Defs
/-- The identity non-unital ring homomorphism from a non-unital semiring to itself.  -/
NonUnitalRingHom.id : (α : Type u_5) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* α
-- Mathlib.Topology.ClusterPt
clusterPt_principal : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {C : Set X},
  ClusterPt x (Filter.principal C) ↔ x ∈ C ∨ AccPt x (Filter.principal C)
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.sub_one_pos : ∀ {p q : ℝ}, p.HolderConjugate q → 0 < p - 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roc : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toArray[i]? = if i < (n - m).toNat then some (m + 1 + ↑i) else none
-- Mathlib.Tactic.NormNum.RealSqrt
/-- `norm_num` extension that evaluates the function `NNReal.sqrt`.  -/
Mathlib.Meta.NormNum.evalNNRealSqrt : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.of_map : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V ↪ V'), (SimpleGraph.map (⇑f) G).IsAcyclic → G.IsAcyclic
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.smul.sizeOf_spec : ∀ {A : Type u} {M : Type v} [inst : SizeOf A] [inst_1 : SizeOf M] (a : A) (m : M),
  sizeOf (Module.Presentation.tautological.R.smul a m) = 1 + sizeOf a + sizeOf m
-- Lean.Environment
/-- Data transmitted by `AddConstAsyncResult.commitConst`.  -/
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal : Type
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_U_eval_one_eq_div : ∀ {𝔽 : Type u_3} [inst : Field 𝔽] [CharZero 𝔽] (n : ℤ) (k : ℕ),
  Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U 𝔽 n)) =
    ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1) / ↑(∏ l ∈ Finset.range k, (2 * l + 3))
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- The inverse to `spine X m`.  -/
SSet.Truncated.StrictSegal.spineToSimplex : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} →
    X.StrictSegal →
      (m : ℕ) →
        (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
          X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h })
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.extension_comp_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] [T0Space β] [CompleteSpace β]
  {f : UniformSpace.Completion α → β},
  UniformContinuous f → UniformSpace.Completion.extension (f ∘ UniformSpace.Completion.coe') = f
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- pullback commutes with composition (up to natural isomorphism).  -/
CategoryTheory.Over.pullbackComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] →
            [inst_2 : CategoryTheory.Limits.HasPullbacksAlong g] →
              CategoryTheory.Over.pullback (CategoryTheory.CategoryStruct.comp f g) ≅
                (CategoryTheory.Over.pullback g).comp (CategoryTheory.Over.pullback f)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.liftMetaTactic1 : (Lean.MVarId → Lean.MetaM (Option Lean.MVarId)) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.coend.condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app j) (CategoryTheory.Limits.Types.coend.ι F j) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j')).map f) (CategoryTheory.Limits.Types.coend.ι F j')
-- Mathlib.Data.Multiset.Pi
/-- `pi m t` constructs the Cartesian product over `t` indexed by `m`.  -/
Multiset.pi : {α : Type u_1} →
  [DecidableEq α] →
    {β : α → Type u_2} → (m : Multiset α) → ((a : α) → Multiset (β a)) → Multiset ((a : α) → a ∈ m → β a)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- Repeated pointwise addition (not the same as pointwise repeated addition!) of a `Set`. See
note [pointwise nat action].  -/
Set.NSMul : {α : Type u_2} → [Zero α] → [Add α] → SMul ℕ (Set α)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_descOpcycles_π_eq_zero_of_boundary : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) [inst_2 : S.HasRightHomology] (x : S.X₃ ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp S.g x),
  CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.descOpcycles k ⋯) = 0
-- Mathlib.Data.Set.Insert
Set.singleton_def : ∀ {α : Type u_1} (a : α), {a} = insert a ∅
-- Init.Data.BitVec.Lemmas
/-- If a bitvec is different than zero, the bit at index `ctz x`, i.e., the first bit after the
trailing zeros, is true.  -/
BitVec.getLsbD_true_ctz_of_ne_zero : ∀ {w : ℕ} {x : BitVec w}, x ≠ 0#w → x.getLsbD x.ctz.toNat = true
-- Lean.Message
Lean.instToMessageDataSyntax : Lean.ToMessageData Lean.Syntax
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ], NeZero (μ Set.univ)