mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C}
  [inst_1 : SizeOf C] (N : ℕ → C) (ι : (n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n }))
  (isColimit' :
    (Δ : SimplexCategoryᵒᵖ) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' N X ι Δ)),
  sizeOf { N := N, ι := ι, isColimit' := isColimit' } = 1
-- Init.Data.SInt.Lemmas
ISize.lt_iff_le_and_ne : ∀ {a b : ISize}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_E'5 : ADEInequality.Admissible (ADEInequality.E' 5)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a multiplication-invariant pseudodistance.  -/
SeminormedGroup.ofMulDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : Group E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y) → SeminormedGroup E
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] (di : IsDenseInducing i) (f : α → γ) (b : β),
  di.extend f b = (Filter.comap i (nhds b)).limUnder f
-- Std.Internal.UV.TCP
/-- Accepts an incoming connection on a listening TCP socket.
 -/
Std.Internal.UV.TCP.Socket.accept : Std.Internal.UV.TCP.Socket → IO (IO.Promise (Except IO.Error Std.Internal.UV.TCP.Socket))
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.IsEquivalent.rpow : ∀ {α : Type u_1} {u v : α → ℝ} {l : Filter α},
  0 ≤ v → Asymptotics.IsEquivalent l u v → ∀ {r : ℝ}, Asymptotics.IsEquivalent l (u ^ r) (v ^ r)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A singleton is a block.  -/
MulAction.IsBlock.singleton : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {a : X}, MulAction.IsBlock G {a}
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.then.match_1.splitter : (motive : Ordering → Sort u_1) →
  (a : Ordering) → (Unit → motive Ordering.eq) → ((a : Ordering) → (a = Ordering.eq → False) → motive a) → motive a
-- Mathlib.Data.Finset.Insert
Finset.cons_ne_empty : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), Finset.cons a s h ≠ ∅
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath.eq_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (x : C) (x_1 : Quiver.Path X x),
  CategoryTheory.composePath x_1 =
    match x, x_1 with
    | .(X), Quiver.Path.nil => CategoryTheory.CategoryStruct.id X
    | x, p.cons e => CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- Given a dense set `t`, then the range of `deriv f` is contained in the closure of the submodule
spanned by the image of `t`.  -/
range_deriv_subset_closure_span_image : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) {t : Set 𝕜},
  Dense t → Set.range (deriv f) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_and : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.and.eval = fun x1 x2 => x1 &&& x2
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.instBEqDefaultClause.beq : {numVarsSucc : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc → Bool
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.image_symm_eq_preimage : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂), ⇑e.symm '' s = ⇑e ⁻¹' s
-- Init.Data.Option.Lemmas
Option.all_false : ∀ {α : Type u_1} {o : Option α}, Option.all (fun x => false) o = o.isNone
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E} {f' : F}, HasLineDerivWithinAt 𝕜 f f' s x v → ∀ (c : 𝕜), HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_pos_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → x < 1 → 0 < Real.logb b x
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Define a continous `𝕜`-linear map fom `𝓓^{n}_{K}(E, F)` to a normed space.  -/
ContDiffMapSupportedIn.mkCLMtoNormedSpace : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    {n : ℕ∞} →
                      {K : TopologicalSpace.Compacts E} →
                        {G : Type u_5} →
                          [inst_7 : NormedAddCommGroup G] →
                            [inst_8 : NormedSpace 𝕜 G] →
                              (A : ContDiffMapSupportedIn E F n K → G) →
                                (∀ (f g : ContDiffMapSupportedIn E F n K), A (f + g) = A f + A g) →
                                  (∀ (c : 𝕜) (f : ContDiffMapSupportedIn E F n K), A (c • f) = c • A f) →
                                    (∃ s C,
                                        0 ≤ C ∧
                                          ∀ (f : ContDiffMapSupportedIn E F n K),
                                            ‖A f‖ ≤
                                              C * (s.sup fun i => ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f) →
                                      ContDiffMapSupportedIn E F n K →L[𝕜] G
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator : Inhabited Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist`.

---

The Hausdorff edistance between two sets is the smallest `r` such that each set
is contained in the `r`-neighborhood of the other one  -/
EMetric.hausdorffEdist : {α : Type u_2} → [PseudoEMetricSpace α] → Set α → Set α → ENNReal
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.uniformEquicontinuous_iff_right : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {p : κ → Prop}
  {s : κ → Set (α × α)} {F : ι → β → α},
  (uniformity α).HasBasis p s →
    (UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.isEmbedding : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → Topology.IsEmbedding f
-- Mathlib.Topology.Algebra.Indicator
IsClopen.continuous_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : One β], IsClopen s → Continuous f → Continuous (s.mulIndicator f)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.vComp_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.LaxTrans F G)
  (θ : CategoryTheory.Oplax.LaxTrans G H) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (η.vCompNaturality θ (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.vCompApp θ c)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapComp f g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.vCompApp θ a) (H.map f) (H.map g)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.vCompNaturality θ f) (H.map g))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (η.vCompApp θ b) (H.map g)).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (F.map f) (η.vCompNaturality θ g))
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.vCompApp θ c)).inv))))
-- Mathlib.Data.Finsupp.Lex
Finsupp.lex_eq_invImage_dfinsupp_lex : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] (r : α → α → Prop) (s : N → N → Prop),
  Finsupp.Lex r s = InvImage (DFinsupp.Lex r fun x => s) Finsupp.toDFinsupp
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.map_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {d : CategoryTheory.Limits.Cone G}
  (hd : CategoryTheory.Limits.IsLimit d) (α : F ⟶ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map c hd α) (d.π.app j) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) (α.app j)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.ofNat : ℕ → Std.Tactic.BVDecide.BVBinOp
-- Mathlib.Order.Hom.Lattice
SupHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : α → β) (hf : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b),
  ⇑{ toFun := f, map_sup' := hf } = f
-- Batteries.Util.ProofWanted
ProofWanted.mk.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α], sizeOf { } = 1
-- Lean.Meta.Tactic.Grind.Types
/-- `withSplitSource s x` executes `x` and uses `s` as the split source for any case-split
registered.
 -/
Lean.Meta.Grind.withSplitSource : {m : Type → Type u_1} →
  {α : Type} → [MonadControlT Lean.Meta.Grind.GrindM m] → [Monad m] → Lean.Meta.Grind.SplitSource → m α → m α
-- Mathlib.Algebra.Group.Indicator
/-- `Set.indicator` as an `addMonoidHom`.  -/
Set.indicatorHom : {α : Type u_6} → (M : Type u_7) → [inst : AddZeroClass M] → Set α → (α → M) →+ α → M
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : CommRingCat}
  (h : X.presheaf.obj (Opposite.op ⊤) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop g)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop f) h)
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.RootOrdered.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → α → Sort u_2) (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α)
  (x : α) (r : RBTree.RBNode α) (v : α) (h_1 : (x : α) → motive RBTree.RBNode.Path.root x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (x : α) → (r : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.Path.left c parent x r) v)
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (x : α) → (parent : RBTree.RBNode.Path α) → (v : α) → motive (RBTree.RBNode.Path.right c l x parent) v),
  (match RBTree.RBNode.Path.left c parent x r, v with
    | RBTree.RBNode.Path.root, x => h_1 x
    | RBTree.RBNode.Path.left c parent x r, v => h_2 c parent x r v
    | RBTree.RBNode.Path.right c l x parent, v => h_3 c l x parent v) =
    h_2 c parent x r v
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_left_comm : ∀ (x y z : ℕ), x ^^^ (y ^^^ z) = y ^^^ (x ^^^ z)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.ite : {x : Type} →
  (c : Prop) →
    [Decidable c] → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.ext_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {e e' : X ≃ᵈ Y},
  e = e' ↔ ∀ (x : X), e x = e' x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- An arrow ending in the zero object is zero  -/
CategoryTheory.Limits.zero_of_to_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (f : X ⟶ 0), f = 0
-- Mathlib.Data.Nat.Nth
Nat.count_nth_of_lt_card_finite : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ} (hp : (Set.ofPred p).Finite),
  n < hp.toFinset.card → Nat.count p (Nat.nth p n) = n
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.exists_of_mem_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  {f : α →o β} {b : β}, b ∈ c.map f → ∃ a ∈ c, f a = b
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.connectedComponentMk.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.connectedComponentMk v = Quot.mk G.Reachable v
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.field : (n : ℕ) → {K : Type u} → [inst : Field K] → (f : Polynomial K) → Field (Polynomial.SplittingFieldAux n f)
-- Mathlib.Algebra.Notation.Prod
Prod.fst_mul : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).1 = p.1 * q.1
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.min_lt_agm_of_pos_of_ne : ∀ {x y : NNReal}, 0 < x → 0 < y → x ≠ y → min x y < x.agm y
-- Mathlib.Data.Set.Piecewise
Set.eqOn_piecewise : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] {f f' g : α → β} {t : Set α},
  Set.EqOn (s.piecewise f f') g t ↔ Set.EqOn f g (t ∩ s) ∧ Set.EqOn f' g (t ∩ sᶜ)
-- Mathlib.Topology.Separation.Basic
t0Space_iff_or_notMem_closure : ∀ (X : Type u) [inst : TopologicalSpace X], T0Space X ↔ Pairwise fun a b => a ∉ closure {b} ∨ b ∉ closure {a}
-- Mathlib.Algebra.Group.Torsion
pow_left_injective : ∀ {M : Type u_1} [inst : Monoid M] [IsMulTorsionFree M] {n : ℕ}, n ≠ 0 → Function.Injective fun a => a ^ n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.number : Lean.Lsp.SymbolKind
-- Init.Data.BitVec.Bitblast
BitVec.DivModState.init.eq_1 : ∀ (w : ℕ), BitVec.DivModState.init w = { wn := w, wr := 0, q := 0#w, r := 0#w }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_eq_fallback : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, a ∉ m → Std.DHashMap.Raw.Const.getD m a fallback = fallback
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- On a sphere of nonzero radius, the central angle `∠ p₁ s.center p₂` equals `π` iff
`p₁` and `p₂` are diametrically opposite.  -/
EuclideanGeometry.Sphere.angle_center_eq_pi_iff_isDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → p₂ ∈ s → s.radius ≠ 0 → (EuclideanGeometry.angle p₁ s.center p₂ = Real.pi ↔ s.IsDiameter p₁ p₂)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity_nonneg : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K ≤ 1 → S.Nonempty → 0 ≤ Finset.connectivity✝ K S
-- Mathlib.Algebra.BigOperators.Finprod
/-- To prove a property of a finite product, it suffices to prove that the property is
multiplicative and holds on the factors.  -/
finprod_induction : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f : α → M} (p : M → Prop),
  p 1 → (∀ (x y : M), p x → p y → p (x * y)) → (∀ (i : α), p (f i)) → p (∏ᶠ (i : α), f i)
-- Mathlib.Data.Fintype.Pi
/-- Finite product of finite sets is finite  -/
Set.Finite.pi : ∀ {ι : Type u_3} [Finite ι] {κ : ι → Type u_4} {t : (i : ι) → Set (κ i)},
  (∀ (i : ι), (t i).Finite) → (Set.univ.pi t).Finite
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.toSubmodule_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ⊥.toSubmodule = ⊥
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.forall_iff : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (P : CategoryTheory.Under X → Prop),
  (∀ (Y : CategoryTheory.Under X), P Y) ↔ ∀ (Y : T) (f : X ⟶ Y), P (CategoryTheory.Under.mk f)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.MemLp.ae_norm_condExp_le_essSup : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E},
  MeasureTheory.MemLp f ⊤ μ → ∀ᵐ (x : α) ∂μ, ‖μ[f | m] x‖ ≤ essSup (fun x => ‖f x‖) μ
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux2.eq_3 : ∀ (o₂ : ONote) (m : ℕ),
  (m = 0 → False) →
    o₂.opowAux2 (ONote.zero, m.succ) =
      match o₂.split' with
      | (b', k) => b'.oadd (m.succPNat ^ k) 0
-- Mathlib.LinearAlgebra.Complex.Module
/-- The real part `ℜ a` of an element `a` of a star module over `ℂ`, as a linear map. This is just
`selfAdjointPart ℝ`, but we provide it as a separate definition in order to link it with lemmas
concerning the `imaginaryPart`, which doesn't exist in star modules over other rings.  -/
ComplexStarModule.termℜ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.factorThruCoimage f
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  WittVector.ghostFun✝ x n = (MvPolynomial.aeval x.coeff) (wittPolynomial p ℤ n)
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- The coercion between integer-fraction pairs happens componentwise.  -/
GenContFract.IntFractPair.coeFn : {K : Type u_1} → {β : Type u_2} → [Coe K β] → GenContFract.IntFractPair K → GenContFract.IntFractPair β
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_union_sdiff : ∀ {α : Type u_1} (s t : Set α), s ∩ t ∪ s \ t = s
-- Lean.Message
Lean.MessageData.brecOn_2.go : {motive_1 : Lean.MessageData → Sort u} →
  {motive_2 : Array Lean.MessageData → Sort u} →
    {motive_3 : List Lean.MessageData → Sort u} →
      (t : List Lean.MessageData) →
        ((t : Lean.MessageData) → t.below → motive_1 t) →
          ((t : Array Lean.MessageData) → Lean.MessageData.below_1 t → motive_2 t) →
            ((t : List Lean.MessageData) → Lean.MessageData.below_2 t → motive_3 t) →
              motive_3 t ×' Lean.MessageData.below_2 t
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Logarithm of function represented by a monomial, i.e.
`m[0] * log basis[0] + ... + m[n] * log basis[n]`.  -/
Tactic.ComputeAsymptotics.UnitMonomial.toLogFun : Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.Basis → ℝ → ℝ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKeyD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Init.System.IOError
/-- An unexpected end-of-file marker was encountered.  -/
IO.Error.unexpectedEof : IO.Error
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.y : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Year.Offset
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.embeddingUpIntLE_f : ∀ (p : ℤ) (n : ℕ), (ComplexShape.embeddingUpIntLE p).f n = p - ↑n
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- Every weakly locally compact space is a compactly coherent space.  -/
CompactlyCoherentSpace.of_weaklyLocallyCompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X], CompactlyCoherentSpace X
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.mk : Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.VarSet → Lean.Elab.Term.Do.CodeBlock
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_eq_not_any_not : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {p : α → β → Bool},
  m.all p = !m.any fun a b => !p a b
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instFunctor : Functor MeasureTheory.OuterMeasure
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Set.IsPWO.submonoid_closure : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α] {s : Set α},
  (∀ x ∈ s, 1 ≤ x) → s.IsPWO → (↑(Submonoid.closure s)).IsPWO
-- Init.Prelude
EStateM.Backtrackable.mk : {δ : outParam (Type u)} → {σ : Type u} → (σ → δ) → (σ → δ → σ) → EStateM.Backtrackable δ σ
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'_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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f] {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x (CategoryTheory.inv f)) h) =
    h
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum.eq_1 : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S),
  p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
-- Mathlib.Algebra.Order.Star.Real
NNReal.instStarOrderedRing : StarOrderedRing NNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The map from the zero object is a kernel of a monomorphism  -/
CategoryTheory.Limits.kernel.isLimitConeZeroCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
            [CategoryTheory.Mono f] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.kernel.zeroKernelFork f)
-- Init.Data.Ord.Basic
Ordering.swap_inj : ∀ {o₁ o₂ : Ordering}, o₁.swap = o₂.swap ↔ o₁ = o₂
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.emptyWithCapacity : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Aesop.OrderedHashSet α
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Construct a bornology from a distance function and metric space axioms.  -/
Bornology.ofDist : {α : Type u_3} →
  (dist : α → α → ℝ) →
    (∀ (x y : α), dist x y = dist y x) → (∀ (x y z : α), dist x z ≤ dist x y + dist y z) → Bornology α
-- Lean.ResolveName
Lean.preprocessSyntaxAndResolve : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Lean.Syntax → (Lean.Name → m (List Lean.Name)) → m (List Lean.Name)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cones.RepresentableBy X) (s : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s = h.homEquiv.symm s.π