mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hasSum_int_oddKernel : ∀ (a : ℝ) {x : ℝ},
  0 < x → HasSum (fun n => (↑n + a) * Real.exp (-Real.pi * (↑n + a) ^ 2 * x)) (HurwitzZeta.oddKernel (↑a) x)
-- Init.Omega.Int
Lean.Omega.Fin.lt_of_not_le : ∀ {n : ℕ} {i j : Fin n}, ¬i ≤ j → j < i
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).inv.hom = α.inv.app c.pt
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_singleton_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∈ s → s ∩ {a} = {a}
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.prod_R : ∀ (ι : Type w), (CategoryTheory.Limits.MultispanShape.prod ι).R = ι
-- Mathlib.Order.Northcott
Northcott.finite_le : ∀ {α : Type u_1} {β : Type u_2} {h : α → β} {inst : LE β} [self : Northcott h] (b : β), {a | h a ≤ b}.Finite
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.mul_iInter₂_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Mul α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s * ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s * t i j
-- Mathlib.GroupTheory.Coset.Card
QuotientGroup.fintypeQuotientRightRel : {α : Type u_1} → [inst : Group α] → {s : Subgroup α} → [Fintype (α ⧸ s)] → Fintype (Quotient (QuotientGroup.rightRel s))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.isOfNatZero : Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Init.Omega.IntList
Lean.Omega.IntList.mul_get : ∀ (xs ys : Lean.Omega.IntList) (i : ℕ), (xs * ys).get i = xs.get i * ys.get i
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a * x) ⁻¹' Set.Ioo b c = Set.Ioo (b / a) (c / a)
-- Mathlib.Topology.UniformSpace.Defs
lift_nhds_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {x : α} {g : Set α → Filter β},
  Monotone g → (nhds x).lift g = (uniformity α).lift fun s => g (UniformSpace.ball x s)
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The algebra norm `algNormOfAlgEquiv` extends the norm on `K`.  -/
IsUltrametricDist.algNormOfAlgEquiv_extends : ∀ {K : Type u_1} [inst : NormedField K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K] (σ : Gal(L/K)) (x : K),
  (IsUltrametricDist.algNormOfAlgEquiv σ) ((algebraMap K L) x) = ‖x‖
-- Init.Data.Option.Lemmas
Option.get!_none : ∀ {α : Type u_1} [inst : Inhabited α], none.get! = default
-- Mathlib.Topology.Separation.Regular
ULift.instT5Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T5Space X], T5Space (ULift.{u_3, u_1} X)
-- Mathlib.Order.RelIso.Basic
RelIso.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : (a a_1 : α) → SizeOf (r a a_1)] [inst_3 : (a a_1 : β) → SizeOf (s a a_1)] (toEquiv : α ≃ β)
  (map_rel_iff' : ∀ {a b : α}, s (toEquiv a) (toEquiv b) ↔ r a b),
  sizeOf { toEquiv := toEquiv, map_rel_iff' := map_rel_iff' } = 1 + sizeOf toEquiv
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestImpl.throwExs : Lean.TSyntax `tactic → Array Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_comm : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a - b < c ↔ a - c < b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_add_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ),
  p.take (n + m) = ((p.take n).append ((p.drop n).take m)).copy ⋯ ⋯
-- Mathlib.NumberTheory.Padics.WithVal
/-- The `p`-adic integers are ring isomorphic to the integers of the uniform completion
of the rationals at the `p`-adic valuation.  -/
PadicInt.withValIntegersRingEquiv : {p : ℕ} → [inst : Fact (Nat.Prime p)] → ↥(Valued.integer (Rat.padicValuation p).Completion) ≃+* ℤ_[p]
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_nonempty_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {pt : DiscreteTiling.PlacedTile ps}, (↑pt).Nonempty ↔ (↑(↑ps pt.index)).Nonempty
-- Init.Data.Array.Lemmas
List.any_toArray : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.toArray.any p = l.any p
-- Mathlib.Algebra.Group.Hom.Defs
AddHomClass.toAddHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] (f : F), ↑f = { toFun := ⇑f, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.add_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R}
  (α β : u ⟶ v), (α + β).left = α.left + β.left
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F G : CategoryTheory.Functor C D} {x y : CategoryTheory.NatTrans F G}, x.app = y.app → x = y
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f) (s : TopologicalSpace.NonemptyCompacts α),
  ↑(TopologicalSpace.NonemptyCompacts.map f hf s) = f '' ↑s
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.mem_lt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o : WithBot α} {x : α},
  t.Bounded o ↑x → Ordnode.All (fun x_1 => x_1 < x) t
-- Mathlib.Algebra.Order.Group.Cone
instPartialOrderGroupCone : (G : Type u_1) → [inst : CommGroup G] → PartialOrder (GroupCone G)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp.eq_3 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.comp f k) =
    Turing.PartrecToTM2.codeSupp' f k ∪ Turing.PartrecToTM2.contSupp k
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.cokernelSequenceCycles f g fg h n).f = (X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
-- Mathlib.MeasureTheory.Order.UpperLower
IsLowerSet.null_frontier : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)}, IsLowerSet s → MeasureTheory.volume (frontier s) = 0
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.productive_tail : ∀ {α : Type u} (s : Stream'.WSeq α) [s.Productive], s.tail.Productive
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_single : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b : β i),
  ‖PiLp.single p i b‖ = ‖b‖
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symmEquiv_apply_apply : ∀ (P : Type u_9) (Q : Type u_10) [inst : Mul P] [inst_1 : Mul Q] (h : P ≃* Q) (a : Q),
  ((MulEquiv.symmEquiv P Q) h) a = h.symm a
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.OplaxTrans F G) {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom h)))))
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_list_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] (l : List (Matrix m n α)),
  l.sum.conjTranspose = (List.map Matrix.conjTranspose l).sum
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.ConnectedComponent.connected_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent), C.toSubgraph.Connected
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (Std.TreeMap.Raw.ofList l cmp).contains k = (List.map Prod.fst l).contains k
-- Mathlib.Algebra.Order.Monovary
antivaryOn_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn (-f) (-g) s ↔ AntivaryOn f g s
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- The measure of the whole space with respect to a finite measure, considered as `ℝ≥0`.  -/
MeasureTheory.measureUnivNNReal : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → NNReal
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Extract and remove the maximum element from the tree, if it exists.

```
split_max {1, 2, 3} = some ({1, 2}, 3)
split_max ∅ = none
```  -/
Ordnode.splitMax : {α : Type u_1} → Ordnode α → Option (Ordnode α × α)
-- Mathlib.CategoryTheory.Comma.Basic
/-- Extract the isomorphism between the left objects from an isomorphism in the comma category.  -/
CategoryTheory.Comma.leftIso : {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} → {X Y : CategoryTheory.Comma L₁ R₁} → (X ≅ Y) → (X.left ≅ Y.left)
-- Mathlib.FieldTheory.IsPerfectClosure
isPRadical_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ),
  IsPRadical i p ↔ (∀ (x : L), ∃ n y, i y = x ^ p ^ n) ∧ RingHom.ker i ≤ pNilradical K p
-- Mathlib.NumberTheory.SelbergSieve
/-- These are the terms that appear in the sum `S` in the main term of the fundamental theorem.

$$S = \sum_{l \mid P, l \le \sqrt{y}} g(l)$$  -/
BoundingSieve.selbergTerms : {s : BoundingSieve} → ArithmeticFunction ℝ
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.ext_spanning : ∀ {α : Type u_2} {M M' : Matroid α}, M.E = M'.E → (∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S) → M = M'
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.nonpos_add_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M},
  (∀ (x : α), f x ≤ 0) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm_conj : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_5} [inst : RCLike 𝕜] (f : α → 𝕜) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm ((starRingEnd (α → 𝕜)) f) p μ = MeasureTheory.eLpNorm f p μ
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instMaxOfSemilatticeSup : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [SemilatticeSup Y] → [inst_2 : Zero Y] → Max (Function.locallyFinsuppWithin U Y)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.inner_single_right : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A]
  [inst_8 : DecidableEq ι] (x : WithCStarModule A ((i : ι) → E i)) {i : ι} (y : E i),
  inner A x ((WithCStarModule.equiv A ((i : ι) → E i)).symm (Pi.single i y)) = inner A (x i) y
-- Aesop.Tree.Data
Aesop.MVarClusterData.goals : {Goal Rapp : Type} → Aesop.MVarClusterData Goal Rapp → Array (IO.Ref Goal)
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressEditFast : String → Lean.Lsp.InsertReplaceEdit → String
-- Init.Data.String.Lemmas.Basic
String.Pos.toSlice_nextn : ∀ {n : ℕ} {s : String} {p : s.Pos}, (p.nextn n).toSlice = p.toSlice.nextn n
-- Mathlib.LinearAlgebra.Eigenspace.Zero
IsNilpotent.charpoly_eq_X_pow_finrank : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Finite R M] [inst_5 : Module.Free R M] {φ : Module.End R M},
  IsNilpotent φ → LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M
-- Mathlib.Algebra.Group.ULift
ULift.mul : {α : Type u} → [Mul α] → Mul (ULift.{u_1, u} α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
-- Std.Http.Internal.IndexMultiMap
/-- Retrieves all values for the given key, or `none` if the key is absent.
 -/
Std.Internal.IndexMultiMap.getAll? : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → α → Option (Array β)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `lowerSemicontinuousWithinAt_iff_le_liminf`. -/
LowerSemicontinuousWithinAt.le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ]
  {f : α → γ}, LowerSemicontinuousWithinAt f s x → f x ≤ Filter.liminf f (nhdsWithin x s)
-- Init.Data.Int.OfNat
Int.Nonneg.mul : ∀ (a b : ℤ), a ≥ 0 → b ≥ 0 → a * b ≥ 0
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg_of_msb_true : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → x.toInt < 0
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.toContinuousMapₐ_apply_apply : ∀ {α : Type u} {γ : Type w} (𝕜 : Type u_1) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : NormedRing γ]
  [inst_3 : NormedAlgebra 𝕜 γ] (f : BoundedContinuousFunction α γ) (a : α),
  ((BoundedContinuousFunction.toContinuousMapₐ 𝕜) f) a = f a
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.instMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
  (f : 0 ⟶ X), CategoryTheory.Mono f
-- Mathlib.Util.Qq
/-- If `e` has type `Sort u` for some level `u`, return `u` and `e : Q(Sort u)`.  -/
Qq.getLevelQ : Lean.Expr → Lean.MetaM ((u : Lean.Level) × Q(Sort u))
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Iio_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ico a b ⊆ Finset.Iio b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_to_countable' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [Countable α] [inst_2 : MeasurableSpace β] {f : β → α},
  (∀ (x : α), MeasurableSet (f ⁻¹' {x})) → Measurable f
-- Mathlib.Algebra.GroupWithZero.Defs
CancelCommMonoidWithZero.mk.sizeOf_spec : ∀ {M₀ : Type u_2} [inst : SizeOf M₀] (toCommMonoidWithZero : CommMonoidWithZero M₀)
  (toIsLeftCancelMulZero : IsLeftCancelMulZero M₀),
  sizeOf { toCommMonoidWithZero := toCommMonoidWithZero, toIsLeftCancelMulZero := toIsLeftCancelMulZero } =
    1 + sizeOf toCommMonoidWithZero + sizeOf toIsLeftCancelMulZero
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzOnWith_iff_norm_inv_mul_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {s : Set E} {f : E → F}
  {C : NNReal}, LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
-- Init.Data.BitVec.Lemmas
BitVec.umulOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w), x.umulOverflow y = decide (x.toNat * y.toNat ≥ 2 ^ w)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The norm of the sum of two vectors equals the norm of their difference if and only if
the angle between them is π/2.  -/
InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  ‖x + y‖ = ‖x - y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftHomologyIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂) {Z : C}
  (h : S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.leftHomologyIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.leftHomologyIso.hom h)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instIsSMulApplyNatMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  IsSMulApply ℕ (ProbabilityTheory.Kernel α β) α (MeasureTheory.Measure β)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc : ∀ {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 D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : D}
  (h :
    e.functor.obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X))
          (e.inverse.obj (e.functor.obj Y))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (e.counitInv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
      (CategoryTheory.CategoryStruct.comp
        (e.functor.map (CategoryTheory.Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ e.functor X Y)
      (CategoryTheory.CategoryStruct.comp
        (e.functor.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))) h)
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context.mk : Lean.ExprSet → Lean.Meta.SplitKind → Lean.Meta.FindSplitImpl.Context
-- Mathlib.Data.Multiset.Count
Multiset.card_eq_countP_add_countP : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α),
  s.card = Multiset.countP p s + Multiset.countP (fun x => ¬p x) s
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_left_comm : ∀ (x y z : ℕ), x &&& (y &&& z) = y &&& (x &&& z)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.min?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Min α] [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.WF → t.keys.min? = t.minKey?
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceTo_eq_self_iff : ∀ {s : String.Slice} {p : s.Pos}, s.sliceTo p = s ↔ p = s.endPos
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.next_stop : ∀ {s : Substring.Raw}, s.Valid → s.next { byteIdx := s.bsize } = { byteIdx := s.bsize }
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.subsingleton_of_rank_adjoin_eq_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  (∀ (x : E), Module.rank F ↥F⟮x⟯ = 1) → Subsingleton (IntermediateField F E)
-- Mathlib.Order.Interval.Finset.Defs
/-- Given a finset on `α`, lift it to being a finset on `WithBot α`
using `WithBot.some` and then insert `⊥`.  -/
WithBot.insertBot : {α : Type u_1} → Finset α ↪o Finset (WithBot α)
-- Mathlib.Data.Finset.Preimage
Finset.preimage_subset : ∀ {α : Type u} {β : Type v} {f : α ↪ β} {s : Finset β} {t : Finset α}, s ⊆ Finset.map f t → s.preimage ⇑f ⋯ ⊆ t
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.natCast_apply : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : PseudoMetricSpace β] [inst_2 : NatCast β] (n : ℕ)
  (x : α), ↑n x = ↑n
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.map_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ]
  {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b')
  [inst_3 : p.IsHomLift f' φ'], p.IsHomLift g (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ')
-- Mathlib.Data.Sum.Order
Sum.Lex.denselyOrdered_of_noMaxOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMaxOrder α],
  DenselyOrdered (α ⊕ₗ β)
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.addCommute_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (m : α) (n : β), AddCommute ((OrderAddMonoidHom.inl α β) m) ((OrderAddMonoidHom.inr α β) n)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insert k v).getKey? k = some k
-- Mathlib.Order.Heyting.Basic
sup_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a ⊔ b) \ c = a \ c ⊔ b \ c
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionSemiHomClass.mk : ∀ {F : Type u_8} {M : outParam (Type u_9)} {N : outParam (Type u_10)} {φ : outParam (M → N)} {X : outParam (Type u_11)}
  {Y : outParam (Type u_12)} [inst : VAdd M X] [inst_1 : VAdd N Y] [inst_2 : FunLike F X Y],
  (∀ (f : F) (c : M) (x : X), f (c +ᵥ x) = φ c +ᵥ f x) → AddActionSemiHomClass F φ X Y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.enumMember : Lean.Lsp.CompletionItemKind