mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Iic_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ico a b ⊆ Finset.Iic b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor from the costructured arrow category on `snd L R` over `b : B` to the
costructured arrow category on `L` over `R.obj b`. It is left adjoint to
`costructuredArrowSndInclusion`, see `costructuredArrowSndAdjunction`.  -/
CategoryTheory.Comma.costructuredArrowSndProj : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (b : B) →
                  CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b)
                    (CategoryTheory.CostructuredArrow L (R.obj b))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.π_desc' : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.Limits.Cofork.IsColimit.desc hs k h) = k
-- Mathlib.CategoryTheory.Sites.Canonical
/-- Variant of the Yoneda embedding which allows a raise in the universe level
for the category of types.  -/
CategoryTheory.GrothendieckTopology.uliftYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [J.Subcanonical] → CategoryTheory.Functor C (CategoryTheory.Sheaf J (Type (max v w)))
-- Mathlib.RingTheory.PowerSeries.Binomial
PowerSeries.binomialSeries_nat : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : BinomialRing R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  (d : ℕ), PowerSeries.binomialSeries A ↑d = (1 + PowerSeries.X) ^ d
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet.of_precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {s : ι → Set Ω} {ι' : Type u_5} {g : ι' → ι},
  Function.Surjective g → ProbabilityTheory.Kernel.iIndepSet (s ∘ g) κ μ → ProbabilityTheory.Kernel.iIndepSet s κ μ
-- Mathlib.Topology.Sheaves.Functors
TopCat.Sheaf.pushforward_forget : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (f : X ⟶ Y),
  (TopCat.Sheaf.pushforward C f).comp (TopCat.Sheaf.forget C Y) =
    (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.pushforward C f)
-- Mathlib.Analysis.Oscillation
oscillation.eq_1 : ∀ {E : Type u} {F : Type v} [inst : PseudoEMetricSpace F] [inst_1 : TopologicalSpace E] (f : E → F) (x : E),
  oscillation f x = ⨅ S ∈ Filter.map f (nhds x), Metric.ediam S
-- Mathlib.CategoryTheory.Balanced
CategoryTheory.balanced_opposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C], CategoryTheory.Balanced Cᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R),
  K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) =
    CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.toSchauderBasis_coord : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (b : HilbertBasis ℕ 𝕜 E) (i : ℕ), b.toSchauderBasis.coord i = (innerSL 𝕜) (b i)
-- Std.Internal.Parsec.Basic
/-- Peeks at the next element or returns a default if at EOF, does not consume input.
 -/
Std.Internal.Parsec.peekD : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → elem → Std.Internal.Parsec ι elem
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.dist_toLp_snd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (y₁ y₂ : β), dist (WithLp.toLp p (0, y₁)) (WithLp.toLp p (0, y₂)) = dist y₁ y₂
-- Init.Prelude
/-- Catches errors thrown in `body`, passing them to `handler`. Errors in `handler` are not caught.
 -/
MonadExcept.tryCatch : {ε : outParam (Type u)} → {m : Type v → Type w} → [self : MonadExcept ε m] → {α : Type v} → m α → (ε → m α) → m α
-- Mathlib.Condensed.Basic
/-- `Condensed.{u} C` is the category of condensed objects in a category `C`, which are
defined as sheaves on `CompHaus.{u}` with respect to the coherent Grothendieck topology.
 -/
Condensed : (C : Type w) → [CategoryTheory.Category.{v, w} C] → Type (max (max (max w v) (u + 1)) u)
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_snd_coe : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (x_1 : Quiver.Costar (Quiver.SingleObj.star S)),
  ↑((Quiver.SchreierGraph.labellingCostarEquiv ι x).symm x_1).snd = x_1.snd
-- Mathlib.Order.Disjointed
disjointed_le_id : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι], disjointed ≤ id
-- Mathlib.MeasureTheory.Measure.Comap
MeasurableEmbedding.comap_add : ∀ {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ ν : MeasureTheory.Measure β),
      MeasureTheory.Measure.comap f (μ + ν) = MeasureTheory.Measure.comap f μ + MeasureTheory.Measure.comap f ν
-- Mathlib.Order.UpperLower.Basic
isUpperSet_iff_Ici_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Ici a ⊆ s
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termHatβ : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Rank
_private.Mathlib.Algebra.Lie.Rank.0.LieModule.termφ : Lean.ParserDescr
-- Mathlib.Order.Lattice
inf_lt_of_right_lt : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, b < c → a ⊓ b < c
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- The derivative of a bounded bilinear map at a point `p : E × F`, as a continuous linear map
from `E × F` to `G`. The statement that this is indeed the derivative of `f` is
`IsBoundedBilinearMap.hasFDerivAt` in `Analysis.Calculus.FDeriv`.  -/
IsBoundedBilinearMap.deriv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : SeminormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {G : Type u_4} →
                  [inst_5 : SeminormedAddCommGroup G] →
                    [inst_6 : NormedSpace 𝕜 G] → {f : E × F → G} → IsBoundedBilinearMap 𝕜 f → E × F → E × F →L[𝕜] G
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.blocksFun.eq_1 : ∀ {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length), c.blocksFun i = ↑(c.boundary ⟨↑i + 1, ⋯⟩) - ↑(c.boundary ⟨↑i, ⋯⟩)
-- Init.Data.UInt.Lemmas
UInt16.add_comm : ∀ (a b : UInt16), a + b = b + a
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instSuccOrderAdditive : {X : Type u_1} → [inst : Preorder X] → [h : SuccOrder X] → SuccOrder (Additive X)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exp_pos : ∀ {G : Type u_3} [inst : Preorder G] {a : G}, 0 < WithZero.exp a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.algebraMap_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (k : 𝕜),
  ((algebraMap 𝕜 (DoubleCentralizer 𝕜 A)) k).toProd = (algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))) k
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The submonoid consisting of the units of a monoid  -/
IsUnit.submonoid : (M : Type u_4) → [inst : Monoid M] → Submonoid M
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ofHom_app_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (f : P.Hom Q) (X : C) (Y : Dᵒᵖ),
  ((CategoryTheory.Profunctor.ofHom f).app X).app Y = f.app X (Opposite.unop Y)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind : Type
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.IsAffineOpen.sup_of_disjoint : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    AlgebraicGeometry.IsAffineOpen V → Disjoint U V → AlgebraicGeometry.IsAffineOpen (U ⊔ V)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Given a set `s`, return the continuous linear map `fun x : E ↦ B x (μ s)` (actually defined
using `transpose` through `mapRange`), where the `B` is a `G`-valued bilinear form on `E × F` and
`μ` is an `F`-valued vector measure. The extension of that set function through `setToFun` gives the
pairing integral of `E`-valued integrable functions.  -/
MeasureTheory.cbmApplyMeasure : {X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {G : Type u_6} →
        {mX : MeasurableSpace X} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NormedAddCommGroup G] →
                    [inst_5 : NormedSpace ℝ G] →
                      MeasureTheory.VectorMeasure X F → (E →L[ℝ] F →L[ℝ] G) → Set X → E →L[ℝ] G
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- An index type for the vertices of a simplex plus its circumcenter.
This is for use in calculations where it is convenient to work with
affine combinations of vertices together with the circumcenter.  (An
equivalent form sometimes used in the literature is placing the
circumcenter at the origin and working with vectors for the vertices.)  -/
Affine.Simplex.PointsWithCircumcenterIndex : ℕ → Type
-- Mathlib.Order.LiminfLimsup
Filter.frequently_lt_of_limsInf_lt : ∀ {α : Type u_1} {f : Filter α} [inst : ConditionallyCompleteLinearOrder α] {a : α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f) Filter.frequently_lt_of_limsInf_lt._auto_1 →
    f.limsInf < a → ∃ᶠ (n : α) in f, n < a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
/-- If `f` is monotone on `a..(b + c)` where `a ≤ b` and `0 ≤ c`, then the interval integral of
`fun x ↦ slope f x (x + c)` on `a..b` is at most `f (b + c) - f a`.  -/
MonotoneOn.intervalIntegral_slope_le : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  MonotoneOn f (Set.Icc a (b + c)) → a ≤ b → 0 ≤ c → ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.or_congr : ∀ (w : ℕ) (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' ||| rhs' = lhs ||| rhs
-- Lean.Environment
_private.Lean.Environment.0.Lean.ensureExtensionsArraySize : Lean.Environment → IO Lean.Environment
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.IsAffineOpen US →
    IsCompact ↑UT →
      IsQuasiSeparated ↑UT →
        IsCompact ↑UX →
          IsQuasiSeparated ↑UX →
            (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE iX US UX hUSX)).Flat →
              CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (toLaxFunctor : CategoryTheory.LaxFunctor B C) →
          (map_id :
              autoParam
                (∀ (X : B),
                  toLaxFunctor.map (CategoryTheory.CategoryStruct.id X) =
                    CategoryTheory.CategoryStruct.id (toLaxFunctor.obj X))
                CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam) →
            autoParam (∀ (X : B), toLaxFunctor.mapId X = CategoryTheory.eqToHom ⋯)
                CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam →
              CategoryTheory.StrictlyUnitaryLaxFunctor B C
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableEqOrdinal : DecidableEq Std.Time.Nanosecond.Ordinal
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instSMulNat : ∀ {L : Type u_2} {M : Type u_3} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M],
  LieDerivation.SMulBracketCommClass ℕ L M
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- the first map `R → L`  -/
CategoryTheory.Limits.MulticospanShape.fst : (self : CategoryTheory.Limits.MulticospanShape) → self.R → self.L
-- Init.Data.UInt.Basic
/-- Strict inequality of 16-bit unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `<` operator.
 -/
UInt16.lt : UInt16 → UInt16 → Prop
-- Init.Data.SInt.Lemmas
Int64.div_self : ∀ {a : Int64}, a / a = if a = 0 then 0 else 1
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm_ιMulti_ιMulti : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x y : Fin n → E),
  (exteriorPower.innerProductForm✝ ((exteriorPower.ιMulti ℝ n) x)) ((exteriorPower.ιMulti ℝ n) y) =
    (Matrix.of fun i j => inner ℝ (x j) (y i)).det
-- Mathlib.Combinatorics.Digraph.Basic
/-- Two vertices are adjacent in the complete bipartite digraph on two vertex types
if and only if they are not from the same side.
Any bipartite digraph may be regarded as a subgraph of one of these.
 -/
Digraph.completeBipartiteGraph : (V : Type u_1) → (W : Type u_2) → Digraph (V ⊕ W)
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Destructor for the constant functor  -/
MvPFunctor.const.get : {n : ℕ} → {A : Type u} → {α : TypeVec.{u} n} → ↑(MvPFunctor.const n A) α → A
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.MinFacHelper.one_lt : ∀ {n k : ℕ}, Mathlib.Meta.NormNum.MinFacHelper n k → 1 < n
-- Mathlib.Data.Int.Fib.Basic
/-- The Fibonacci sequence for integers. This satisfies `fib 0 = 0`, `fib 1 = 1`,
`fib (n + 2) = fib n + fib (n + 1)`.

This is an extension of `Nat.fib`.  -/
Int.fib : ℤ → ℤ
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.sum_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C}
  {J : Type u_1} (s : Finset J) (f : J → (P ⟶ Q)) (g : Q ⟶ R) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (∑ j ∈ s, f j) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) g) h
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.inner_toCLM_conjTranspose_left : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] {M : CStarMatrix m n A}
  {v : WithCStarModule A (n → A)} {w : WithCStarModule A (m → A)},
  inner A ((CStarMatrix.toCLM (Matrix.conjTranspose M)) v) w = inner A v ((CStarMatrix.toCLM M) w)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_trim : ∀ {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {β : Type u_6} {m m0 : MeasurableSpace β}
  {μ : MeasureTheory.Measure β} (hm : m ≤ m0) {f : β → G},
  MeasureTheory.StronglyMeasurable f → ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
-- Mathlib.Data.Option.NAry
Option.map₂_coe_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : Option β),
  Option.map₂ f (some a) b = Option.map (fun b => f a b) b
-- Lean.Data.Lsp.CodeActions
/-- Whether the client honors the change annotations in
text edits and resource operations returned via the
`CodeAction#edit` property by for example presenting
the workspace edit in the user interface and asking
for confirmation.  -/
Lean.Lsp.CodeActionClientCapabilities.honorsChangeAnnotations? : Lean.Lsp.CodeActionClientCapabilities → Option Bool
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotation by 0 is the identity.  -/
Orientation.rotation_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)), o.rotation 0 = LinearIsometryEquiv.refl ℝ V
-- Mathlib.Data.Setoid.Partition
/-- If x ∈ α is in 2 elements of a set of sets partitioning α, those 2 sets are equal.  -/
Setoid.eq_of_mem_eqv_class : ∀ {α : Type u_1} {c : Set (Set α)},
  (∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) → ∀ {x : α} {b b' : Set α}, b ∈ c → x ∈ b → b' ∈ c → x ∈ b' → b = b'
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.instImplicit.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.PatternArgKind.instImplicit = 1
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {t : Finset (α × β × γ)} →
        [DecidableEq α] →
          [DecidableEq β] → [DecidableEq γ] → DecidableRel (SimpleGraph.TripartiteFromTriangles.graph t).Adj
-- Mathlib.Data.Set.Monotone
strictAntiOn_insert_iff_of_forall_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  (∀ x ∈ s, x ≤ a) → (StrictAntiOn f (insert a s) ↔ (∀ b ∈ s, b < a → f a < f b) ∧ StrictAntiOn f s)
-- Mathlib.Algebra.RingQuot
RingQuot.one_quot : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), { toQuot := Quot.mk (RingQuot.Rel r) 1 } = 1
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.toArray_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β} {pos : ℕ},
  (array.iterFromIdxM m pos).toArray = pure (array.extract pos)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.left_ne_right_iff_radius_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → (p₁ ≠ p₂ ↔ 0 < s.radius)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.isLittleO_of_lt_exps : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {t1 t2 : Tactic.ComputeAsymptotics.Monomial},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length t1.unit = List.length basis →
      List.length t2.unit = List.length basis →
        t2.coef ≠ 0 → t1.unit < t2.unit → t1.toFun basis =o[Filter.atTop] t2.toFun basis
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.pairwise_commute_of_mem_zpowers : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α),
  Pairwise fun i j => ∀ (x y : Equiv.Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Commute x y
-- Mathlib.Algebra.Group.Prod
Prod.instMulOneClass : {M : Type u_3} → {N : Type u_4} → [MulOneClass M] → [MulOneClass N] → MulOneClass (M × N)
-- Std.Time.Format.Modifier
Std.Time.Modifier.k.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.k presentation = Std.Time.Modifier.k presentation_1 → presentation = presentation_1
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.re_neg : ∀ (z : Complex.UnitClosedDisc), (-z).re = -z.re
-- Std.Time.Format.Modifier
Std.Time.Modifier.E.inj : ∀ {presentation presentation_1 : Std.Time.Text},
  Std.Time.Modifier.E presentation = Std.Time.Modifier.E presentation_1 → presentation = presentation_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv_assoc : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)]
  (g : CategoryTheory.CostructuredArrow L Y) {Z : H} (h_1 : (CategoryTheory.StructuredArrow.right E).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y).comp F) g)
      (CategoryTheory.CategoryStruct.comp h.isoColimit.inv h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
        ((CategoryTheory.StructuredArrow.right E).map g.hom))
      h_1
-- Mathlib.RingTheory.Smooth.Basic
/-- Given extensions `0 → I₁ → P₁ → A → 0` and `0 → I₂ → P₂ → A → 0` with `P₁` formally smooth,
this is an arbitrarily chosen map `P₁/I₁² → P₂/I₂²` of extensions.
 -/
Algebra.Extension.homInfinitesimal : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (P₁ : Algebra.Extension R A) →
            (P₂ : Algebra.Extension R A) → [Algebra.FormallySmooth R P₁.Ring] → P₁.infinitesimal.Hom P₂.infinitesimal
-- Mathlib.Algebra.Group.Shrink
/-- Shrink `α` to a smaller universe preserves addition.  -/
Shrink.addEquiv : {α : Type u_2} → [inst : Small.{v, u_2} α] → [inst_1 : Add α] → Shrink.{v, u_2} α ≃+ α
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The inclusion of the bounded above derived category.  -/
DerivedCategory.Minus.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Functor (DerivedCategory.Minus C) (DerivedCategory C)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.swap.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.swap A B = (ContinuousAddMonoidHom.snd A B).prod (ContinuousAddMonoidHom.fst A B)
-- Mathlib.Topology.Order
mem_nhds_induced : ∀ {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β),
  s ∈ nhds a ↔ ∃ u ∈ nhds (f a), f ⁻¹' u ⊆ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_Z : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.dblXYZ P 2 = W'.dblZ P
-- Init.Data.SInt.Lemmas
Int64.le_or_lt : ∀ (a b : Int64), a ≤ b ∨ b < a
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (toEquiv : α ≃ β)
  (isometry_toFun : Isometry toEquiv.toFun) (toEquiv_1 : α ≃ β) (isometry_toFun_1 : Isometry toEquiv_1.toFun),
  ({ toEquiv := toEquiv, isometry_toFun := isometry_toFun } =
      { toEquiv := toEquiv_1, isometry_toFun := isometry_toFun_1 }) =
    (toEquiv = toEquiv_1)