mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.Nat.Bisect
/-- Given natural numbers `a < b` such that `p a = true` and `p b = false`, `bisect` finds a natural
number `a ≤ c < b` such that `p c = true` and `p (c+1) = false`.
 -/
Nat.bisect : {start stop : ℕ} → {p : ℕ → Bool} → start < stop → p start = true → p stop = false → ℕ
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet_eq_prod_singularValues : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] [inst_6 : FiniteDimensional 𝕜 V] (f : U →ₗ[𝕜] V),
  f.normDet = ∏ i ∈ Finset.range (Module.finrank 𝕜 U), f.singularValues i
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.sSup_apply_le : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] {s : Set (Lex ((i : ι) → (fun i => α i) i))} {i : ι}
  {e : Lex ((i : ι) → (fun i => α i) i)}, (∀ f ∈ s, (∀ j < i, f j = sSup s j) → f i ≤ e i) → sSup s i ≤ e i
-- Mathlib.Util.AtomM.Recurse
/-- the reducibility setting to use when comparing atoms for defeq  -/
Mathlib.Tactic.AtomM.Recurse.Config.red : Mathlib.Tactic.AtomM.Recurse.Config → Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.comp_descToInjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [inst_2 : CategoryTheory.Injective J]
  (hf : CategoryTheory.CategoryStruct.comp S.f f = 0),
  CategoryTheory.CategoryStruct.comp S.g (hS.descToInjective f hf) = f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.mk.injEq : ∀ (position : Lean.Lsp.Position) (label : Lean.Lsp.InlayHintLabel) (kind? : Option Lean.Lsp.InlayHintKind)
  (textEdits? : Option (Array Lean.Lsp.TextEdit)) (tooltip? : Option Lean.Lsp.InlayHintTooltip)
  (paddingLeft? paddingRight? : Option Bool) (data? : Option Lean.Json) (position_1 : Lean.Lsp.Position)
  (label_1 : Lean.Lsp.InlayHintLabel) (kind?_1 : Option Lean.Lsp.InlayHintKind)
  (textEdits?_1 : Option (Array Lean.Lsp.TextEdit)) (tooltip?_1 : Option Lean.Lsp.InlayHintTooltip)
  (paddingLeft?_1 paddingRight?_1 : Option Bool) (data?_1 : Option Lean.Json),
  ({ position := position, label := label, kind? := kind?, textEdits? := textEdits?, tooltip? := tooltip?,
        paddingLeft? := paddingLeft?, paddingRight? := paddingRight?, data? := data? } =
      { position := position_1, label := label_1, kind? := kind?_1, textEdits? := textEdits?_1, tooltip? := tooltip?_1,
        paddingLeft? := paddingLeft?_1, paddingRight? := paddingRight?_1, data? := data?_1 }) =
    (position = position_1 ∧
      label = label_1 ∧
        kind? = kind?_1 ∧
          textEdits? = textEdits?_1 ∧
            tooltip? = tooltip?_1 ∧ paddingLeft? = paddingLeft?_1 ∧ paddingRight? = paddingRight?_1 ∧ data? = data?_1)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c c' : CategoryTheory.Limits.PushoutCocone f g} (e : c ≅ c') (x₁ : X₁)
  (x₂ : X₂),
  (CategoryTheory.ConcreteCategory.hom c.inl) x₁ = (CategoryTheory.ConcreteCategory.hom c.inr) x₂ ↔
    (CategoryTheory.ConcreteCategory.hom c'.inl) x₁ = (CategoryTheory.ConcreteCategory.hom c'.inr) x₂
-- Mathlib.Data.SetLike.Basic
/-- The coercion from a term of a `SetLike` to its corresponding `Set`.  -/
SetLike.coe : {A : Type u_1} → {B : outParam (Type u_2)} → [self : SetLike A B] → A → Set B
-- Std.Time.Format.Modifier
Std.Time.Modifier.e.injEq : ∀ (presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text),
  (Std.Time.Modifier.e presentation = Std.Time.Modifier.e presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.single_hadamard_single_of_ne : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : MulZeroClass α]
  {ia : m} {ja : n} {ib : m} {jb : n},
  ¬(ia = ib ∧ ja = jb) → ∀ (a b : α), (Matrix.single ia ja a).hadamard (Matrix.single ib jb b) = 0
-- Init.Data.List.Lemmas
List.intercalate_nil : ∀ {α : Type u_1} {ys : List α}, ys.intercalate [] = []
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.eq_3 : ∀ {α : Type u} {β : Type v} (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntry?
      (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1) =
    Std.DTreeMap.Internal.Impl.Const.minEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
-- Mathlib.Data.List.Intervals
List.Ico.filter_le_of_bot : ∀ {n m : ℕ}, n < m → List.filter (fun x => decide (x ≤ n)) (List.Ico n m) = [n]
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_injective : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], Function.Injective QuaternionAlgebra.coe
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
-- Lean.DeprecatedModule
Lean.instInhabitedDeprecatedModuleEntry.default : Lean.DeprecatedModuleEntry
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimitsOfSize_iff_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G),
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F ↔
    CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The isomorphism between star and an abstract initial object of `WithInitial C`  -/
CategoryTheory.WithInitial.starIsoInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.WithInitial.star ≅ ⊥_ CategoryTheory.WithInitial C
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.restrict.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Submonoid M} {N' : Submonoid N}
  {f : M →* N} (h : Set.MapsTo ⇑f ↑M' ↑N'), MonoidHom.restrict h = (f.domRestrict M').codRestrict N' ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instIsMulCommutative_adjoin : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Type u_2}
  [inst_3 : SetLike S A] [inst_4 : MulMemClass S A] (s : S) [IsMulCommutative ↥s],
  IsMulCommutative ↥(Algebra.adjoin R ↑s)
-- Init.Data.List.Sublist
List.instDecidableSublistOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (l₁ l₂ : List α) → Decidable (l₁.Sublist l₂)
-- Mathlib.Algebra.Free
/-- Recursor that uses `pure` instead of `of`.  -/
FreeSemigroup.recOnPure : {α : Type u} →
  {C : FreeSemigroup α → Sort l} →
    (x : FreeSemigroup α) →
      ((x : α) → C (pure x)) → ((x : α) → (y : FreeSemigroup α) → C (pure x) → C y → C (pure x * y)) → C x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulForwardPatternModel.toLawfulForwardPattern : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.ForwardPattern pat}
  {inst_1 : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.LawfulForwardPatternModel pat], String.Slice.Pattern.LawfulForwardPattern pat
-- Mathlib.Analysis.Analytic.Order
/-- On a preconnected set, a meromorphic function has finite order at one point if it has finite
order at another point.  -/
AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x y : 𝕜},
  AnalyticOnNhd 𝕜 f U → IsPreconnected U → x ∈ U → y ∈ U → analyticOrderAt f x ≠ ⊤ → analyticOrderAt f y ≠ ⊤
-- Mathlib.FieldTheory.Perfect
/-- The iterated Frobenius automorphism for a perfect ring.  -/
iterateFrobeniusEquiv : (R : Type u_1) → (p : ℕ) → ℕ → [inst : CommSemiring R] → [ExpChar R p] → [PerfectRing R p] → R ≃+* R
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [Inhabited α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} [inst_5 : Inhabited α], (m₁.inter m₂).getKey! k = if m₂.contains k = true then m₁.getKey! k else default
-- Init.Data.Fin.Fold
Fin.foldl.loop.eq_def : ∀ {α : Sort u_1} (n : ℕ) (f : α → Fin n → α) (x : α) (i : ℕ),
  Fin.foldl.loop n f x i = if h : i < n then Fin.foldl.loop n f (f x ⟨i, h⟩) (i + 1) else x
-- Mathlib.Data.TwoPointing
TwoPointing.mk.injEq : ∀ {α : Type u_3} (toProd : α × α) (fst_ne_snd : toProd.1 ≠ toProd.2) (toProd_1 : α × α)
  (fst_ne_snd_1 : toProd_1.1 ≠ toProd_1.2),
  ({ toProd := toProd, fst_ne_snd := fst_ne_snd } = { toProd := toProd_1, fst_ne_snd := fst_ne_snd_1 }) =
    (toProd = toProd_1)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.tautologicalCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)),
  (CategoryTheory.Presheaf.tautologicalCocone P).pt = P
-- Mathlib.Topology.Algebra.Monoid
nhds_one_mul_nhds : ∀ {M : Type u_6} [inst : MulOneClass M] [inst_1 : TopologicalSpace M] [ContinuousMul M] (a : M),
  nhds 1 * nhds a = nhds a
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.null : {α : Type u} → {β : Type v} → {σ : Type w} → Lean.PersistentHashMap.Entry α β σ
-- Aesop.Util.UnorderedArraySet
_private.Aesop.Util.UnorderedArraySet.0.Aesop.UnorderedArraySet.mk : {α : Type u_1} → [inst : BEq α] → Array α → Aesop.UnorderedArraySet α
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
multipliableLocallyUniformlyOn_iff_hasProdLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  MultipliableLocallyUniformlyOn f s ↔ HasProdLocallyUniformlyOn f (fun x => ∏' (i : ι), f i x) s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_union_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (mem : k ∈ t₂),
  (t₁ ∪ t₂).get k ⋯ = t₂.get k mem
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Ioo : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.Ioo a b)],
  (Set.Ioo a b).toFinset = Finset.Ioo a b
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_mapDomainAddEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (e : M ≃ N)
  (x : MonoidAlgebra R M), ((MonoidAlgebra.mapDomainAddEquiv R e) x).coeff = Finsupp.equivMapDomain e x.coeff
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.instLawfulGetElemMem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp],
  LawfulGetElem (Std.ExtTreeMap α β cmp) α β fun m a => a ∈ m
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- A monad equipped with the ability to construct `WhiskerLeft` terms.  -/
Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft : (Type → Type) → Type
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.propagateDiseqOf.visitLhs : ℕ → Lean.Expr → Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.trivial_projective_of_subsingleton : ∀ {k : Type u} [inst : CommRing k] {G : Type u} [inst_1 : Group G] [Subsingleton G],
  CategoryTheory.Projective (Rep.trivial k G k)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Given a family of points together with a chosen base point in that family, membership of the
affine span of this family corresponds to an identity in terms of `weightedVSubOfPoint`, with
weights that are not required to sum to 1.  -/
mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd : ∀ {ι : Type u_1} (k : Type u_2) (V : Type u_3) {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Nontrivial k] (p : ι → P) (j : ι) (q : P),
  q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
_private.Mathlib.RingTheory.SimpleModule.WedderburnArtin.0.IsArtinianRing.isNoetherianRing_iff_isArtinianRing_mulOpposite : {R : Type u} → [inst : Ring R] → [IsArtinianRing R] → ProofWanted (IsNoetherianRing Rᵐᵒᵖ ↔ IsArtinianRing Rᵐᵒᵖ)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceE_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_3),
  (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f =
    CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯) (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_inf : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s t : Subsemiring S)
  (f : R →+* S), Subsemiring.comap f (s ⊓ t) = Subsemiring.comap f s ⊓ Subsemiring.comap f t
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.insert : Lean.Meta.Simp.UsedSimps → Lean.Meta.Origin → Lean.Meta.Simp.UsedSimps
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Relations.adF.eq_1 : ∀ (R : Type u) {B : Type v} [inst : CommRing R] (CM : Matrix B B ℤ),
  CartanMatrix.Relations.adF R CM =
    Function.uncurry fun i j =>
      ((LieAlgebra.ad R (FreeLieAlgebra R (CartanMatrix.Generators B)))
            ((FreeLieAlgebra.of R ∘ CartanMatrix.Generators.F) i) ^
          (-CM i j).toNat)
        ⁅(FreeLieAlgebra.of R ∘ CartanMatrix.Generators.F) i, (FreeLieAlgebra.of R ∘ CartanMatrix.Generators.F) j⁆
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Given an additive group acting freely and transitively, an equivalence between the
orbits under the action of an additive subgroup and the quotient of the group by the subgroup.  -/
AddAction.equivAddSubgroupOrbitsQuotientAddGroup : {G : Type u} →
  {X : Type v} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        X →
          [AddAction.IsPretransitive G X] →
            [IsCancelVAdd G X] → (H : AddSubgroup G) → AddAction.orbitRel.Quotient (↥H) X ≃ G ⧸ H
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- Cusp forms of weight `k < 12` for `𝒮ℒ` are zero-dimensional.  -/
CuspForm.rank_eq_zero_of_weight_lt_twelve : ∀ {k : ℤ}, k < 12 → Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The cone hull of a convex set is simply the union of the open halflines through that set.  -/
ConvexCone.coe_hull_of_convex : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M},
  Convex 𝕜 s → ↑(ConvexCone.hull 𝕜 s) = {x | ∃ r, 0 < r ∧ x ∈ r • s}
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiAlgebra.congr_simp : ∀ (R : Type u) (ι : Type v) (A : Type u_1) [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : CommSemiring A]
  [inst_3 : Algebra R A] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousMul A],
  ContinuousMultilinearMap.mkPiAlgebra R ι A = ContinuousMultilinearMap.mkPiAlgebra R ι A
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.ae_ae_of_ae_join : ∀ {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {p : α → Prop},
  (∀ᵐ (a : α) ∂m.join, p a) → ∀ᵐ (μ : MeasureTheory.Measure α) ∂m, ∀ᵐ (a : α) ∂μ, p a
-- Mathlib.Logic.Function.Basic
Function.const_def : ∀ {α : Sort u_1} {β : Sort u_2} {y : β}, (fun x => y) = Function.const α y
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
adjoin_le_integralClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x : A},
  IsIntegral R x → R[x] ≤ integralClosure R A
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.gamma_zero_le_of_veblen_le`. -/
Ordinal.gamma0_le_of_veblen_le : ∀ {o : Ordinal.{u}}, Ordinal.veblen o 0 ≤ o → Ordinal.gamma 0 ≤ o
-- Mathlib.Algebra.CharP.Quotient
Ideal.Quotient.index_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), ↑(Submodule.toAddSubgroup I).index = 0
-- Lean.Data.LBool
Lean.LBool.false.sizeOf_spec : sizeOf Lean.LBool.false = 1
-- Mathlib.Topology.FiberBundle.Constructions
FiberBundle.pullback_trivializationAtlas' : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] (f : K),
  FiberBundle.trivializationAtlas' = {ef | ∃ e, ∃ (_ : MemTrivializationAtlas e), ef = e.pullback f}
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.norm_down : ∀ {E : Type u_2} [inst : Norm E] (x : ULift.{u_5, u_2} E), ‖x.down‖ = ‖x‖
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_eq_same : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] (i : ι) (x : M i),
  Pi.mulSingle i x i = x
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- **Alias** of the reverse direction of `LinearMap.ker_coFG_iff_hasFiniteRange`. -/
LinearMap.HasFiniteRange.cofg_ker : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasFiniteRange → f.ker.CoFG
-- Init.Data.Ord.Basic
Ordering.isLE_left_of_isLE_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isLE = true → o₁.isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_alter_eq_sub_one : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  k ∈ t → (f (Std.DTreeMap.Const.get? t k)).isNone = true → (Std.DTreeMap.Const.alter t k f).size = t.size - 1
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.ord_cof : ∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f),
  a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
/-- A variant of `ContinuousMapZero.hasFiniteIntegral_of_bound` spelled in terms of
`ContinuousMapZero.mkD`.  -/
ContinuousMapZero.hasFiniteIntegral_mkD_of_bound : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : CompactSpace Y] [inst_4 : Zero Y] (f : X → Y → E)
  (g : ContinuousMapZero Y E),
  (∀ᵐ (x : X) ∂μ, Continuous (f x)) →
    (∀ᵐ (x : X) ∂μ, f x 0 = 0) →
      ∀ (bound : X → ℝ),
        MeasureTheory.HasFiniteIntegral bound μ →
          (∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖f x y‖ ≤ bound x) →
            MeasureTheory.HasFiniteIntegral (fun x => ContinuousMapZero.mkD (f x) g) μ
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat : ∀ (R : Type u) [inst : Ring R],
  CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)
-- Mathlib.Analysis.BoundedVariation
BoundedVariationOn.bilinear_comp : ∀ {α : Type u_2} [inst : LinearOrder α] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedAddCommGroup G]
  [inst_6 : NormedSpace ℝ G] {s : Set α} {f : α → E} {g : α → F},
  BoundedVariationOn f s →
    BoundedVariationOn g s → ∀ (B : E →L[ℝ] F →L[ℝ] G), BoundedVariationOn (fun x => (B (f x)) (g x)) s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W},
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f =
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g →
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f =
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g →
      f = g
-- Init.Data.Range.Polymorphic.UInt
UInt32.instHasSize_2 : Std.Rxi.HasSize UInt32
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_vadd : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} (x : E),
  Bornology.IsVonNBounded 𝕜 (x +ᵥ s) ↔ Bornology.IsVonNBounded 𝕜 s
-- Init.Data.Float.Float32
/-- Obtains the `Float32` whose value is the same as the given `UInt16`.  -/
UInt16.toFloat32 : UInt16 → Float32
-- Mathlib.Algebra.Group.Action.End
/-- The tautological action by `MulAut M` on `M`.

This generalizes `Function.End.applyMulAction`.  -/
MulAut.applyMulDistribMulAction : {M : Type u_2} → [inst : Monoid M] → MulDistribMulAction (MulAut M) M
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.toAdicCompletion.congr_simp : ∀ (σ : Type u_3) (R : Type u_4) [inst : Finite σ] [inst_1 : CommRing R],
  MvPowerSeries.toAdicCompletion σ R = MvPowerSeries.toAdicCompletion σ R
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.mk : Lean.Elab.Do.ReturnCont →
  Option (Lean.Elab.Do.DoElabM Lean.Expr) → Option (Lean.Elab.Do.DoElabM Lean.Expr) → Lean.Elab.Do.ContInfo
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.drop : Substring.Raw → ℕ → Substring.Raw
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.hundred_lt_pow_initialBound_mul : ∀ {ε : ℝ}, 0 < ε → ∀ (l : ℕ), 100 < 4 ^ SzemerediRegularity.initialBound ε l * ε ^ 5
-- Lean.Declaration
Lean.InductiveType.ctors : Lean.InductiveType → List Lean.Constructor
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instFinitenessRelation : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [inst_1 : Std.IteratorAccess α m] →
          [inst_2 : Monad m] →
            [Std.Iterators.Finite α m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.StepSizeIterator α m β) m
-- Lean.Elab.Term.TermElabM
/-- If `mayPostpone == true` and `e`'s head is a metavariable, throw `Exception.postpone`.  -/
Lean.Elab.Term.tryPostponeIfMVar : Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.InformationTheory.Hamming
Hamming.instNeg : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → Neg (β i)] → Neg (Hamming β)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_elim_eval : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R),
  (MvPolynomial.eval fun x => x.elim y s) f =
    Polynomial.eval y (Polynomial.map (MvPolynomial.eval s) ((MvPolynomial.optionEquivLeft R S₁) f))
-- Mathlib.RingTheory.Nilpotent.Defs
pow_pred_nilpotencyClass : ∀ {R : Type u_1} {x : R} [inst : MonoidWithZero R] [Nontrivial R], IsNilpotent x → x ^ (nilpotencyClass x - 1) ≠ 0