mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_symm_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (r : Rᵐᵒᵖ) (n : ℕ),
  (Polynomial.opRingEquiv R).symm (Polynomial.C r * Polynomial.X ^ n) =
    MulOpposite.op (Polynomial.C (MulOpposite.unop r) * Polynomial.X ^ n)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.coe_ofOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ↪ β), ⇑(RelEmbedding.ofOnFun r f) = ⇑f
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.add_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β},
  StrictConcaveOn 𝕜 s f → ConcaveOn 𝕜 s g → StrictConcaveOn 𝕜 s (f + g)
-- Lean.LocalContext
Lean.LocalContext.lastDecl : Lean.LocalContext → Option Lean.LocalDecl
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_ground_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E : Set α}, (N.comapOn E f).E = E
-- Mathlib.Order.DirSupClosed
dirSupInaccOn_iff_forall_sSup : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : CompleteLattice α],
  DirSupInaccOn D s ↔
    ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty
-- Mathlib.Data.ENNReal.Basic
ENNReal.instAddCommMonoid : AddCommMonoid ENNReal
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {f : β k → β k},
          (Std.DTreeMap.Internal.Impl.modify k f t₁).Equiv (Std.DTreeMap.Internal.Impl.modify k f t₂)
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ioi : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Ici a) → Filter.Tendsto f Filter.atTop Filter.atTop → Set.Ioi (f a) ⊆ f '' Set.Ioi a
-- Std.Time.Date.ValidDate
Std.Time.instDecidableEqValidDate : {leap : Bool} → DecidableEq (Std.Time.ValidDate leap)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.QuotientMeasureEqMeasurePreimage.mk : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.QuotientMeasureEqMeasurePreimage._auto_1}
  {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))},
  (∀ (t : Set α),
      MeasureTheory.IsFundamentalDomain G t ν →
        μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t)) →
    MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.setOfPred_isPrime_finite : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R], {I | I.IsPrime}.Finite
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.sorted_iff_seq_sorted : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)}, ms.Sorted ↔ ms.seq.Sorted
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_of_injective : ∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι → κ),
  Function.Injective e →
    ∀ (f : ι → M) (g : κ → M), (∀ i ∉ Set.range e, g i = 1) → (∀ (i : ι), f i = g (e i)) → ∏ i, f i = ∏ j, g j
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)),
  (Std.Internal.List.Const.modifyKey k f l).length = l.length
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (Δ : SimplexCategoryᵒᵖ),
  (CategoryTheory.nerve C).obj Δ = CategoryTheory.ComposableArrows C (Opposite.unop Δ).len
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- Universal property of the free product of algebras:
for every `R`-algebra `B`, every family of maps `maps : (i : I) → (A i →ₐ[R] B)` lifts
to a unique arrow `π` from `FreeProduct R A` such that  `π ∘ ι i = maps i`.  -/
LinearAlgebra.FreeProduct.lift : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] →
              {B : Type w'} →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] → ({i : I} → A i →ₐ[R] B) ≃ (LinearAlgebra.FreeProduct R A →ₐ[R] B)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is a group object and `F` is monoidal,
then `Hom(X, G) → Hom(F X, F G)` preserves inverses.  -/
CategoryTheory.Functor.map_inv' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X G : C} (f : X ⟶ G) [inst_5 : CategoryTheory.GrpObj G],
  F.map f⁻¹ = (F.map f)⁻¹
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex_union_eq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    Disjoint (K₁.carrier + -V) (K₂.carrier + -V) →
      MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V =
        MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β}
  (h : l.Balanced), l.Ordered → (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v l h).2.impl.Ordered
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.ext : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] {f g : A ≃⋆* B},
  (∀ (a : A), f a = g a) → f = g
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_apply_right`. -/
Equiv.Perm.SameCycle.apply_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle x (f y)
-- Init.Data.Dyadic.Basic
Dyadic.one_mul : ∀ (x : Dyadic), 1 * x = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_associator : ∀ {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₄} {Y : Type u₅} {Z : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} Z] {T : Type u₇} [inst_6 : CategoryTheory.Category.{v₇, u₇} T]
  (U : CategoryTheory.Functor X Y) (V : CategoryTheory.Functor Y Z) (W : CategoryTheory.Functor Z T),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map (U.associator V W).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G (U.comp V) W).hom
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj W).whiskerLeft
          (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U V).hom)
        (CategoryTheory.CategoryStruct.comp
          (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj W).associator
              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V)
              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)).inv
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight
              (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G V W).inv
              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U))
            (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U (V.comp W)).inv)))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyPrepareParams : Type
-- Mathlib.GroupTheory.Schreier
/-- **Schreier's Lemma**: If `R : Finset G` and `H : Subgroup G` are complements with `1 ∈ R`, and
if `G` is generated by `S : Finset G`, then `H` is generated by the `Finset`
  `(R * S).image (fun g ↦ g * (hR.toRightFun g)⁻¹)`.  -/
Subgroup.closure_mul_image_eq_top' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : DecidableEq G] {R S : Finset G}
  (hR : Subgroup.IsComplement ↑H ↑R),
  1 ∈ R →
    Subgroup.closure ↑S = ⊤ → Subgroup.closure ↑(Finset.image (fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.iff_of_equiv_equiv : ∀ {A₁ : Type u_1} {B₁ : Type u_2} {A₂ : Type u_3} {B₂ : Type u_4} [inst : Field A₁] [inst_1 : Ring B₁]
  [inst_2 : Field A₂] [inst_3 : Ring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) → (Algebra.IsSeparable A₁ B₁ ↔ Algebra.IsSeparable A₂ B₂)
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.neg.match_1.splitter : (motive : ℤ → Sort u_1) → (n : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive n
-- Mathlib.Analysis.BoxIntegral.Basic
/-- A function that is bounded on a box `I` and a.e. continuous is integrable on `I`.

This is a version of `integrable_of_bounded_and_ae_continuousWithinAt` with a stronger continuity
assumption so that the user does not need to specialize the continuity assumption to each box on
which the theorem is to be applied.  -/
BoxIntegral.integrable_of_bounded_and_ae_continuous : ∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : Fintype ι]
  (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E},
  (∃ C, ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ],
      (∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x) → BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_mul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {a b : G}, ContMDiffAt I I n (fun x => x * a) b
-- Mathlib.Order.Minimal
maximal_iff_forall_gt : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : Preorder α], Maximal P x ↔ P x ∧ ∀ ⦃y : α⦄, x < y → ¬P y
-- Mathlib.Order.FixedPoints
OrderHom.lfp_induction : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {p : α → Prop},
  (∀ (a : α), p a → a ≤ OrderHom.lfp f → p (f a)) → (∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)) → p (OrderHom.lfp f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.sub_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] (f g : X ⟶ G) (h : G ⟶ H)
  [CategoryTheory.IsAddMonHom h] {Z : C} (h_1 : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f - g) (CategoryTheory.CategoryStruct.comp h h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h - CategoryTheory.CategoryStruct.comp g h)
      h_1
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.scientificLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (s₀ : E.I₀ → F.I₀) (h₀ h₀_1 : (i : E.I₀) → E.X i ⟶ F.X (s₀ i))
  (e_h₀ : h₀ = h₀_1) (w₀ : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i) (F.f (s₀ i)) = E.f i),
  { s₀ := s₀, h₀ := h₀, w₀ := w₀ } = { s₀ := s₀, h₀ := h₀_1, w₀ := ⋯ }
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_monotone : ∀ {R : Type u} [inst : Preorder R], Monotone Tropical.untrop
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_left_le_size_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_smul : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass S R N] [inst_8 : SMulCommClass R S N] (a : S)
  (B : LinearMap.BilinMap R M N), (a • B).toQuadraticMap = a • B.toQuadraticMap
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.mk.inj : ∀ {ref : Lean.Syntax} {tactic : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq} {ref_1 : Lean.Syntax}
  {tactic_1 : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq},
  { ref := ref, tactic := tactic } = { ref := ref_1, tactic := tactic_1 } → ref = ref_1 ∧ tactic = tactic_1
-- Lean.Server.CodeActions.Basic
Lean.Server.instFileSourceCodeAction : Lean.Lsp.FileSource Lean.Lsp.CodeAction
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.mfderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {s : Set E} {x : E}, UniqueMDiffAt[s] x → mfderiv[s] ⇑f x = f
-- Mathlib.RingTheory.Bialgebra.GroupLike
isGroupLikeElem_unitsInv : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {u : Aˣ},
  IsGroupLikeElem R ↑u⁻¹ ↔ IsGroupLikeElem R ↑u
-- Lean.Parser.Command
Lean.Parser.Command.import.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Tactics
/-- A `simpArg` is either a `*`, `-lemma` or a simp lemma specification
(which includes the `↑` `↓` `←` specifications for pre, post, reverse rewriting).
 -/
Lean.Parser.Tactic.simpArg : Lean.ParserDescr
-- Lean.Compiler.IR.Basic
/-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`.  -/
Lean.IR.Expr.uproj : ℕ → Lean.IR.VarId → Lean.IR.Expr
-- Mathlib.CategoryTheory.Action.Basic
Action.resId_hom_app_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} [inst_1 : Monoid G] (X : Action V G),
  ((Action.resId V).hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
-- Std.Async.Basic
/-- Create an `AsyncTask` that resolves to the value of `x`.
 -/
Std.Async.AsyncTask.ofPromise : {α : Type} →
  IO.Promise (Except IO.Error α) →
    optParam String "the promise linked to the Async Task was dropped" → Std.Async.AsyncTask α
-- Mathlib.Dynamics.Ergodic.Ergodic
QuasiErgodic.aeconst_set₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  QuasiErgodic f μ →
    MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.coe_measureUnivNNReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  ↑(MeasureTheory.measureUnivNNReal μ) = μ Set.univ
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `MonoOver.image : Over X ⥤ MonoOver X` is left adjoint to
`MonoOver.forget : MonoOver X ⥤ Over X`
 -/
CategoryTheory.MonoOver.imageForgetAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] → CategoryTheory.MonoOver.image ⊣ CategoryTheory.MonoOver.forget X
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconcaveOn.inf : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {f g : E → β} [inst_4 : SemilatticeInf β],
  QuasiconcaveOn 𝕜 s f → QuasiconcaveOn 𝕜 s g → QuasiconcaveOn 𝕜 s (f ⊓ g)
-- Std.Time.Date.PlainDate
Std.Time.instReprPlainDate : Repr Std.Time.PlainDate
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.of_finite : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} [Finite β]
  [L.HasSupport] {f : β → α}, Multipliable f L
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    ∀ (a b : ℝ) (N : ℕ),
      MeasureTheory.Submartingale
        (fun n => ∑ k ∈ Finset.range n, (1 - MeasureTheory.upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- If a coalgebra morphism has an inverse, it is a coalgebra isomorphism.  -/
CoalgEquiv.ofCoalgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] →
                    (f : A →ₗc[R] B) →
                      (g : B →ₗc[R] A) → f.comp g = CoalgHom.id R B → g.comp f = CoalgHom.id R A → A ≃ₗc[R] B
-- Mathlib.Computability.Partrec
Nat.Partrec.ppred : Nat.Partrec fun n => ↑n.ppred
-- Mathlib.Data.Finset.Density
Finset.dens.eq_1 : ∀ {α : Type u_2} [inst : Fintype α] (s : Finset α), s.dens = ↑s.card / ↑(Fintype.card α)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.add_lt_aleph0 : ∀ {a b : Cardinal.{u_1}}, a < Cardinal.aleph0 → b < Cardinal.aleph0 → a + b < Cardinal.aleph0
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instNoZeroDivisorsCastInt : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d], NoZeroDivisors (ℤ√↑d)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (x_3 : CategoryTheory.LaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- `α →ᵇ β` is the type of bounded continuous functions `α → β` from a topological space to a
metric space.

When possible, instead of parametrizing results over `(f : α →ᵇ β)`,
you should parametrize over `(F : Type*) [BoundedContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `BoundedContinuousMapClass`.  -/
BoundedContinuousFunction.«term_→ᵇ_» : Lean.TrailingParserDescr
-- Batteries.Recycling.RBTree.Basic
/-- The keys of the map. This is an `O(1)` wrapper operation, which
can be used in `for` loops or converted to an array or list.
 -/
RBTree.RBMap.keys : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → RBTree.RBMap.Keys α β cmp
-- Std.Internal.Do.Triple.SpecLemmas
/-- An invariant combinator for `String.Slice` loops with early return, for the new `do`
elaborator which uses `Prod` for the state tuple: `onContinue` is the invariant while iterating,
`onReturn` holds once the loop returned early with a value.  -/
Std.Internal.Do.StringSliceInvariant.withEarlyReturnNewDo : {s : String.Slice} →
  {β γ : Type u} →
    (Pred : Type u) →
      [Std.Internal.Do.Assertion Pred] →
        (s.Pos → β → Pred) → (γ → β → Pred) → Std.Internal.Do.StringSliceInvariant s (Option γ × β) Pred
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableEmbedding_neg : ∀ {α : Type u_3} {m : MeasurableSpace α} [inst : InvolutiveNeg α] [MeasurableNeg α], MeasurableEmbedding Neg.neg
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.divRight₀_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : MulPosReflectLT G₀] (a : G₀)
  (ha : 0 < a) (x : G₀), (RelIso.symm (OrderIso.divRight₀ a ha)) x = x * a
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.comp_monotone_on_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
  AntivaryOn f g s → Monotone f' → AntivaryOn (f' ∘ f) g s
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instPartialOrder : {X : Type u_1} →
  {R : Type u_2} → [inst : Zero R] → [inst_1 : Add R] → [inst_2 : PartialOrder R] → PartialOrder (PseudoMetric X R)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.ParseResult.success.injEq : ∀ {α ι : Type} (pos : ι) (res : α) (pos_1 : ι) (res_1 : α),
  (Std.Internal.Parsec.ParseResult.success pos res = Std.Internal.Parsec.ParseResult.success pos_1 res_1) =
    (pos = pos_1 ∧ res = res_1)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.restrictScalars_toSubalgebra : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L]
  {E : IntermediateField L' L},
  (IntermediateField.restrictScalars K E).toSubalgebra = Subalgebra.restrictScalars K E.toSubalgebra
-- Lean.Elab.InfoTree.Types
Lean.Elab.UserWidgetInfo.stx : Lean.Elab.UserWidgetInfo → Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_compl : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableEq V] [inst_2 : DecidableRel G.Adj] (v : V),
  Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.map : ∀ {α : Type u_1} {β : Type u_2} {n : Type u_4} [inst : Zero α] [inst_1 : Zero β] {A : Matrix n n α},
  A.IsDiag → ∀ {f : α → β}, f 0 = 0 → (A.map f).IsDiag
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.fst d) = forIn t.keys init f
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.not_indep_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {X : Set α}, M.IsLoop e → e ∈ X → ¬M.Indep X
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.tensor : ∀ {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₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {inst_4 : F₁.LaxMonoidal} {inst_5 : F₂.LaxMonoidal}
  [self : CategoryTheory.NatTrans.IsMonoidal τ] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₁ X Y)
      (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (τ.app X) (τ.app Y))
      (CategoryTheory.Functor.LaxMonoidal.μ F₂ X Y)