mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.mono_null : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} ⦃s t : Set α⦄, s ⊆ t → μ t = 0 → μ s = 0
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.const.inj : ∀ {α : Type} {a a_1 : Bool}, Std.Tactic.BVDecide.BoolExpr.const a = Std.Tactic.BVDecide.BoolExpr.const a_1 → a = a_1
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Sort u_3) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size)
  (h_1 :
    (size : ℕ) →
      (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β)) →
        (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
          motive ⟨{ size := size, buckets := buckets }, hm⟩),
  (match ⟨{ size := size, buckets := buckets }, hm⟩ with
    | ⟨{ size := size, buckets := buckets }, hm⟩ => h_1 size buckets hm) =
    h_1 size buckets hm
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mul_left : ∀ {R : Type u} [inst : Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R},
  U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x₀ * x) ⁻¹' U
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_coe_pi : (↑Real.pi).cos = -1
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_subset_closure : ∀ {α : Type u_2} {X Y : Set α} (M : Matroid α), X ⊆ Y → M.closure X ⊆ M.closure Y
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Same as `partialTraj_comp_partialTraj` but only assuming `a ≤ b`. It requires Markov kernels.  -/
ProbabilityTheory.Kernel.partialTraj_comp_partialTraj' : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (c : ℕ),
  a ≤ b →
    (ProbabilityTheory.Kernel.partialTraj κ b c).comp (ProbabilityTheory.Kernel.partialTraj κ a b) =
      ProbabilityTheory.Kernel.partialTraj κ a c
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.beq' : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Data.Set.Finite.Lattice
Set.finite_iUnion : ∀ {α : Type u} {ι : Sort w} [Finite ι] {f : ι → Set α}, (∀ (i : ι), (f i).Finite) → (⋃ i, f i).Finite
-- Mathlib.Order.Bounded
Set.bounded_self : ∀ {α : Type u_1} {r : α → α → Prop} (a : α), Set.Bounded r {b | r b a}
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Prod.borelSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α]
  [mβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β] [SecondCountableTopologyEither α β],
  BorelSpace (α × β)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciInf_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {a : α},
  BddBelow (Set.range f) → (a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_zero : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α}, Std.PRange.succMany 0 a = a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The `darts` of a walk is the list of darts it visits in order.  -/
SimpleGraph.Walk.darts : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → List G.Dart
-- Mathlib.Order.Interval.Finset.Defs
instSubsingletonLocallyFiniteOrder : ∀ {α : Type u_1} [inst : Preorder α], Subsingleton (LocallyFiniteOrder α)
-- Mathlib.Topology.Algebra.Module.Compact
IsNoetherianRing.isClosed_ideal : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [IsNoetherianRing R]
  [CompactSpace R] [T2Space R] (I : Ideal R), IsClosed ↑I
-- Lean.Declaration
Lean.ConstantInfo.quotInfo.inj : ∀ {val val_1 : Lean.QuotVal}, Lean.ConstantInfo.quotInfo val = Lean.ConstantInfo.quotInfo val_1 → val = val_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.ιPi.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right],
  CategoryTheory.Limits.Multiequalizer.ιPi I = CategoryTheory.Limits.Multiequalizer.ιPi I
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHAddOffset : HAdd Std.Time.PlainTime Std.Time.Nanosecond.Offset Std.Time.PlainTime
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.thinSkeleton_mk_representative_eq_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (A : CategoryTheory.Subobject X),
  CategoryTheory.ThinSkeleton.mk (CategoryTheory.Subobject.representative.obj A) = A
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- A family of `MvPowerSeries` in the form `1 + f i` is multipliable if the weighted order of `f i`
tends to infinity.  -/
MvPowerSeries.WithPiTopology.multipliable_one_add_of_tendsto_weightedOrder_atTop_nhds_top : ∀ {σ : Type u_3} {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {ι : Type u_5}
  {f : ι → MvPowerSeries σ R} [inst_2 : LinearOrder ι] [LocallyFiniteOrderBot ι] {w : σ → ℕ},
  Filter.Tendsto (fun i => MvPowerSeries.weightedOrder w (f i)) Filter.atTop (nhds ⊤) → Multipliable fun x => 1 + f x
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv.eq_1 : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] (μ : MeasureTheory.Measure G),
  μ.inv = MeasureTheory.Measure.map Inv.inv μ
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instToFormatTrie : {α : Type} → [Std.ToFormat α] → Std.ToFormat (Lean.Meta.DiscrTree.Trie α)
-- Init.Data.Rat.Lemmas
Rat.natCast_mul : ∀ (a b : ℕ), ↑(a * b) = ↑a * ↑b
-- Aesop.Util.UnorderedArraySet
/-- Precondition: `xs` is sorted.  -/
Aesop.UnorderedArraySet.ofSortedArray : {α : Type u_1} → [inst : BEq α] → Array α → Aesop.UnorderedArraySet α
-- Mathlib.Data.List.Dedup
List.Disjoint.union_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α}, xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.mem_Icc : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) {x : M} [inst_5 : FiniteDimensional ℝ E], ↑f x ∈ Set.Icc 0 1
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (f : G →+ G'),
  (AddSubgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Unexpander for `MonoidAlgebra`.  -/
MonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander
-- Lean.Elab.Attributes
Lean.Elab.Attribute.mk.injEq : ∀ (kind : Lean.AttributeKind) (name : Lean.Name) (stx : Lean.Syntax) (kind_1 : Lean.AttributeKind) (name_1 : Lean.Name)
  (stx_1 : Lean.Syntax),
  ({ kind := kind, name := name, stx := stx } = { kind := kind_1, name := name_1, stx := stx_1 }) =
    (kind = kind_1 ∧ name = name_1 ∧ stx = stx_1)
-- Init.Data.List.Lemmas
List.decide_exists_mem : ∀ {α : Type u_1} {l : List α} {p : α → Prop} [inst : DecidablePred p],
  decide (∃ x ∈ l, p x) = l.any fun b => decide (p b)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- [Stacks Tag 00I0](https://stacks.math.columbia.edu/tag/00I0) ((1)) -/
PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructible : ∀ {R : Type u_4} [inst : CommRing R] {s : Set (PrimeSpectrum R)},
  StableUnderGeneralization s → Topology.IsConstructible s → IsOpen s
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_normalCore : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [H.FiniteIndex], H.normalCore.FiniteIndex
-- Mathlib.Computability.DFA
DFA.comap.eq_1 : ∀ {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ),
  DFA.comap f M = { step := fun s a => M.step s (f a), start := M.start, accept := M.accept }
-- Mathlib.Analysis.Convex.Hull
convexHull_convexHull_union_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s t : Set E), (convexHull 𝕜) (s ∪ (convexHull 𝕜) t) = (convexHull 𝕜) (s ∪ t)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.prec : Nat.Partrec.Code → Nat.Partrec.Code → Nat.Partrec.Code
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLineRange : Lean.FromJson Lean.Lsp.LineRange
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- Compose two morphisms in a bicategorical category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.Bicategory.«term_⊗≫_» : Lean.TrailingParserDescr
-- Init.Core
Quotient.inductionOn₂ : ∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop}
  (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a : α) (b : β), motive ⟦a⟧ ⟦b⟧) → motive q₁ q₂
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skipWhile_cast : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  (pos.cast hst).skipWhile pat = (pos.skipWhile pat).cast hst
-- Mathlib.Data.Rat.Floor
Rat.isInt_intFloor_ofIsRat_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (r : α)
  (n d : ℕ),
  Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsInt ⌊r⌋ (Int.negOfNat (-(-↑n / ↑d)).toNat)
-- Mathlib.Algebra.Group.Defs
AddLeftCancelMonoid.mk : {M : Type u} → [toAddMonoid : AddMonoid M] → [toIsLeftCancelAdd : IsLeftCancelAdd M] → AddLeftCancelMonoid M
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.sdiff : ∀ {α : Type u} {s t : Set α}, s.Infinite → t.Finite → (s \ t).Infinite
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y).unop
      ((CategoryTheory.shiftFunctor C n).map
        (CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f).unop) =
    f.unop
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.instInhabitedScore.default : Lean.FuzzyMatching.Score✝
-- Init.Data.Order.MinMaxOn
max_apply : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : Max β]
  [Std.LawfulOrderLeftLeaningMax β] {f : α → β} {x y : α}, f x ⊔ f y = f (maxOn f x y)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey?_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {f : β → β} {km kmm : α} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ (hkm : Std.Internal.List.minKey? l = some km),
      (Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l)).get ⋯ = kmm → (kmm == km) = true
-- Init.Data.Char.Basic
Char.instDecidableLt : (a b : Char) → Decidable (a < b)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsLinearMap.with_bound : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsLinearMap 𝕜 f → ∀ (M : ℝ), (∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → IsBoundedLinearMap 𝕜 f
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  (LieAlgebra.IsKilling.rootSystem H).IsCrystallographic
-- Std.Data.DTreeMap.Raw.Basic
/-- Creates a new empty tree map. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree map. `simp` replaces
`empty` with `∅`.
 -/
Std.DTreeMap.Raw.empty : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp
-- Mathlib.NumberTheory.Divisors
Nat.Prime.divisors : ∀ {p : ℕ}, Nat.Prime p → p.divisors = {1, p}
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.transpose_permMatrix : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Zero R] [inst_2 : One R],
  (Equiv.Perm.permMatrix R σ).transpose = Equiv.Perm.permMatrix R σ⁻¹
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.instDecidableEqBicone : {J : Type u_1} → [DecidableEq J] → DecidableEq (CategoryTheory.Bicone J)
-- Mathlib.Data.Finset.Basic
Finset.disjoint_disjUnion_right : ∀ {α : Type u_1} {s t u : Finset α} (h : Disjoint t u), Disjoint s (t.disjUnion u h) ↔ Disjoint s t ∧ Disjoint s u
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_sdiv_union_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s₁ s₂ t₁ t₂ : Set β}, s₁ ∩ s₂ /ₛ (t₁ ∪ t₂) ⊆ s₁ /ₛ t₁ ∪ (s₂ /ₛ t₂)
-- Mathlib.Order.Filter.Defs
/-- The applicative sequentiation operation. This is not induced by the bind operation.  -/
Filter.seq : {α : Type u_1} → {β : Type u_2} → Filter (α → β) → Filter α → Filter β
-- Mathlib.Data.Prod.Basic
Function.Semiconj.swap_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β), Function.Semiconj Prod.swap (Prod.map f g) (Prod.map g f)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.skipWhile.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((nextCurr : s.Pos) → motive (some nextCurr)) → (Unit → motive none) → motive x
-- Mathlib.Data.ENat.Basic
/-- A version of `mul_top` where the RHS is stated as an `ite`  -/
ENat.mul_top' : ∀ {m : ℕ∞}, m * ⊤ = if m = 0 then 0 else ⊤
-- Std.Http.Protocol.H1
/-- Returns `true` when user-provided headers include body framing fields.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.hasFramingHeaders : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Bool
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.mk.inj : ∀ {C : Type u₁} {of of_1 : C}, { of := of } = { of := of_1 } → of = of_1