mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.RelIso.Basic
/-- Identity map is a relation homomorphism.  -/
RelHom.id : {α : Type u_1} → (r : α → α → Prop) → r →r r
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.node.inj : ∀ {α : Type} {vs : Array α} {children : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)} {vs_1 : Array α}
  {children_1 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)},
  Lean.Meta.DiscrTree.Trie.node vs children = Lean.Meta.DiscrTree.Trie.node vs_1 children_1 →
    vs = vs_1 ∧ children = children_1
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.sub : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x y : A},
  IsIntegral R x → IsIntegral R y → IsIntegral R (x - y)
-- Mathlib.Data.Fintype.EquivFin
Fintype.one_lt_card_iff : ∀ {α : Type u_1} [inst : Fintype α], 1 < Fintype.card α ↔ ∃ a b, a ≠ b
-- Init.Data.List.Find
List.idxOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α), List.idxOf? a = List.findIdx? fun x => x == a
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_natCast : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NatCast F] (n : ℕ), deriv ↑n = 0
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_sub : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  (x y : ↥p), ↑(x - y) = ↑x - ↑y
-- Init.Data.UInt.Lemmas
UInt16.mod_zero : ∀ {a : UInt16}, a % 0 = a
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A function has locally bounded variation on a set `s` if, given any interval `[a, b]` with
endpoints in `s`, then the function has finite variation on `s ∩ [a, b]`.  -/
LocallyBoundedVariationOn : {α : Type u_1} → [LinearOrder α] → {E : Type u_2} → [PseudoEMetricSpace E] → (α → E) → Set α → Prop
-- Mathlib.Logic.Function.Basic
Function.apply_invFun_apply : ∀ {α : Type u_3} {β : Type u_4} {f : α → β} {a : α}, f (Function.invFun f (f a)) = f a
-- Lean.Compiler.IR.CompilerM
Lean.IR.addDecls : Array Lean.IR.Decl → Lean.IR.CompilerM Unit
-- Init.GetElem
/-- The classes `GetElem` and `GetElem?` implement lookup notation,
specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.

Both classes are indexed by types `coll`, `idx`, and `elem` which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation `valid` determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.

For example, an instance for arrays looks like
`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
holds, which is true when `i` is less than the size of the array. `Array`
additionally supports indexing with `USize` instead of `Nat`.
In either case, because the bounds are checked at compile time,
no runtime check is required.

Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
`GetElem coll idx elem valid` and uses this to infer the type of the return
value `elem` and side condition `valid` required to ensure `xs[i]` yields
a valid value of type `elem`. The tactic `get_elem_tactic` is
invoked to prove validity automatically. The `xs[i]'p` notation uses the
proof `p` to satisfy the validity condition.
If the proof `p` is long, it is often easier to place the
proof in the context using `have`, because `get_elem_tactic` tries
`assumption`.


The proof side-condition `valid xs i` is automatically dispatched by the
`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
`get_elem_tactic_extensible` using `macro_rules`.

`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
an `Option elem`, with `none` signalling that the value isn't present, and
the latter returns `elem` but panics if the value isn't there, returning
`default : elem` based on the `Inhabited elem` instance.
These are provided by the `GetElem?` class, for which there is a default instance
generated from a `GetElem` class as long as `valid xs i` is always decidable.

Important instances include:
  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
    side goal `i < l.length`.

 -/
GetElem : (coll : Type u) → (idx : Type v) → outParam (Type w) → outParam (coll → idx → Prop) → Type (max (max u v) w)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.unitsWithZeroEquiv_apply : ∀ {α : Type u_1} [inst : Group α] (a : (WithZero α)ˣ), WithZero.unitsWithZeroEquiv a = WithZero.unzero ⋯
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
Submodule.exists_linearEquiv_restrict_eq : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {W W' : Submodule K V} [FiniteDimensional K ↥W] (f : ↥W ≃ₗ[K] ↥W'), ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- Let `s ⊆ X`. Suppose that `X` is Hausdorff, and that to prove that `s` is closed,
it suffices to show that for every compact set `K ⊆ X`, `s ∩ K` is closed.
Then `X` is compactly generated.  -/
compactlyGeneratedSpace_of_isClosed_of_t2 : ∀ {X : Type u} [inst : TopologicalSpace X] [T2Space X],
  (∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s) → CompactlyGeneratedSpace X
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.filterMap_equiv_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → β → Bool},
  m.WF → (Std.HashMap.Raw.filterMap (fun k => Option.guard fun v => f k v) m).Equiv (Std.HashMap.Raw.filter f m)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inr_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.snd X Y) h) =
    h
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_const_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c : ε},
  autoParam (‖c‖ₑ ≠ ⊤) intervalIntegrable_const_iff._auto_1 →
    (IntervalIntegrable (fun x => c) μ a b ↔ c = 0 ∨ μ (Set.uIoc a b) < ⊤)
-- Mathlib.Topology.Order.Basic
pi_Iic_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i},
  (∀ (i : ι), x i < a i) → Set.Iic a ∈ nhds x
-- Lean.Elab.Tactic.Grind.Basic
/-- Backtracking `try`/`catch`. This is used for the `MonadExcept` instance for `GrindTacticM`.
 -/
Lean.Elab.Tactic.Grind.tryCatchRestore : {α : Type} →
  Lean.Elab.Tactic.Grind.GrindTacticM α →
    (Lean.Exception → Lean.Elab.Tactic.Grind.GrindTacticM α) → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `leftToMax j j'` is an arbitrary choice of morphism from `j` to `max j j'`,
whose existence is ensured by `IsFiltered`.
 -/
CategoryTheory.IsFiltered.leftToMax : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] → (j j' : C) → j ⟶ CategoryTheory.IsFiltered.max j j'
-- Mathlib.Analysis.Normed.Group.Basic
abs_norm_sub_norm_le' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), |‖a‖ - ‖b‖| ≤ ‖a / b‖
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.mapπ₀_mk : ∀ {X Y : SSet} (f : X ⟶ Y) (x₀ : X.obj (Opposite.op { len := 0 })),
  SSet.mapπ₀ f (SSet.π₀.mk x₀) =
    SSet.π₀.mk ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₀)
-- Mathlib.GroupTheory.OreLocalization.Cardinality
OreLocalization.oreDiv_one_surjective_of_finite_left : ∀ {R : Type u} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] (X : Type v)
  [inst_2 : MulAction R X] [Finite ↥S], Function.Surjective fun x => x /ₒ 1
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Iic : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], (Finset.Iic a).Nonempty
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The sphere of radius `r = ‖y‖` is tangent to the plane `⟪x, y⟫ = ‖y‖ ^ 2` at `x = y`.  -/
eq_of_norm_le_re_inner_eq_norm_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, ‖x‖ ≤ ‖y‖ → RCLike.re (inner 𝕜 x y) = ‖y‖ ^ 2 → x = y
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mem_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  {s : TopologicalSpace.Closeds α} {t : TopologicalSpace.Closeds β} {x : α × β}, x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_le : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {U : NonUnitalSubalgebra R B},
  NonUnitalSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalSubalgebra.comap f U
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.HasPluralDefaults.plural : {α : Sort u_1} → [self : Lean.HasPluralDefaults✝ α] → α → α
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `norm_le_norm_add_norm_sub`. -/
norm_le_insert : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (u v : E), ‖v‖ ≤ ‖u‖ + ‖u - v‖
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddCommMonoid : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddCommMonoid α] → AddCommMonoid (Shrink.{v, u_2} α)
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.Config.mk : Mathlib.Tactic.AtomM.Recurse.Config →
  Mathlib.Tactic.BehaviorIfUnchanged → Mathlib.Tactic.RingNF.RingMode → Mathlib.Tactic.RingNF.Config
-- Mathlib.Order.Rel.GaloisConnection
/-- `rightFixedPoints` is the set of elements `I : Set β` satisfying `leftDual (rightDual I) = I`.
 -/
SetRel.rightFixedPoints : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set (Set β)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))]
  {Z : C}
  (h :
    CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inl g₁
        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl
          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
        h)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.mk : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} {h : x ⟶ c},
  Nonempty ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan →
    CategoryTheory.Bicategory.LanLift.CommuteWith f g h
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.liftOfIsRightKanExtension.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : L.comp F' ⟶ F) (e_α : α = α_1) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H)
  (β β_1 : L.comp G ⟶ F), β = β_1 → F'.liftOfIsRightKanExtension α G β = F'.liftOfIsRightKanExtension α_1 G β_1
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.mk.sizeOf_spec : ∀ {α : Type u_7} [inst : SizeOf α] (MeasurableSet' : Set α → Prop) (measurableSet_empty : MeasurableSet' ∅)
  (measurableSet_compl : ∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ)
  (measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)),
  sizeOf
      { MeasurableSet' := MeasurableSet', measurableSet_empty := measurableSet_empty,
        measurableSet_compl := measurableSet_compl, measurableSet_iUnion := measurableSet_iUnion } =
    1 + sizeOf measurableSet_empty
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.Cauchy.limit.congr_simp : ∀ {K : Type u_2} [inst : Field K] {ℱ ℱ_1 : Filter (LaurentSeries K)} (e_ℱ : ℱ = ℱ_1) (hℱ : Cauchy ℱ),
  LaurentSeries.Cauchy.limit hℱ = LaurentSeries.Cauchy.limit ⋯
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_abs : ∀ (b x : ℝ), Real.logb b |x| = Real.logb b x
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.trajFun.eq_1 : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
  ProbabilityTheory.Kernel.trajFun κ a x₀ = (ProbabilityTheory.Kernel.trajContent κ x₀).measure ⋯ ⋯ ⋯
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinCLM_eq_setIntegral : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.IntegrableOn φ (↑K) μ →
    ∀ {f : ContDiffMapSupportedIn E F₁ n K},
      (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f = ∫ (x : E) in ↑K, (B (f x)) (φ x) ∂μ
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.hasseDeriv_single : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k : ℕ) (n : ℤ)
  (x : V), (LaurentSeries.hasseDeriv R k) ((HahnSeries.single n) x) = (HahnSeries.single (n - ↑k)) (Ring.choose n k • x)
-- Mathlib.Algebra.FreeMonoid.Basic
_private.Mathlib.Algebra.FreeMonoid.Basic.0.FreeAddMonoid.sumAux.match_1.splitter : {M : Type u_1} →
  (motive : List M → Sort u_2) →
    (x : List M) → (Unit → motive []) → ((x : M) → (xs : List M) → motive (x :: xs)) → motive x
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g +ᵥ s, f x ∂μ
-- Mathlib.Order.Filter.CardinalInter
Filter.eventually_cardinal_ball : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι},
  Cardinal.mk ↑S < c →
    ∀ {p : α → (i : ι) → i ∈ S → Prop},
      (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.tendstoInMeasure_of_ne_top : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  {f : ι → α → E} {l : Filter ι} {g : α → E},
  (∀ (ε : ENNReal), 0 < ε → ε ≠ ⊤ → Filter.Tendsto (fun i => μ {x | ε ≤ edist (f i x) (g x)}) l (nhds 0)) →
    MeasureTheory.TendstoInMeasure μ f l g
-- Mathlib.Data.Nat.BitIndices
Nat.mem_bitIndices : ∀ {i n : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a space with second countable topology and a sigma-finite measure, a measurable function
is `FinStronglyMeasurable`.  -/
MeasureTheory.finStronglyMeasurable_of_measurable : ∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ], Measurable f → MeasureTheory.FinStronglyMeasurable f μ
-- Mathlib.Data.EReal.Operations
EReal.sub_pos : ∀ {x y : EReal}, 0 < x - y ↔ y < x
-- Lean.Data.Lsp.Basic
Lean.Lsp.SnippetString.mk.sizeOf_spec : ∀ (value : String), sizeOf { value := value } = 1 + sizeOf value
-- Plausible.Testable
Plausible.Imp.printableProp : {x y : Prop} → [Plausible.PrintableProp x] → [Plausible.PrintableProp y] → Plausible.PrintableProp (x → y)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- A continuous function on a compact space is automatically a bounded continuous function.  -/
BoundedContinuousFunction.mkOfCompact : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] → [CompactSpace α] → C(α, β) → BoundedContinuousFunction α β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.inc.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {n : ℕ} {check persistent : Bool}
  {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_15} {fvarId_1 : Lean.FVarId}
  {n_1 : ℕ} {check_1 persistent_1 : Bool} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_15},
  Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h =
      Lean.Compiler.LCNF.Code.inc fvarId_1 n_1 check_1 persistent_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ k = k_1
-- Mathlib.Combinatorics.Graph.Maps
/-- **Alias** of `Graph.IsSubgraph.map`. -/
Graph.map_mono : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G H : Graph α β} (f : α → α'), G ≤ H → Graph.map f G ≤ Graph.map f H
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- A function `f : α → ℚ → ℝ` is a (kernel) rational cumulative distribution function if it is
measurable in the first argument and if `f a` satisfies a list of properties for all `a : α`:
monotonicity between 0 at -∞ and 1 at +∞ and a form of continuity.

A function with these properties can be extended to a measurable function `α → StieltjesFunction ℝ`.
See `ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction`.
 -/
ProbabilityTheory.IsMeasurableRatCDF : {α : Type u_1} → [MeasurableSpace α] → (α → ℚ → ℝ) → Prop
-- Init.Data.List.MinMaxIdx
List.isSome_minIdxOn?_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {x : α},
  x ∈ xs → (List.minIdxOn? f xs).isSome = true
-- Init.Grind.Norm
Lean.Grind.Int.pow_one : ∀ (a : ℤ), a ^ 1 = a
-- Mathlib.Lean.Name
/-- Retrieve all names in the environment satisfying a predicate,
gathered together into a `HashMap` according to the module they are defined in.
 -/
allNamesByModule : (Lean.Name → Bool) → Lean.CoreM (Std.HashMap Lean.Name (Array Lean.Name))
-- Mathlib.Control.Traversable.Basic
Traversable.toFunctor : {t : Type u → Type u} → [self : Traversable t] → Functor t
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The cofan for `summand s.N Δ` induced by a splitting of a simplicial object.  -/
CategoryTheory.SimplicialObject.Splitting.cofan : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        (Δ : SimplexCategoryᵒᵖ) → CategoryTheory.Limits.Cofan (CategoryTheory.SimplicialObject.Splitting.summand s.N Δ)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.pUnitAlgEquiv_symm_monomial : ∀ (R : Type u) [inst : CommSemiring R] {d : PUnit.{1} →₀ ℕ} {r : R},
  (MvPolynomial.pUnitAlgEquiv R).symm ((Polynomial.monomial (d ())) r) = (MvPolynomial.monomial d) r
-- Mathlib.Data.Setoid.Partition
/-- If x ∈ α is in 2 equivalence classes, the equivalence classes are equal.  -/
Setoid.eq_of_mem_classes : ∀ {α : Type u_1} {r : Setoid α} {x : α} {b : Set α},
  b ∈ r.classes → x ∈ b → ∀ {b' : Set α}, b' ∈ r.classes → x ∈ b' → b = b'
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonadFinally : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → [MonadFinally m] → MonadFinally (Lean.MonadStateCacheT α β m)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_ringHom_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective RingHomClass.toRingHom
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.forCodeM : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] → Lean.Compiler.LCNF.Alt pu → (Lean.Compiler.LCNF.Code pu → m Unit) → m Unit
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.sUnion : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : Set (Set M)},
  S.Finite → (∀ s ∈ S, IsSemilinearSet s) → IsSemilinearSet (⋃₀ S)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Left unitality of the enriched structure  -/
CategoryTheory.MonoidalClosed.id_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y : C)
  [inst_2 : CategoryTheory.Closed x],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (x ⟹ y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalClosed.id x) (x ⟹ y))
        (CategoryTheory.MonoidalClosed.comp x x y)) =
    CategoryTheory.CategoryStruct.id (x ⟹ y)
-- Init.Data.String.Defs
String.utf8EncodeChar_ne_nil : ∀ {c : Char}, String.utf8EncodeChar c ≠ []
-- Std.Time.Time.Unit.Millisecond
/-- Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
 -/
Std.Time.Millisecond.Ordinal.ofNat : (data : ℕ) → data ≤ 999 → Std.Time.Millisecond.Ordinal
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_eq_bot_iff : ∀ {R : Type u_1} [inst : Semiring R] {f : LaurentPolynomial R}, f.degree = ⊥ ↔ f = 0
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_eq_one_iff : ∀ {n : ℕ}, n.minFac = 1 ↔ n = 1
-- Mathlib.Data.Multiset.UnionInter
Multiset.add_eq_union_left_of_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, t ≤ s → (u + s = u ∪ t ↔ Disjoint u s ∧ s = t)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
cmp.congr_simp : ∀ {α : Type u} [inst : LT α] {inst_1 : DecidableLT α} [inst_2 : DecidableLT α] (a a_1 : α),
  a = a_1 → ∀ (b b_1 : α), b = b_1 → cmp a b = cmp a_1 b_1