mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)) (x : α) (xs : List α),
  l = x :: xs →
    (match l with
      | [] => h_1 ()
      | x :: xs => h_2 x xs) ≍
      h_2 x xs
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insert_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v).size ≤ m.size + 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- If `G` preserves any pointwise right Kan extension of `F` along `L` at `c`, then it preserves
all of them.  -/
CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt.mk' : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (c : C) {E : L.RightExtension F} (hE : E.IsPointwiseRightKanExtensionAt c)
  (hGE : ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c),
  G.PreservesPointwiseRightKanExtensionAt F L c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TotallyBounded.neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {s : Set α},
  TotallyBounded s → TotallyBounded (-s)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RocSliceData α β → Std.Roc α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.inv_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [inst_6 : CategoryTheory.IsIso f],
  CategoryTheory.inv f.base = (CategoryTheory.inv f).base
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The short complex in `D` obtained by applying a functor `F : C ⥤ D` to a
short complex in `C`, assuming that `F` preserves zero morphisms.  -/
CategoryTheory.ShortComplex.map : {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.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            CategoryTheory.ShortComplex C →
              (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → CategoryTheory.ShortComplex D
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_sdiff_right : ∀ {α : Type u_1} {s t u : Set α}, s \ (t \ u) = s \ t ∪ s ∩ u
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.val_centralizer_smul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) (k : ↥(Subgroup.centralizer {g}))
  (c : ↥g.cycleFactorsFinset), ↑(k • c) = ↑k * ↑c * ↑k⁻¹
-- Mathlib.Data.Tree.Basic
/-- Do an action for every node of the tree.
Actions are taken in node -> left subtree -> right subtree recursive order.
This function is the `traverse` function for the `Traversable BinaryTree` instance.
 -/
BinaryTree.traverse : {m : Type u_1 → Type u_2} →
  [Applicative m] → {α : Type u_3} → {β : Type u_1} → (α → m β) → BinaryTree α → m (BinaryTree β)
-- Mathlib.Order.Fin.Basic
/-- `Fin.castAdd` as an `OrderEmbedding`.

`castAddEmb m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAddEmb` and `Fin.addNatEmb`.  -/
Fin.castAddOrderEmb : {n : ℕ} → (m : ℕ) → Fin n ↪o Fin (n + m)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.map.eq_1 : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f),
  CategoryTheory.MorphismProperty.Over.map Q hPf =
    CategoryTheory.MorphismProperty.Comma.mapRight (CategoryTheory.Functor.id T)
      (CategoryTheory.Discrete.natTrans fun x => f) ⋯
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (X : C) [inst_5 : CategoryTheory.Projective X],
  CategoryTheory.IsIso ((CategoryTheory.ProjectiveResolution.self X).fromLeftDerivedZero' F)
-- Lean.Meta.Hint
/-- "Monolithic" diff: shows a deletion of the entire existing source, followed by an insertion of the
entire suggestion.
 -/
Lean.Meta.Hint.DiffGranularity.all : Lean.Meta.Hint.DiffGranularity
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.hasFiniteMulSupport_fun_pow : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : α → M) {g : α → ℕ},
  Function.HasFiniteSupport g → Function.HasFiniteMulSupport fun a => f a ^ g a
-- Init.Data.Array.Lemmas
Array.eq_toArray : ∀ {α : Type u_1} {xs : Array α} {as : List α}, xs = as.toArray ↔ xs.toList = as
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_self : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M)
  [inst_5 : DecidableEq ι] {i j : ι}, i ≠ j → f (Function.update v i (v j)) = 0
-- Mathlib.Order.Hom.Lattice
InfHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β), (InfHom.id β).comp f = f
-- Mathlib.Algebra.Group.Subgroup.Map
/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use `MulEquiv.subgroupMap` for better definitional equalities.  -/
Subgroup.equivMapOfInjective : {G : Type u_1} →
  [inst : Group G] →
    {N : Type u_5} →
      [inst_1 : Group N] → (H : Subgroup G) → (f : G →* N) → Function.Injective ⇑f → ↥H ≃* ↥(Subgroup.map f H)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.card_roots_le : ∀ {R : Type u_1} {P : Cubic R} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R],
  P.roots.toFinset.card ≤ 3
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- The spine of an `n`-simplex in `X` is the path of edges of length `n` formed
by traversing in order through the vertices of `X _⦋n⦌ₙ₊₁`.  -/
SSet.spine : (X : SSet) → (n : ℕ) → X.obj (Opposite.op { len := n }) → X.Path n
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, returning `none` if no such element exists.
 -/
Std.TreeSet.Raw.getLE? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Option α
-- Mathlib.Order.CompleteLattice.Basic
Prod.fst_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α × β),
  (iInf f).1 = ⨅ i, (f i).1
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyEq.countable_iInter`. -/
EventuallyEq.countable_iInter : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → ⋂ i, s i =ᶠ[l] ⋂ i, t i
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum may be split into a subtraction of affine combinations over two subsets.  -/
Finset.affineCombination_sdiff_sub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
  s₂ ⊆ s →
    ∀ (w : ι → k) (p : ι → P),
      (Finset.affineCombination k (s \ s₂) p) w -ᵥ (Finset.affineCombination k s₂ p) (-w) = (s.weightedVSub p) w
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.acc_of_single_erase : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop}
  [inst_1 : DecidableEq ι] {x : Π₀ (i : ι), α i} (i : ι),
  (Acc (DFinsupp.Lex r s) fun₀ | i => x i) → Acc (DFinsupp.Lex r s) (DFinsupp.erase i x) → Acc (DFinsupp.Lex r s) x
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.derivative_iterate_coeff : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k : ℕ)
  (f : LaurentSeries V) (n : ℤ),
  ((⇑(LaurentSeries.derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)
-- Mathlib.Data.Set.Card
/-- We can shrink a set to any smaller size.  -/
Set.exists_subset_card_eq : ∀ {α : Type u_1} {s : Set α} {n : ℕ}, n ≤ s.ncard → ∃ t ⊆ s, t.ncard = n
-- Mathlib.Data.NNReal.Basic
NNReal.coe_list_sum : ∀ (l : List NNReal), ↑l.sum = (List.map NNReal.toReal l).sum
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.inv_hom_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (e : A ≅ B) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_neg : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (p p' : Lean.Grind.Linarith.Poly),
  (p' == p.mul (-1)) = true → Lean.Grind.Linarith.Poly.denote' ctx p ≠ 0 → Lean.Grind.Linarith.Poly.denote' ctx p' ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- Making this a global instance would make the typeclass search go in an infinite loop.  -/
CategoryTheory.Limits.hasPullback_symmetry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasPullback f g], CategoryTheory.Limits.HasPullback g f
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.preimage : ∀ {R : Type u_3} {X : Type u_5} {Y : Type u_6} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] {f : X → Y}
  {s : Set Y}, Convexity.IsAffineMap R f → Convexity.IsConvexSet R s → Convexity.IsConvexSet R (f ⁻¹' s)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedLocalTimeType : Inhabited Std.Time.TimeZone.LocalTimeType
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The tensor unit is a terminal object.  -/
CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.SemiCartesianMonoidalCategory C] →
      CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.eq_1 : ∀ {α : Type u_1} (M : Matroid α), M.IsCircuit = Minimal M.Dep
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toListRev_eq_toListRev_toIterM : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toListRev = it.toIterM.toListRev.run
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- If `S` is a formally unramified `R`-algebra, essentially of finite type, the diagonal is an
open immersion.  -/
Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.FormallyUnramified R S]
  [Algebra.EssFiniteType R S],
  AlgebraicGeometry.IsOpenImmersion
    (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      WeierstrassCurve.Projective.Point.toAffine W (W.add P Q) =
        WeierstrassCurve.Projective.Point.toAffine W P + WeierstrassCurve.Projective.Point.toAffine W Q
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerRight_id : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X Y : C),
  CategoryTheory.eHomWhiskerRight V (CategoryTheory.CategoryStruct.id X) Y = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), Function.Surjective WithAbs.ofAbs
-- Mathlib.Order.Closure
/-- Send an `x` to an element of the set of closed elements (by taking the closure).  -/
LowerAdjoint.toClosed : {α : Type u_1} →
  {β : Type u_4} → [inst : PartialOrder α] → [inst_1 : Preorder β] → {u : β → α} → (l : LowerAdjoint u) → α → ↑l.closed
-- Mathlib.Algebra.Ring.Parity
Nat.even_or_odd : ∀ (n : ℕ), Even n ∨ Odd n
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence holds if and only if all non-negative distances are the same.  -/
congruent_iff_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], Congruent v₁ v₂ ↔ ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_sSup_of_directedOn : ∀ {R : Type u} [inst : NonAssocSemiring R] {S : Set (Subsemiring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Init.Data.Fin.Lemmas
Fin.succ_zero_eq_one : ∀ {n : ℕ}, Fin.succ 0 = 1
-- Mathlib.Analysis.InnerProductSpace.Calculus
_private.Mathlib.Analysis.InnerProductSpace.Calculus.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.modifyM.eq_1 : ∀ {α : Type u} {m : Type u → Type u_1} [inst : Monad m] (xs : Array α) (i : ℕ) (f : α → m α),
  xs.modifyM i f =
    if h : i < xs.size then
      have v := xs[i];
      do
      let v ← f v
      pure (xs.set i v h)
    else pure xs
-- Init.Data.UInt.Bitwise
UInt16.toBitVec_and : ∀ (a b : UInt16), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trList_ne_consₗ : ∀ (l : List ℕ), ∀ x ∈ Turing.PartrecToTM2.trList l, x ≠ Turing.PartrecToTM2.Γ'.consₗ
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_hom_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).hom.hom₃ =
    CategoryTheory.CategoryStruct.id X₂
-- Init.Data.Option.Lemmas
Option.commutative_merge : ∀ {α : Type u_1} (f : α → α → α) [Std.Commutative f], Std.Commutative (Option.merge f)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A complete atomic Boolean algebra is a complete Boolean algebra
that is also completely distributive.

We take iSup_iInf_eq as the definition here,
and prove later on that this implies atomicity.
 -/
CompleteAtomicBooleanAlgebra : Type u → Type u
-- Mathlib.Order.Interval.Multiset
Multiset.left_mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∈ Multiset.Icc a b ↔ a ≤ b
-- Mathlib.AlgebraicGeometry.Group.Smooth
/-- If `G` is a group scheme over an algebraically closed field `k` that is reduced and locally
of finite type, then `G` is smooth over `k`.
 -/
_private.Mathlib.AlgebraicGeometry.Group.Smooth.0.AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed : ∀ {K : Type u} [inst : Field K] {G : AlgebraicGeometry.Scheme} (f : G ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [AlgebraicGeometry.LocallyOfFiniteType f] [CategoryTheory.GrpObj (CategoryTheory.Over.mk f)]
  [AlgebraicGeometry.IsReduced G] [IsAlgClosed K], AlgebraicGeometry.Smooth f
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.zero : ∀ (R : Type u_1) [inst : AddMonoid R] [inst_1 : StarAddMonoid R], IsSelfAdjoint 0
-- Mathlib.Data.Finset.Grade
Finset.isAtom_iff : ∀ {α : Type u_1} {s : Finset α}, IsAtom s ↔ ∃ a, s = {a}
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousNegCoe : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Neg (R i)]
  [inst_3 : ∀ (i : ι), NegMemClass (S i) (R i)] [∀ (i : ι), ContinuousNeg (R i)],
  ContinuousNeg (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Init.Data.List.Nat.TakeDrop
List.dropWhile_eq_drop_findIdx_not : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.dropWhile p xs = List.drop (List.findIdx (fun a => !p a) xs) xs
-- Lean.Expr
/-- Checks if an expression is a "natural number numeral in normal form",
i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
and if so returns `n`.
 -/
Lean.Expr.nat? : Lean.Expr → Option ℕ
-- Init.Data.OfScientific.Basic
/-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
Examples:
- `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
- `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`

Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
 -/
OfScientific : Type u → Type u
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addEntries.injEq : ∀ (entries entries_1 : Array Lean.Meta.SimpEntry),
  (Lean.Elab.Tactic.ElabSimpArgResult.addEntries entries = Lean.Elab.Tactic.ElabSimpArgResult.addEntries entries_1) =
    (entries = entries_1)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
/-- The balanced hull of `s` is minimal in the sense that it is contained in any balanced superset
`t` of `s`.  -/
Balanced.balancedHull_subset_of_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s t : Set E},
  Balanced 𝕜 t → s ⊆ t → balancedHull 𝕜 s ⊆ t
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)),
  (CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence F sq sq₃).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun D =>
        CategoryTheory.Pseudofunctor.DescentData'.isoMk
          (fun x => CategoryTheory.Iso.refl (((CategoryTheory.Functor.id (F.DescentData' sq sq₃)).obj D).obj x)) ⋯)
      ⋯
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagations.mk : Lean.Meta.Grind.PendingSolverPropagationsData✝ → Lean.Meta.Grind.PendingSolverPropagations
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.done.sizeOf_spec : ∀ (result : String), sizeOf (Std.Http.Internal.UnquoteState.done✝ result) = 1 + sizeOf result
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k k' fallback : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKeyD k' fallback =
        if compare k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Init.Data.Iterators.Basic
Std.Shrink.deflate_inj : ∀ {α : Type u_1} {x y : α}, Std.Shrink.deflate x = Std.Shrink.deflate y ↔ x = y
-- Mathlib.Order.Heyting.Hom
CoheytingHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toLatticeHom : LatticeHom α β) (map_top' : toLatticeHom.toFun ⊤ = ⊤)
  (map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b),
  sizeOf { toLatticeHom := toLatticeHom, map_top' := map_top', map_sdiff' := map_sdiff' } =
    1 + sizeOf toLatticeHom + sizeOf map_top'
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.todo : Lean.Meta.LazyDiscrTree.PartialMatch → Array Lean.Expr
-- Mathlib.Order.Fin.Basic
Fin.top_eq_zero : ∀ {n : ℕ} [inst : NeZero n], ⊤ = 0 ↔ n = 1
-- Mathlib.Dynamics.Flow
Flow.isInvariant_iff_image_eq : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddGroup τ]
  (ϕ : Flow τ α) (s : Set α), IsInvariant ϕ.toFun s ↔ ∀ (t : τ), ϕ.toFun t '' s = s
-- Mathlib.Algebra.Polynomial.Basic
/-- See also `Polynomial.sum_smul_index` for a version using multiplication on the RHS.  -/
Polynomial.sum_smul_index' : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} {T : Type u_2} [inst_1 : DistribSMul T R] [inst_2 : AddCommMonoid S]
  (p : Polynomial R) (b : T) (f : ℕ → R → S), (∀ (i : ℕ), f i 0 = 0) → (b • p).sum f = p.sum fun n a => f n (b • a)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.hasInlineAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instSMulSubtypeAEEqFunMemAddSubgroupLp : {M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : SMul M α] →
                [MeasureTheory.SMulInvariantMeasure M α μ] →
                  [MeasurableConstSMul M α] → SMul Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Data.PNat.Factors
/-- We can forget the primality property and regard a multiset
of primes as just a multiset of positive integers, or a multiset
of natural numbers.  In the opposite direction, if we have a
multiset of positive integers or natural numbers, together with
a proof that all the elements are prime, then we can regard it
as a multiset of primes.  The next block of results records
obvious properties of these coercions.
 -/
PrimeMultiset.toNatMultiset : PrimeMultiset → Multiset ℕ
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Nanosecond.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subNanoseconds : Std.Time.WallTime → Std.Time.Nanosecond.Offset → Std.Time.WallTime
-- Init.Data.Array.Lemmas
/-- Variant of `all_eq_true` in terms of membership rather than an array index.  -/
Array.all_eq_true' : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.all p = true ↔ ∀ x ∈ as, p x = true
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.isTable_singleton : ∀ {b : ByteArray}, 1 ≤ b.size → String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ b #[0]
-- Init.Data.UInt.Lemmas
UInt32.lt_iff_toBitVec_lt : ∀ {a b : UInt32}, a < b ↔ a.toBitVec < b.toBitVec