mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_empty : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, nhdsSetWithin s ∅ = ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_dite_right : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  (P : Prop) [inst_2 : Decidable P] (x : β → ¬P → α),
  (∑'[L] (b : β), if h : P then 0 else x b h) = if h : P then 0 else ∑'[L] (b : β), x b h
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
SkewMonoidAlgebra.nonUnitalAlgHom_ext' : ∀ {k : Type u_1} {G : Type u_2} {A : Type u_6} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Monoid G]
  [inst_2 : Semiring k] [inst_3 : MulSemiringAction G k] [inst_4 : DistribMulAction k A]
  {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A},
  φ₁.toMulHom.comp ↑(SkewMonoidAlgebra.of k G) = φ₂.toMulHom.comp ↑(SkewMonoidAlgebra.of k G) → φ₁ = φ₂
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The fundamental property of the adjoint.  -/
LinearMap.adjoint_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) (y : F),
  inner 𝕜 x ((LinearMap.adjoint A) y) = inner 𝕜 (A x) y
-- Mathlib.Order.Basic
Ne.lt_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → a ≤ b → a < b
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limitEquivSections_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x : CategoryTheory.Limits.limit F) (j : J),
  ↑((CategoryTheory.Limits.Types.limitEquivSections F) x) j =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x
-- Mathlib.Tactic.ErwQuestion
/-- Checks that the input `Expr` represents a proof produced by `(e)rw at` and returns the type of the
LHS of the equality (from the lemma used).
This will be defeq to the hypothesis being written, but not necessarily reducibly so.
 -/
Mathlib.Tactic.Erw?.extractRewriteHypEq : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [h : Std.TransCmp cmp] {k a : α} {v : β},
  (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial.eq_2 : ∀ (n : ℕ), n.succ.superFactorial = n.succ.factorial * n.superFactorial
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linkRef.nameStart : Lean.Parser.ParserFn
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_max : ∀ {X Y : SSet} (A B : X.Subcomplex) (p : Y ⟶ X), (A ⊔ B).preimage p = A.preimage p ⊔ B.preimage p
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.top_isIndContained_top_iff : ∀ {V : Type u_1} {W : Type u_2},
  (SimpleGraph.completeGraph V).IsIndContained (SimpleGraph.completeGraph W) ↔ Nonempty (V ↪ W)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
L_apply : ∀ {𝕜 : 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) {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] (g h : G) [inst_7 : ContMDiffMul I (↑⊤) G],
  (smoothLeftMul I g) h = g * h
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.sInf_adj_of_nonempty : ∀ {V : Type u} {G : SimpleGraph V} {a b : V} {s : Set G.Subgraph},
  s.Nonempty → ((sInf s).Adj a b ↔ ∀ G' ∈ s, G'.Adj a b)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_union_zero : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.closure (s ∪ {0}) = AddSubgroup.closure s
-- Mathlib.Topology.Algebra.Group.Basic
nhdsMulHom.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  nhdsMulHom = { toFun := nhds, map_mul' := ⋯ }
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.optionEquivLeft_X_some : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (i : σ),
  (MvPowerSeries.optionEquivLeft σ R) (MvPowerSeries.X (some i)) = PowerSeries.C (MvPowerSeries.X i)
-- Lean.Data.NameTrie
Lean.instInhabitedNamePart : Inhabited Lean.NamePart
-- Mathlib.Data.Part
Part.get_eq_iff_mem : ∀ {α : Type u_1} {o : Part α} {a : α} (h : o.Dom), o.get h = a ↔ a ∈ o
-- Mathlib.Analysis.Normed.Lp.lpHolder
/-- The map between `lp` spaces satisfying `ENNReal.HolderTriple` induced by a
uniformly bounded family of continuous bilinear maps on the underlying spaces.  -/
lp.holder : {ι : 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 q : ENNReal} →
                          (r : ENNReal) →
                            [hpqr : p.HolderTriple q r] →
                              (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) →
                                {K : ℝ} → (∀ (i : ι), ‖B i‖ ≤ K) → ↥(lp E p) → ↥(lp F q) → ↥(lp G r)
-- Mathlib.Algebra.Group.Basic
sub_nsmul_neg : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) {m n : ℕ}, n ≤ m → (m - n) • -a = -(m • a) + n • a
-- Mathlib.CategoryTheory.Presentable.Presheaf
CategoryTheory.Presheaf.instIsLocallyPresentableFunctorOppositeOfHasPullbacks : ∀ {A : Type u'} [inst : CategoryTheory.Category.{v', u'} A] [CategoryTheory.IsLocallyPresentable.{w, v', u'} A]
  [CategoryTheory.Limits.HasPullbacks A] (C : Type w) [inst_3 : CategoryTheory.SmallCategory C],
  CategoryTheory.IsLocallyPresentable.{w, max v' w, max (max (max u' w) v') w} (CategoryTheory.Functor Cᵒᵖ A)
-- Aesop.Tree.UnsafeQueue
Aesop.instInhabitedPostponedSafeRule.default : Aesop.PostponedSafeRule
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.filter_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  Std.ExtDHashMap.filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.ExtDHashMap.Const.get m k h) = false
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the right left `𝟙 X` on the right is a pushout square.  -/
CategoryTheory.IsPushout.zero_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPushout 0 0 (CategoryTheory.CategoryStruct.id X) 0
-- Aesop.Tree.Data
Aesop.Goal.setOrigin : Aesop.GoalOrigin → Aesop.Goal → Aesop.Goal
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.MulSaturated.sInf : ∀ {M : Type u_1} [inst : MulOneClass M] {f : Set (Submonoid M)}, (∀ s ∈ f, s.MulSaturated) → (sInf f).MulSaturated
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The coroot corresponding to a root.  -/
LieAlgebra.IsKilling.coroot : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            {H : LieSubalgebra K L} →
              [inst_4 : H.IsCartanSubalgebra] → [LieAlgebra.IsKilling K L] → LieModule.Weight K (↥H) L → ↥H
-- Init.Data.String.Defs
String.toByteArray_push : ∀ {s : String} {c : Char}, (s.push c).toByteArray = s.toByteArray ++ [c].utf8Encode
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.cofixA_eq_zero : ∀ (F : PFunctor.{uA, uB}) (x y : PFunctor.Approx.CofixA F 0), x = y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (t.alter k f).getKey! k = if (f t[k]?).isSome = true then k else default
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instSMulNatHom : {M N : AddCommGrpCat} → SMul ℕ (M ⟶ N)
-- Mathlib.Order.Category.BddDistLat
BddDistLat.Hom.ext : ∀ {X Y : BddDistLat} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J J' : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} (F_1 : J ⟶ J') (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).map F_1).snd.app X_1 = (F_1.app X_1).snd
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapRight_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set (γ × β)},
  MeasurableSet s → (κ.swapRight a) s = (κ a) {p | p.swap ∈ s}
-- Lean.Parser.Types
Lean.Parser.instBEqParserCacheKey : BEq Lean.Parser.ParserCacheKey
-- Init.Data.SInt.Bitwise
ISize.and_neg_one : ∀ {a : ISize}, a &&& -1 = a
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Variant with the same base that doesn't need `restrictScalars`.  -/
Algebra.TensorProduct.lift_comp_includeRight' : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hfg : ∀ (x : A) (y : B), Commute (f x) (g y)),
  (Algebra.TensorProduct.lift f g hfg).comp Algebra.TensorProduct.includeRight = g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The class of the element `Y - y(X)` in `R[W]` for some `y(X)` in `R[X]`.  -/
WeierstrassCurve.Affine.CoordinateRing.YClass : {R : Type r} → [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → Polynomial R → W'.CoordinateRing
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp.instBraided.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  [inst_4 : CategoryTheory.BraidedCategory C] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided],
  CategoryTheory.Functor.mapAddGrp.instBraided F =
    { toMonoidal := CategoryTheory.Functor.mapAddGrp.instMonoidal F, braided := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.mk.injEq : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] (X : D) [addMod : CategoryTheory.AddModObj A X] (X_1 : D)
  (addMod_1 : CategoryTheory.AddModObj A X_1),
  ({ X := X, addMod := addMod } = { X := X_1, addMod := addMod_1 }) = (X = X_1 ∧ addMod ≍ addMod_1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.toUnder_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T)
  (X_1 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))),
  ((CategoryTheory.StructuredArrow.toUnder X F).obj X_1).hom = X_1.hom
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseWeekdayShort : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Weekday
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.homCategory.ext : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ}, (∀ (a : B), Γ.as.app a = Δ.as.app a) → Γ = Δ
-- Init.Data.String.Defs
String.Slice.Pos.mk : {s : String.Slice} → (offset : String.Pos.Raw) → String.Pos.Raw.IsValidForSlice s offset → s.Pos
-- Mathlib.Order.Filter.Defs
/-- `f.Frequently p` or `∃ᶠ x in f, p x` mean that `{x | ¬p x} ∉ f`. E.g., `∃ᶠ x in atTop, p x`
means that there exist arbitrarily large `x` for which `p` holds true.  -/
Filter.Frequently : {α : Type u_1} → (α → Prop) → Filter α → Prop
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_mul_le_iff₀` for a version with multiplication on the other side.  -/
inv_mul_le_iff₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (c⁻¹ * b ≤ a ↔ b ≤ a * c)
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.ι_D₁_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂)
  (h : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h_1 : (K₁.mapBifunctor K₂ F c).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j') h_1) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j') h_1
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.replaceFTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((acc : Array α) → motive [] acc) →
          ((x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc) → motive x x_1
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- A finite product of pseudometric spaces is a pseudometric space, with the sup distance.  -/
pseudoMetricSpacePi : {β : Type u_2} →
  {X : β → Type u_3} → [Fintype β] → [(b : β) → PseudoMetricSpace (X b)] → PseudoMetricSpace ((b : β) → X b)
-- Lean.Message
/-- Preserves the originating syntax of the message.
 -/
Lean.MessageData.ofOriginatingSyntax : Lean.Syntax → Lean.MessageData → Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskeringEquivalence_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cocone.whiskeringEquivalence e).unitIso =
    CategoryTheory.NatIso.ofComponents'
      (fun s =>
        CategoryTheory.Limits.Cocone.extInv
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯)
      ⋯
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extInv.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} {c c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt)
  (w : ∀ (j : J), c.ι.app j = CategoryTheory.CategoryStruct.comp (c'.ι.app j) φ.inv),
  CategoryTheory.Limits.Cocone.extInv φ w =
    { hom := { hom := φ.hom, w := ⋯ }, inv := { hom := φ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_mono_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] (f : α → ε),
  ν.AbsolutelyContinuous μ → MeasureTheory.eLpNormEssSup f ν ≤ MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Order.DirectedInverseSystem
/-- To define a function from the direct limit, it suffices to provide one function from each
component subject to a compatibility condition.  -/
DirectLimit.lift : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F : ι → Type u_4} →
      {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
        (f : (i j : ι) → (h : i ≤ j) → T h) →
          [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
            [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                {C : Sort u_9} →
                  (ih : (i : ι) → F i → C) →
                    (∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)) → DirectLimit F f → C
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Hom.neg_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G X : C}
  [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ G),
  -f = CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.GroupTheory.Congruence.Hom
Con.mkMulHom.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), c.mkMulHom = { toFun := Con.toQuotient, map_mul' := ⋯ }
-- Mathlib.Algebra.Module.Presentation.Tautological
/-- The obvious solution of `tautologicalRelations A M` in the module `M`.  -/
Module.Presentation.tautologicalSolution : (A : Type u) →
  [inst : Ring A] →
    (M : Type v) →
      [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → (Module.Presentation.tautologicalRelations A M).Solution M
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Restrict the codomain of a multilinear map to a submodule.

This is the multilinear version of `LinearMap.codRestrict`.  -/
MultilinearMap.codRestrict : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  (f : MultilinearMap R M₁ M₂) →
                    (p : Submodule R M₂) → (∀ (v : (i : ι) → M₁ i), f v ∈ p) → MultilinearMap R M₁ ↥p
-- Mathlib.Algebra.Free
FreeSemigroup.lift_comp_of : ∀ {α : Type u} {β : Type v} [inst : Semigroup β] (f : α → β), ⇑(FreeSemigroup.lift f) ∘ FreeSemigroup.of = f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.prod_bot_left : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (t : AffineSubspace k P), ⊥.prod t = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCocone_ι_app : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F)
  (j : CategoryTheory.Discrete J), B.toCocone.ι.app j = B.ι j.as
-- Mathlib.Algebra.Category.Grp.Colimits
/-- (implementation detail) A morphism of commutative additive groups `Quot F →+ A`
induces a cocone on `F` as long as the universes work out.
 -/
AddCommGrpCat.Colimits.toCocone : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        {A : Type w} → [inst_2 : AddCommGroup A] → (AddCommGrpCat.Colimits.Quot F →+ A) → CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y]
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from X)
          (CategoryTheory.Limits.terminal.from Y))
        h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Mathlib.NumberTheory.FLT.Basic
FermatLastTheoremWith.mono : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] {m n : ℕ},
  m ∣ n → FermatLastTheoremWith R m → FermatLastTheoremWith R n
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_zero_apply : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (iterateFrobeniusEquiv R p 0) x = x
-- Init.Data.List.Find
List.findIdx?_eq_some_iff_findIdx_eq : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ},
  List.findIdx? p xs = some i ↔ i < xs.length ∧ List.findIdx p xs = i
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instHashableKey : Hashable Lean.Meta.RefinedDiscrTree.Key
-- Init.Data.List.Sublist
List.prefix_cons_iff : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :: t ∧ t <+: l₂
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.one_le_dist_inr_inl : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {x : X} {y : Y},
  1 ≤ Metric.Sum.dist (Sum.inr y) (Sum.inl x)
-- Init.Data.List.Range
List.zipIdx_map_snd : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.map Prod.snd (l.zipIdx i) = List.range' i l.length
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of `ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetSum_of_notMem`. -/
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∑ j ∈ s, f j) (f i) κ μ
-- Lean.Elab.Term.TermElabM
/-- Return the declaration of the given metavariable  -/
Lean.Elab.Term.getMVarDecl : Lean.MVarId → Lean.Elab.TermElabM Lean.MetavarDecl