mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WellFoundedSet
Set.Subsingleton.isPWO : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.Subsingleton → s.IsPWO
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} [inst_2 : Inhabited (β a)] {v : β k},
  (t.insertIfNew k v).get! a = if h : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get! a
-- Init.Data.SInt.Basic
/-- Decides whether two 16-bit signed integers are equal. Usually accessed via the `DecidableEq Int16`
instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Int16.decEq 123 123 = .isTrue rfl`
 * `(if ((-7) : Int16) = 7 then "yes" else "no") = "no"`
 * `show (7 : Int16) = 7 by decide`
 -/
Int16.decEq : (a b : Int16) → Decidable (a = b)
-- Init.Data.Fin.Lemmas
Fin.cast_zero : ∀ {n m : ℕ} [inst : NeZero n] [inst_1 : NeZero m] (h : n = m), Fin.cast h 0 = 0
-- Lean.Meta.Tactic.Grind.EMatch
/-- Performs one round of E-matching, and returns new instances.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.ematchCore : Array Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.InstanceMap
-- Lean.Meta.Tactic.Apply
/-- Try to synthesize instances for the metavariables `mvars`.
Returns metavariables that still need to be synthesized.
We can view the resulting array as the set of metavariables that we should try again.
This is needed when applying or rewriting with functions with complex instances.
For example, consider `rw [@map_smul]` where `map_smul` is
```
map_smul {F : Type u_1} {M : Type u_2} {N : Type u_3} {φ : M → N}
         {X : Type u_4} {Y : Type u_5}
         [SMul M X] [SMul N Y] [FunLike F X Y] [MulActionSemiHomClass F φ X Y]
         (f : F) (c : M) (x : X) : DFunLike.coe f (c • x) = φ c • DFunLike.coe f x
```
and `MulActionSemiHomClass` is defined as
```
class MulActionSemiHomClass (F : Type _)
   {M N : outParam (Type _)} (φ : outParam (M → N))
   (X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
```
The left-hand-side of the equation does not bind `N`. Thus, `SMul N Y` cannot
be synthesized until we synthesize `MulActionSemiHomClass F φ X Y`. Note that
`N` is an output parameter for `MulActionSemiHomClass`.
 -/
_private.Lean.Meta.Tactic.Apply.0.Lean.Meta.synthAppInstances.step : Lean.Name → Lean.MVarId → Bool → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.imₗ_apply : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] (self : QuadraticAlgebra R a b),
  (QuadraticAlgebra.imₗ a b) self = self.im
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.injEq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R}
  (toCompletion toCompletion_1 : (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion),
  ({ toCompletion := toCompletion } = { toCompletion := toCompletion_1 }) = (toCompletion = toCompletion_1)
-- Lean.ReducibilityAttrs
Lean.isImplicitReducibleCore : Lean.Environment → Lean.Name → Bool
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.resolventTransform_def : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜} (μ : MeasureTheory.Measure 𝕜),
  MeasureTheory.resolventTransform μ = fun a => ∫ (x : 𝕜), resolvent a x ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Every diagram is naturally isomorphic (actually, equal) to a `wideCospan`  -/
CategoryTheory.Limits.WidePullbackShape.diagramIsoWideCospan : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (F : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape J) C) →
        F ≅
          CategoryTheory.Limits.WidePullbackShape.wideCospan (F.obj none) (fun j => F.obj (some j)) fun j =>
            F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂_symm : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Fintype n] [inst_8 : Fintype m]
  [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂),
  (Matrix.toLinearMap₂ b₁ b₂).symm = LinearMap.toMatrix₂ b₁ b₂
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instContinuousLinearMapClass : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W},
  ContinuousLinearMapClass (ContIntertwiningMap π₁ π₂) R V W
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Convert a `MatchResult` into a `Array`, with better matches at the start of the array.
 -/
Lean.Meta.RefinedDiscrTree.MatchResult.toArray : {α : Type} → Lean.Meta.RefinedDiscrTree.MatchResult α → Array α
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.subLeft_symm_apply : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x b : G),
  (Homeomorph.subLeft x).symm b = -b + x
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- `S` has Dirichlet density `δ` when the ratio of the partial sum over `S` to the sum over all
nonzero prime ideals,
$$
\frac{\sum_{\mathfrak p \in S} \operatorname{N} \mathfrak p^{-s}}
  {\sum_{\mathfrak p} \operatorname{N} \mathfrak p^{-s}},
$$
tends to `δ` as $s \to 1^+$.  -/
NumberField.Set.HasDirichletDensity : {K : Type u_1} →
  [inst : Field K] →
    [NumberField K] → Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → ℝ → Prop
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.congr_fun_ae : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f g : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s μ → f =ᵐ[μ.restrict s] g → MeasureTheory.IntegrableOn g s μ
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bodyInterest.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β] (x : Bool), sizeOf (Std.Http.Server.Connection.Recv.bodyInterest✝ x) = 1 + sizeOf x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.mkJmp : Lean.Syntax → Lean.Name → Array Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_add_apply : ∀ {P Q : AddCommGrpCat} (f g : P ⟶ Q) (x : ↑P),
  (CategoryTheory.ConcreteCategory.hom (f + g)) x =
    (CategoryTheory.ConcreteCategory.hom f) x + (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.comp_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S} (f : E.Hom F) (g : F.Hom G)
  (a : E.I₀), (f.comp g).s₀ a = (g.s₀ ∘ f.s₀) a
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β), (sSupHom.id β).comp f = f
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithInitial Cᵒᵖ),
  (CategoryTheory.WithTerminal.opEquiv C).counitIso.inv.app X =
    (match X with
      | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of x)
      | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_rid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 E 𝕜), ‖(TensorProduct.rid 𝕜 E) x‖ = ‖x‖
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  [∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.RightResolution X₂)] [Φ.arrow.HasRightResolutions] [W₂.ContainsIdentities]
  {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_3, u_3} D] (L : CategoryTheory.Functor C₂ D) [L.IsLocalization W₂]
  {X₂ : C₂} {X₃ : D} (y : L.obj X₂ ⟶ X₃),
  CategoryTheory.IsConnected
    ((CategoryTheory.TwoSquare.mk Φ.functor (Φ.functor.comp L) L (CategoryTheory.Functor.id D)
          (Φ.functor.comp L).rightUnitor.inv).CostructuredArrowDownwards
      y)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U.eq_4 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.U R (Int.negSucc n) =
    2 * Polynomial.X * Polynomial.Chebyshev.U R (-↑n) - Polynomial.Chebyshev.U R (-↑n + 1)
-- Std.Internal.UV.DNS
/-- Performs a reverse DNS lookup on a `SocketAddress`.
 -/
Std.Internal.UV.DNS.getNameInfo : Std.Net.SocketAddress → IO (IO.Promise (Except IO.Error (String × String)))
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on a closed interval of real numbers,
or on the unit interval of real numbers  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromRealInterval : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Lean.DocString.Syntax
Lean.Doc.Syntax.doc_arg.quot : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway : ∀ {X : AlgebraicGeometry.Scheme} {F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat}
  {α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F},
  CategoryTheory.NatTrans.Coequifibered α ↔
    ∀ (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      IsLocalization.Away ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U))) f)
        ↑(F.obj (Opposite.op (U.basicOpen f)))
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_eq_ofInt : ∀ {n : ℤ} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt), Int16.ofIntLE n h₁ h₂ = Int16.ofInt n
-- Mathlib.Order.SymmDiff
bihimp_self : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a : α), bihimp a a = ⊤
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.any_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : MonadLiftT m n] [inst_3 : Std.IteratorLoop α m m] [inst_4 : Monad m]
  [LawfulMonad m] [inst_6 : Monad n] [inst_7 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [LawfulMonadLiftT m n] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → n (Option β')} {p : β' → Bool},
  Std.IterM.any p (Std.IterM.filterMapM f it) =
    Std.IterM.anyM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => pure { down := p fx }
          | none => pure { down := false })
      (Std.IterM.mapM pure it)
-- Mathlib.Data.Set.Sigma
Set.forall_sigma_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α i → Prop},
  (∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p ⟨i, a⟩
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.instFintype : {G : Type u_3} → [Fintype G] → Fintype (ConjAct G)
-- Mathlib.AlgebraicGeometry.EffectiveEpi
/-- If `π : X ⟶ Y` is a flat and surjective morphism between affine schemes, then `π` is a
regular epimorphism in the category of schemes.  -/
AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (π : X ⟶ Y)
  [AlgebraicGeometry.Surjective π] [AlgebraicGeometry.Flat π], CategoryTheory.IsRegularEpi π
-- Mathlib.Order.Lattice
/-- The binary infimum, used to derive `Min α`  -/
SemilatticeInf.inf : {α : Type u} → [self : SemilatticeInf α] → α → α → α
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldlM.eq_1 : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} [inst : Monad m] (f : σ → α → m σ) (x : σ),
  RBTree.RBNode.foldlM f x RBTree.RBNode.nil = pure x
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The logarithms of the Euler factors of a Dirichlet L-series form a summable sequence.  -/
DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ}, 1 < s.re → Summable fun p => -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁),
  (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).hom)
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
-- Mathlib.Computability.Ackermann
ack_mono_right : ∀ (m : ℕ), Monotone (ack m)
-- Mathlib.Algebra.Group.Ideal
/-- The additive semigroup ideal generated by `s` is `s ∪ Set.univ + s`.  -/
AddSemigroupIdeal.coe_closure : ∀ {M : Type u_1} [inst : AddSemigroup M] {s : Set M}, ↑(AddSemigroupIdeal.closure s) = s ∪ (Set.univ + s)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.out : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.Final] (d : D),
  CategoryTheory.IsConnected (CategoryTheory.StructuredArrow d F)
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.hasDerivAt_mulExpNegMulSq : ∀ {ε : ℝ} (y : ℝ),
  HasDerivAt ε.mulExpNegMulSq (Real.exp (-(ε * y * y)) + y * (Real.exp (-(ε * y * y)) * (-2 * ε * y))) y
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
exteriorPower.basis_repr_ne : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) {s t : ↑(Set.powersetCard I n)},
  s ≠ t → ((Module.Basis.exteriorPower n b).repr (exteriorPower.ιMulti_family R n (⇑b) s)) t = 0
-- Mathlib.Algebra.CharP.Basic
CharP.natCast_eq_natCast' : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}, a ≡ b [MOD p] → ↑a = ↑b
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesStep.eq_1 : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = { carrier := {x | ∀ (y : G), ⁅x, y⁆ ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.neg : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} {f : X → E},
  MeasureTheory.LocallyIntegrableOn f s μ → MeasureTheory.LocallyIntegrableOn (-f) s μ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `-π / 2`, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(-Real.pi / 2) → x ≠ 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.findP?_insert_of_ne : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {v : α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsStrictCut cmp cut] (t : RBTree.RBSet α cmp),
  cut v ≠ Ordering.eq → (t.insert v).findP? cut = t.findP? cut
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.norm`.

---

The norm of a strongly progressive process is strongly progressive.  -/
MeasureTheory.ProgMeasurable.norm : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  [inst_1 : MeasurableSpace ι] {β : Type u_4} {u : ι → Ω → β} [inst_2 : SeminormedAddCommGroup β],
  MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsStronglyProgressive f fun t ω => ‖u t ω‖
-- Mathlib.Data.Real.ConjExponents
ENNReal.isConjExponent_comm : ∀ {p q : ENNReal}, p.HolderConjugate q ↔ q.HolderConjugate p
-- Mathlib.Computability.Reduce
ManyOneReducible.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, p ≤₀ q → q ≤₀ r → p ≤₀ r
-- Mathlib.SetTheory.Ordinal.Notation
/-- The property satisfied by `fundamentalSequence o`:

* `inl none` means `o = 0`
* `inl (some a)` means `o = succ a`
* `inr f` means `o` is a limit ordinal and `f` is a strictly increasing sequence which converges to
  `o`  -/
ONote.FundamentalSequenceProp : ONote → Option ONote ⊕ (ℕ → ONote) → Prop
-- Lean.Elab.ConfigEval.Commands
/-- `option key := fun cfg item => ...` adds a configuration option named `key` with the given
expression as its handler. The handler is only called when the key is an exact match.
The provided value is in `item.value`. Such a handler implies `omit key`.

`option key.* := fun cfg item => ...` adds configuration options with `key` as a proper prefix.
The most-specific `*` handler is called if no handlers for exact matches apply.
 -/
Lean.Elab.ConfigEval.configEntryHandler : Lean.ParserDescr
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instBotValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → Bot (ValuativeRel.ValueGroupWithZero R)
-- Init.Data.List.Impl
/-- Auxiliary for `replace`: `replace.go l b c xs acc = acc.toList ++ replace xs b c`,
unless `b` is not found in `xs` in which case it returns `l`.  -/
_private.Init.Data.List.Impl.0.List.replaceTR.go : {α : Type u_1} → [BEq α] → List α → α → α → List α → Array α → List α
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- A groupoid is closed under restriction if it contains all restrictions of its element local
homeomorphisms to open subsets of the source.  -/
ClosedUnderRestriction : {H : Type u_1} → [inst : TopologicalSpace H] → StructureGroupoid H → Prop
-- Init.Data.Prod
Prod.instReflBEq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [inst_1 : BEq β] [ReflBEq α] [ReflBEq β], ReflBEq (α × β)
-- Mathlib.Order.CompleteLattice.SetLike
Sublattice.mem_subtype : ∀ {X : Type u_1} {L : Sublattice (Set X)} {T : ↥L} {x : X}, x ∈ L.subtype T ↔ x ∈ T
-- Lean.ExtraModUses
Lean.IndirectModUse.declName : Lean.IndirectModUse → Lean.Name
-- Mathlib.Analysis.Convex.Between
mem_const_vadd_affineSegment : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (v : V),
  v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y
-- Mathlib.CategoryTheory.Square
CategoryTheory.Functor.mapSquare_map_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (F.mapSquare.map φ).τ₃ = F.map φ.τ₃
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context : Type
-- Mathlib.Data.Fintype.WithTopBot
instFintypeWithBot.eq_1 : ∀ {α : Type u_1} [inst : Fintype α], instFintypeWithBot = { elems := instFintypeWithBot._aux_1, complete := ⋯ }
-- Mathlib.Data.Set.Subset
Set.eq_of_preimage_val_eq_of_subset : ∀ {α : Type u_2} {A B C : Set α}, B ⊆ A → C ⊆ A → Subtype.val ⁻¹' B = Subtype.val ⁻¹' C → B = C
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mul_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.GrpObj A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul
      (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h) =
    CategoryTheory.CategoryStruct.comp (β_ A A).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {V W : BialgCat R} {toBialgHom' toBialgHom'_1 : V.carrier →ₐc[R] W.carrier},
  { toBialgHom' := toBialgHom' } = { toBialgHom' := toBialgHom'_1 } → toBialgHom' = toBialgHom'_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.equiv_iff_toList_perm : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ ↔ (Std.DHashMap.Raw.Const.toList m₁).Perm (Std.DHashMap.Raw.Const.toList m₂)
-- Mathlib.ModelTheory.Basic
/-- The homomorphism commutes with the interpretations of the function symbols  -/
FirstOrder.Language.Embedding.map_fun' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.Embedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  self.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (self.toFun ∘ x)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_finset_inf : ∀ {ι : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] (f : ι → TopologicalSpace.Closeds α) (s : Finset ι),
  ↑(s.inf f) = s.inf (SetLike.coe ∘ f)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.of_isIso_fac_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} {h : Z ⟶ X}
  [CategoryTheory.IsIso f] [hh : CategoryTheory.IsIso h],
  CategoryTheory.CategoryStruct.comp g f = h → CategoryTheory.IsIso g
-- Mathlib.Data.Set.Lattice
Set.sInter_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → Set γ) (s : Set α) (t : Set β),
  ⋂₀ Set.image2 f s t = ⋂ a ∈ s, ⋂ b ∈ t, f a b
-- Mathlib.Topology.Sheaves.Skyscraper
/-- `skyscraperPresheafFunctor` is the right adjoint of `Presheaf.stalkFunctor`
 -/
skyscraperPresheafStalkAdjunction : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              TopCat.Presheaf.stalkFunctor C p₀ ⊣ skyscraperPresheafFunctor p₀
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.of_mul : ∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : SMul R M] [inst_1 : Mul R] [IsScalarTower R R M],
  IsSMulRegular M (a * b) → IsSMulRegular M b
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.t2Space : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [T2Space F] (𝔖 : Set (Set E)), ⋃₀ 𝔖 = Set.univ → T2Space (UniformConvergenceCLM σ F 𝔖)