mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.bilin_of_top_right : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p : ENNReal}
  (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K : ℝ},
  (∀ (i : ι), ‖B i‖ ≤ K) →
    ∀ {e : (i : ι) → E i} {f : (i : ι) → F i}, Memℓp e p → Memℓp f ⊤ → Memℓp (fun i => ((B i) (e i)) (f i)) p
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
HasFDerivWithinAt.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
  {g : ι → E → F} {g' : ι → E →L[𝕜] F} {s : Set E} {x : E} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  HasFDerivWithinAt f f' s x →
    (∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x) →
      HasFDerivWithinAt (fun x => (f x) fun x_1 => g x_1 x)
        ((ContinuousAlternatingMap.apply 𝕜 F G fun x_1 => g x_1 x) ∘SL f' +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL g' i)
        s x
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.neg_add_toLeftFun_mem : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G} (hS : AddSubgroup.IsComplement S ↑H) (g : G),
  -g + ↑(hS.toLeftFun g) ∈ H
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.mapAugmentedCechConerve_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g),
  (CategoryTheory.Arrow.mapAugmentedCechConerve F).right = CategoryTheory.Arrow.mapCechConerve F
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The model space used to define `n`-dimensional real manifolds without boundary.  -/
Manifold.term𝓡_ : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Extend an ordered partition of `n` entries, by adding singleton to the left or appending it
to one of the existing part.  -/
OrderedFinpartition.extend : {n : ℕ} → (c : OrderedFinpartition n) → Option (Fin c.length) → OrderedFinpartition (n + 1)
-- Lean.Server.References
Lean.Server.instToJsonIlean.toJson : Lean.Server.Ilean → Lean.Json
-- Batteries.Data.Float.Lemmas
Float32.nan_beq_eq_false : ∀ (f : Float32), (Float32.nan == f) = false
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.le_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  (s : AddSubmonoid M), s ≤ s.topologicalClosure
-- Mathlib.Data.List.InsertIdx
List.take_eraseIdx_eq_take_of_le : ∀ {α : Type u} (l : List α) (i j : ℕ), i ≤ j → List.take i (l.eraseIdx j) = List.take i l
-- Mathlib.Tactic.Simps.Basic
/-- A Boolean specifying whether this projection is written as prefix.  -/
Simps.ProjectionData.isPrefix : Simps.ProjectionData → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Star
HasFDerivWithinAt.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : StarModule 𝕜 F] [inst_8 : ContinuousStar F] {f : E → F} {f' : E →L[𝕜] F} {x : E}
  {s : Set E} [inst_9 : TrivialStar 𝕜],
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => star (f x)) (↑(starL' 𝕜) ∘SL f') s x
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y)
      (X.presheaf.stalkSpecializes h)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_δ : ∀ {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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : G.LaxMonoidal] (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ F X Y =
    (adj.homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))).symm
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
        (CategoryTheory.Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)))
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.mul_one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : L.Term ((γ ⊕ α) ⊕ β)),
  FirstOrder.Language.Term.constantsVarsEquivLeft.symm t =
    (FirstOrder.Language.Term.relabel (⇑(Equiv.sumAssoc γ α β)) t).varsToConstants
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Polynomial.Chebyshev.complex_ofReal_eval_C : ∀ (x : ℝ) (n : ℤ), ↑(Polynomial.eval x (Polynomial.Chebyshev.C ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.C ℂ n)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_equivMapOfInjective_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : M →ₛₗ[σ₁₂] M₂)
  (i : Function.Injective ⇑f) (p : Submodule R M) (x : ↥(Submodule.map f p)),
  f ↑((Submodule.equivMapOfInjective f i p).symm x) = ↑x
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeS_prodMap : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (f : R →+* S) (g : S →+* T), (f.prodMap g).rangeS = f.rangeS.prod g.rangeS
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.addMonoid : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → AddMonoid (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.equivOfEquivalence_apply : ∀ {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a : α),
  (CategoryTheory.Discrete.equivOfEquivalence h) a =
    (CategoryTheory.Discrete.as ∘ h.functor.obj ∘ CategoryTheory.Discrete.mk) a
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_transpose : ∀ {n : Type u_3} {α : Type v} (A : Matrix n n α), A.transpose.diag = A.diag
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiber.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y),
  AlgebraicGeometry.Scheme.Hom.fiber f y = CategoryTheory.Limits.pullback f (Y.fromSpecResidueField y)
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
/-- If `p` is an odd prime and `IsCyclotomicExtension {p} K L`, then
`discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)` if
`Irreducible (cyclotomic p K)`.  -/
IsCyclotomicExtension.discr_odd_prime : ∀ {p : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsCyclotomicExtension {p} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ p),
  Irreducible (Polynomial.cyclotomic p K) →
    p ≠ 2 → Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
-- Mathlib.Tactic.TFAE
/-- Turn syntax for a given index into a natural number, as long as it lies between `1` and
`maxIndex`.  -/
Mathlib.Tactic.TFAE.elabIndex : Lean.TSyntax `num → ℕ → Lean.MetaM ℕ
-- Mathlib.Algebra.Group.Prod
MonoidHom.prod_unique : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : M →* N × P), ((MonoidHom.fst N P).comp f).prod ((MonoidHom.snd N P).comp f) = f
-- Mathlib.GroupTheory.DoubleCoset
/-- The double coset as an element of `Set α` corresponding to `s a t`  -/
DoubleCoset.doubleCoset : {α : Type u_2} → [Mul α] → α → Set α → Set α → Set α
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.List.takeWhile₂.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (b : β) (bs : List β)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_2 : (x : List α) → (x_1 : List β) → motive x x_1),
  (match a :: as, b :: bs with
    | a :: as, b :: bs => h_1 a as b bs
    | x, x_1 => h_2 x x_1) =
    h_1 a as b bs
-- Lean.DocString.Markdown
Lean.Doc.MarkdownM.InlineCtx.mk.inj : ∀ {inEmph inBold inLink inEmph_1 inBold_1 inLink_1 : Bool},
  { inEmph := inEmph, inBold := inBold, inLink := inLink } =
      { inEmph := inEmph_1, inBold := inBold_1, inLink := inLink_1 } →
    inEmph = inEmph_1 ∧ inBold = inBold_1 ∧ inLink = inLink_1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.op_comp_unop : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp g.unop f.unop).op = CategoryTheory.CategoryStruct.comp f g
-- Init.Data.Array.Range
Array.range'_1_concat : ∀ {s n : ℕ}, Array.range' s (n + 1) = Array.range' s n ++ #[s + n]
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_hom_counit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (adj1.rightAdjointUniq adj2).hom F)
      adj2.counit =
    adj1.counit
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] (f : SkewMonoidAlgebra k G), f.sum SkewMonoidAlgebra.single = f
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffAt.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E} {x : G}
  {n : WithTop ℕ∞}, ContDiffAt ℝ n f x → f x ≠ 0 → ContDiffAt ℝ n (fun y => ‖f y‖) x
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- `WalkingParallelPair` as a category is equivalent to a special case of
`WalkingParallelFamily`.  -/
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool) ≌ CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The equivalence between `Hom (F X) Y` and `Hom X (G Y)` coming from an adjunction  -/
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G → (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
-- Mathlib.CategoryTheory.Comma.Basic
/-- The canonical functor from the product of two categories to the comma category of their
respective functors into `Discrete PUnit`.  -/
CategoryTheory.Comma.fromProd : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) →
          (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) →
            CategoryTheory.Functor (A × B) (CategoryTheory.Comma L R)
-- Mathlib.Algebra.Group.Units.Defs
isAddUnit_iff_exists_neg : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {a : M}, IsAddUnit a ↔ ∃ b, a + b = 0
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.divOf_add_modOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x : AddMonoidAlgebra k G) (g : G), AddMonoidAlgebra.of' k G g * x.divOf g + x.modOf g = x
-- Mathlib.CategoryTheory.Action.Basic
Action.mk.injEq : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (V_1 : V)
  (ρ : G →* CategoryTheory.End V_1) (V_2 : V) (ρ_1 : G →* CategoryTheory.End V_2),
  ({ V := V_1, ρ := ρ } = { V := V_2, ρ := ρ_1 }) = (V_1 = V_2 ∧ ρ ≍ ρ_1)
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.mk : Lean.LevelSet → Lean.ExprSet → Array Lean.Name → Lean.CollectLevelParams.State
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Ioc : ∀ (a b : ℝ), UniqueDiffOn ℝ (Set.Ioc a b)
-- Mathlib.Data.Num.Basic
/-- Converts a `ZNum` to an `Option Num`, where `ofZNum p = 0` if `p < 0`.  -/
Num.ofZNum : ZNum → Num
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- The right uniformity on a topological group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformGroup` structure. Two important special cases where they _do_ coincide are for
commutative groups (see `isUniformGroup_of_commGroup`) and for compact groups (see
`IsUniformGroup.of_compactSpace`).  -/
IsTopologicalGroup.rightUniformSpace : (G : Type u_1) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → UniformSpace G
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg.inj : ∀ {e : Lean.Expr} {p : Int.Internal.Linear.Poly} {e_1 : Lean.Expr} {p_1 : Int.Internal.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg e p = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreNeg e_1 p_1 →
    e = e_1 ∧ p = p_1
-- Init.Data.SInt.Basic
/-- The largest number that `Int16` can represent: `2^15 - 1 = 32767`.  -/
Int16.maxValue : Int16
-- Mathlib.GroupTheory.Solvable
Group.instIsSolvableOfSubsingleton : ∀ (G : Type u_1) [inst : Group G] [Subsingleton G], Group.IsSolvable G
-- Mathlib.Order.UpperLower.Closure
/-- The biggest lower subset of a lower set `s` not containing an element `a`.  -/
LowerSet.erase : {α : Type u_1} → [inst : Preorder α] → LowerSet α → α → LowerSet α
-- Mathlib.Order.Closure
ClosureOperator.ext_isClosed : ∀ {α : Type u_1} [inst : PartialOrder α] (c₁ c₂ : ClosureOperator α),
  (∀ (x : α), c₁.IsClosed x ↔ c₂.IsClosed x) → c₁ = c₂
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instCategoryWithWeakEquivalencesHoCat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.CategoryWithWeakEquivalences (HomotopicalAlgebra.CofibrantObject.HoCat C)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_concaveOn_of_integrand_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {β : Type u_6} [inst_6 : AddCommMonoid β] [inst_7 : Module ℝ β] {f : α → β → E} {s : Set β},
  Convex ℝ s →
    (∀ᵐ (x : α) ∂μ, ConcaveOn ℝ s (f x)) →
      (∀ a ∈ s, MeasureTheory.Integrable (fun x => f x a) μ) → ConcaveOn ℝ s fun b => ∫ (x : α), f x b ∂μ
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finite : ∀ {α : Type u} {m : MeasureTheory.OuterMeasure α} {ι : Type u_1} {s : ι → Set α} {t : Set ι},
  t.Finite → (∀ i ∈ t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ t, s i)
-- Mathlib.Topology.Order.Monotone
/-- If a function is monotone in a second countable topological space, then there
are only countably many points that have several preimages.  -/
Monotone.countable_setOfPred_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [SecondCountableTopology α],
  Monotone f → {c | ∃ x y, x < y ∧ f x = c ∧ f y = c}.Countable
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.iInf_Ioi_eq : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [OrderTopology R] [DenselyOrdered R]
  [NoMaxOrder R] (f : StieltjesFunction R) (x : R), ⨅ r, ↑f ↑r = ↑f x
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t).a =
    t.desc (CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c)
-- Mathlib.Data.Nat.Cast.Order.Basic
/-- See also `Nat.cast_nonneg`, specialised to `IsOrderedRing`.  -/
Nat.cast_nonneg' : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ),
  0 ≤ ↑n
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a nonarchimedean additive abelian group, and let `f : ℕ → G` be a
function such that the differences `f (n + 1) - f n` tend to zero.
Then the function is a Cauchy sequence.  -/
NonarchimedeanAddGroup.cauchySeq_of_tendsto_sub_nhds_zero : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G]
  {f : ℕ → G}, Filter.Tendsto (fun n => f (n + 1) - f n) Filter.atTop (nhds 0) → CauchySeq f
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_zero_bot : CongruenceSubgroup.Gamma 0 = ⊥
-- Mathlib.SetTheory.ZFC.PSet
PSet.mk_type : ∀ (α : Type u_1) (A : α → PSet.{u_1}), (PSet.mk α A).Type = α
-- Mathlib.Analysis.MellinTransform
mellin_comp_mul_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) {a : ℝ},
  0 < a → mellin (fun t => f (a * t)) s = ↑a ^ (-s) • mellin f s
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorem.mk : Lean.Name → ℕ → Array Lean.Meta.DiscrTree.Key → Lean.Meta.Ext.ExtTheorem
-- Lean.Environment
Lean.ModuleIdx : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.ofList_singleton : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {k : α} {v : β k},
  Std.DHashMap.ofList [⟨k, v⟩] = ∅.insert k v
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km fallback : α}, t.maxKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_left : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌈x⌉) (nhdsWithin (↑n) (Set.Iic ↑n)) (nhdsWithin (↑n) (Set.Iic ↑n))
-- Init.Data.Int.DivMod.Basic
/-- Balanced division.

This returns the unique integer so that `b * (Int.bdiv a b) + Int.bmod a b = a`.

Examples:
* `(7 : Int).bdiv 0 = 0`
* `(0 : Int).bdiv 7 = 0`
* `(12 : Int).bdiv 6 = 2`
* `(12 : Int).bdiv 7 = 2`
* `(12 : Int).bdiv 8 = 2`
* `(12 : Int).bdiv 9 = 1`
* `(-12 : Int).bdiv 6 = -2`
* `(-12 : Int).bdiv 7 = -2`
* `(-12 : Int).bdiv 8 = -1`
* `(-12 : Int).bdiv 9 = -1`
 -/
Int.bdiv : ℤ → ℕ → ℤ
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_obj : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] (j : J),
  (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂).obj j =
    CategoryTheory.Enriched.FunctorCategory.enrichedHom V ((CategoryTheory.Under.forget j).comp F₁)
      ((CategoryTheory.Under.forget j).comp F₂)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEquiv_eq_map : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} (f : α ≃ β), M.mapEquiv f = M.map ⇑f ⋯
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instAdd : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → Add (M →ₗ⁅R,L⁆ N)
-- Mathlib.FieldTheory.Relrank
/-- `IntermediateField.relrank A B` is defined to be `[B : A ⊓ B]` as a `Cardinal`, in particular,
when `A ≤ B` it is `[B : A]`, the degree of the field extension `B / A`.
This is similar to `Subgroup.relIndex` but it is `Cardinal` valued.  -/
IntermediateField.relrank : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → IntermediateField F E → IntermediateField F E → Cardinal.{v}
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.symm₂ : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁}, p.Homotopic q → p.symm.Homotopic q.symm
-- Mathlib.Algebra.Group.Subgroup.Map
/-- the `AddMonoidHom` from an additive subgroup to its image  -/
AddMonoidHom.addSubgroupMap : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : AddGroup G] → [inst_1 : AddGroup G'] → (f : G →+ G') → (H : AddSubgroup G) → ↥H →+ ↥(AddSubgroup.map f H)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.ofPolar_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (toFun : M → N)
  (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
  (polar_add_left :
    ∀ (x x' y : M), QuadraticMap.polar toFun (x + x') y = QuadraticMap.polar toFun x y + QuadraticMap.polar toFun x' y)
  (polar_smul_left : ∀ (a : R) (x y : M), QuadraticMap.polar toFun (a • x) y = a • QuadraticMap.polar toFun x y)
  (a : M), (QuadraticMap.ofPolar toFun toFun_smul polar_add_left polar_smul_left) a = toFun a