mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.ToNat
/-- Two finite cardinals are equal
iff they are equal their `Cardinal.toNat` projections are equal.  -/
Cardinal.toNat_inj_of_lt_aleph0 : ∀ {c d : Cardinal.{u}}, c < Cardinal.aleph0 → d < Cardinal.aleph0 → (Cardinal.toNat c = Cardinal.toNat d ↔ c = d)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.reverseAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (l r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match a :: l, r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_2 a l r
-- Mathlib.RingTheory.Ideal.Operations
Submodule.mem_smul_span_singleton : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Ideal R}
  [I.IsTwoSided] {m x : M}, x ∈ I • (R ∙ m) ↔ ∃ y ∈ I, y • m = x
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instMonoidalCategoryStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Grp C)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanDidOpenTextDocumentParams.toJson : Lean.Lsp.LeanDidOpenTextDocumentParams → Lean.Json
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
/-- A morphism `s : Spec (.of Ω) ⟶ S` where `Ω` is a separably closed field
defines a point for the small étale site of `S`.  -/
AlgebraicGeometry.Scheme.pointSmallEtale : {S : AlgebraicGeometry.Scheme} →
  {Ω : Type u} →
    [inst : Field Ω] → [IsSepClosed Ω] → (AlgebraicGeometry.Spec (CommRingCat.of Ω) ⟶ S) → S.smallEtaleTopology.Point
-- Init.Data.List.Find
List.findIdx?_map : ∀ {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {l : List β},
  List.findIdx? p (List.map f l) = List.findIdx? (p ∘ f) l
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piCongrRight_trans : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} {Ps : η → Type u_19} [inst : (j : η) → Add (Ms j)]
  [inst_1 : (j : η) → Add (Ns j)] [inst_2 : (j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j)
  (fs : (j : η) → Ns j ≃+ Ps j),
  (AddEquiv.piCongrRight es).trans (AddEquiv.piCongrRight fs) = AddEquiv.piCongrRight fun i => (es i).trans (fs i)
-- Std.Sync.CancellationContext
Std.CancellationContext.State.mk.sizeOf_spec : ∀ (tokens : Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare) (id : UInt64),
  sizeOf { tokens := tokens, id := id } = 1 + sizeOf tokens + sizeOf id
-- Lean.Elab.Command
Lean.Elab.Command.instMonadEnvCommandElabM : Lean.MonadEnv Lean.Elab.Command.CommandElabM
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mapComp_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.mapComp F G).inv.app X =
    (match X with
      | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of (G.obj (F.obj a)))
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.le_def : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, I ≤ J ↔ ∀ (U : ↑X.affineOpens), I.ideal U ≤ J.ideal U
-- Init.Data.BitVec.Lemmas
/-- Equation theorem for `Int.sub` when both arguments are `Int.ofNat`  -/
_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.ofNat_sub_ofNat_of_lt : ∀ {n m : ℕ}, n < m → ↑n - ↑m = -(↑(m - 1 - n) + 1)
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.specialLinearGroup_smul_def : ∀ {K : Type u_1} {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Field K] [inst_2 : Module K V]
  (g : SpecialLinearGroup K V) (D : Projectivization K V), g • D = SpecialLinearGroup.toLinearEquiv g • D
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_find?_of_lt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.lt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.find? (fun x => k x.fst == Ordering.eq) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        List.find? (fun x => k x.fst == Ordering.eq) l.toListModel
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
Field.instIsTopologicalGroupAbsoluteGaloisGroup : ∀ (K : Type u_1) [inst : Field K], IsTopologicalGroup (Field.absoluteGaloisGroup K)
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
_private.Mathlib.LinearAlgebra.TensorProduct.DirectLimit.0.«term_▷_» : Lean.TrailingParserDescr
-- Aesop.Script.CtorNames
Aesop.mkCtorNames : Lean.InductiveVal → Lean.CoreM (Array Aesop.CtorNames)
-- Mathlib.Dynamics.FixedPoints.Support
/-- A self-map `f : X → X` has compact fixed support if and only if `f` fixes the complement of a
closed compact set. If `X` is preregular, then use `compactSupport_iff` instead.  -/
Function.HasCompactFixedSupport_iff' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → X},
  Function.HasCompactFixedSupport f ↔ ∃ K, IsClosed K ∧ IsCompact K ∧ (Function.fixedPoints f)ᶜ ⊆ K
-- Mathlib.Data.Multiset.Count
Multiset.count_eq_of_nodup : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, s.Nodup → Multiset.count a s = if a ∈ s then 1 else 0
-- Init.Data.List.Impl
List.findRev?.eq_def : ∀ {α : Type u} (p : α → Bool) (x : List α),
  List.findRev? p x =
    match x with
    | [] => none
    | a :: as =>
      match List.findRev? p as with
      | some b => some b
      | none => if p a = true then some a else none
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.anyM_map : ∀ {α β β' : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → β'}
  {p : β' → m Bool}, Std.Iter.anyM p (Std.Iter.map f it) = Std.Iter.anyM (fun x => p (f x)) it
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      autoParam ((X : C) → CategoryTheory.Closed X) CategoryTheory.MonoidalClosed.closed._autoParam →
        CategoryTheory.MonoidalClosed C
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRightIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (Z : C),
  (CategoryTheory.MonoidalCategory.whiskerRightIso f Z).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z
-- Init.Data.UInt.Lemmas
UInt64.ofFin_add : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a + b) = UInt64.ofFin a + UInt64.ofFin b
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_Iio_le : ∀ {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} {f : ↑(Set.Iio o) → Ordinal.{u_1}},
  o.card ≤ c → (∀ (i : ↑(Set.Iio o)), (f i).card ≤ c) → (⨆ i, f i).card ≤ c
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_inl_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set α},
  MeasurableSet (Sum.inl '' s) ↔ MeasurableSet s
-- Mathlib.Algebra.Polynomial.Basic
/-- See also `Polynomial.sum_smul_index'` for a version using `smul` on the RHS.  -/
Polynomial.sum_smul_index : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p : Polynomial R) (b : R) (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → (b • p).sum f = p.sum fun n a => f n (b * a)
-- Lean.Expr
/-- Eta reduction. If `e` is of the form `(fun x => f x)`, then return `f`.
 -/
Lean.Expr.eta : Lean.Expr → Lean.Expr
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.foldl : ∀ {α : Type u_1} {l m r : List Char} (f : α → Char → α) (init : α) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → Substring.Raw.Legacy.foldl f init s = List.foldl f init m
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β k}, (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true
-- Mathlib.LinearAlgebra.SymplecticGroup
Matrix.J_inv : ∀ (l : Type u_1) (R : Type u_2) [inst : DecidableEq l] [inst_1 : CommRing R] [inst_2 : Fintype l],
  (Matrix.J l R)⁻¹ = -Matrix.J l R
-- Lean.Util.Profile
Lean.profileitM : {m : Type → Type} →
  (ε : Type) →
    [MonadFunctorT (EIO ε) m] → {α : Type} → String → Lean.Options → m α → optParam Lean.Name Lean.Name.anonymous → m α
-- Mathlib.FieldTheory.Fixed
IsInvariantSubfield.smul_mem : ∀ {M : Type u} {inst : Monoid M} {F : Type v} {inst_1 : Field F} {inst_2 : MulSemiringAction M F} {S : Subfield F}
  [self : IsInvariantSubfield M S] (m : M) {x : F}, x ∈ S → m • x ∈ S
-- Mathlib.NumberTheory.FactorisationProperties
Nat.abundancyIndex.eq_1 : ∀ (n : ℕ), n.abundancyIndex = ↑(∑ i ∈ n.divisors, i) / ↑n
-- Std.Async.UDP
_private.Std.Async.UDP.0.Std.Async.UDP.Socket.ofNative.sizeOf_spec : ∀ (native : Std.Internal.UV.UDP.Socket), sizeOf { native := native } = 1 + sizeOf native
-- Mathlib.Topology.ContinuousMap.Bounded.Star
/-- The ⋆-algebra-homomorphism forgetting that a bounded continuous function is bounded.  -/
BoundedContinuousFunction.toContinuousMapStarₐ : {α : Type u} →
  {β : Type v} →
    (𝕜 : Type u_2) →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : NormedRing β] →
            [inst_3 : NormedAlgebra 𝕜 β] →
              [inst_4 : StarAddMonoid β] → [inst_5 : NormedStarGroup β] → BoundedContinuousFunction α β →⋆ₐ[𝕜] C(α, β)
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_uSizeToBitVec : ∀ (x : USize), ISize.ofBitVec x.toBitVec = x.toISize
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidableEq (AddSubgroup G)],
      ∀ j ∈ s, ⋃ i ∈ {x ∈ s | H x = H j}, g i +ᵥ ↑(H i) ≠ Set.univ → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
-- Mathlib.Algebra.Group.Prod
MonoidHom.coprod_comp_inl : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : CommMonoid P]
  (f : M →* P) (g : N →* P), (f.coprod g).comp (MonoidHom.inl M N) = f
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.span_singleton_eq_top : ∀ (R : Type u_2) [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M]
  {m : M}, m ≠ 0 → R ∙ m = ⊤
-- Mathlib.Data.Multiset.Replicate
Multiset.rel_replicate_left : ∀ {α : Type u_1} {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ},
  Multiset.Rel r (Multiset.replicate n a) m ↔ m.card = n ∧ ∀ x ∈ m, r a x
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_add_compProd : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''}
  {Y : Ω'' → ℝ} {cY : NNReal} [MeasureTheory.SFinite ν] {η : ProbabilityTheory.Kernel (Ω' × Ω) Ω''}
  [ProbabilityTheory.IsZeroOrMarkovKernel η],
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY η (ν.compProd κ) →
      ∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * (X ω.1 + Y ω.2))) (ν.bind ⇑(κ.compProd η))
-- Lean.Parser.Basic
Lean.Parser.pushNone : Lean.Parser.Parser
-- Mathlib.Data.Fin.SuccPred
/-- `succAbove p i` embeds `Fin n` into `Fin (n + 1)` with a hole around `p`.  -/
Fin.succAbove : {n : ℕ} → Fin (n + 1) → Fin n → Fin (n + 1)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.neg_one_mul : ∀ {R : Type u_2} [inst : CommRing R] {a b : R}, -1 * a = b → -a = b
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_add : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ ψ : MvPolynomial σ R), ↑(φ + ψ) = ↑φ + ↑ψ
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- `riemannZeta₀ s` is the completion of `riemannZeta s - (s-1)⁻¹` at `s = 1`.  -/
riemannZeta₀ : ℂ → ℂ
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.Array.cons_lex_cons.forIn'_congr_aux : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_4} {β : Type u_1} [Monad m] {as bs : ρ} {x : Membership α ρ}
  [inst : ForIn' m ρ α inferInstance] (w : as = bs) {b b' : β},
  b = b' →
    ∀ {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)},
      (∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b) → forIn' as b f = forIn' bs b' g
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (β_ X Y).inv (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst Y X
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- `VAddMemClass S R M` says `S` is a type of subsets `s ≤ M` that are closed under the
additive action of `R` on `M`.

Note that only `R` is marked as an `outParam` here, since `M` is supplied by the `SetLike`
class instead.  -/
VAddMemClass : (S : Type u_1) → (R : outParam (Type u_2)) → (M : Type u_3) → [VAdd R M] → [SetLike S M] → Prop
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.uliftFunctor.eq_1 : CommMonCat.uliftFunctor =
  { obj := fun X => CommMonCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      CommMonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((CommMonCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (a₁ a₂ a₃ : ℤ) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : ℤ) (h₁ : a₁ + b₁ = 0) (h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0),
  (CategoryTheory.shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₃ b₃ h₃).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₂ b₂ h₂).inv.app
            (Opposite.op ((CategoryTheory.shiftFunctor C b₁).1 (Opposite.unop X))))
          ((CategoryTheory.shiftFunctor Cᵒᵖ a₂).map
            ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₁ b₁ h₁).inv.app X))))
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_strict_mono_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E] {a b b' : E}
  {r : k}, b < b' → 0 < r → (AffineMap.lineMap a b) r < (AffineMap.lineMap a b') r
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.maxNilpotentIdeal_eq_top_of_isNilpotent : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [LieRing.IsNilpotent L],
  LieAlgebra.maxNilpotentIdeal R L = ⊤
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.image_finsetSum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : AddCommMonoid α]
  [inst_2 : AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α),
  ⇑f '' ∑ i ∈ m, s i = ∑ i ∈ m, ⇑f '' s i
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_piUnique : ∀ {ι : Type u_1} [inst : Fintype ι] {X : ι → Type u_4} [inst_1 : Unique ι] {m : (i : ι) → MeasurableSpace (X i)}
  (μ : (i : ι) → MeasureTheory.Measure (X i)),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piUnique X)) (MeasureTheory.Measure.pi μ) (μ default)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- Measure on `α` such that for a measurable set `s`, `ρ.IicSnd r s = ρ (s ×ˢ Iic r)`.  -/
MeasureTheory.Measure.IicSnd : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure (α × ℝ) → ℝ → MeasureTheory.Measure α
-- Mathlib.LinearAlgebra.Transvection.Generation
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.auxTransvection.congr_simp : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {e e_1 : V ≃ₗ[K] V} (e_e : e = e_1) {f f_1 : Module.Dual K V} (e_f : f = f_1) {u u_1 : V} (e_u : u = u_1)
  (hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ LinearMap.ker f),
  LinearEquiv.auxTransvection✝ hf = LinearEquiv.auxTransvection✝ ⋯
-- Mathlib.Data.Multiset.Defs
Multiset.card_mono : ∀ {α : Type u_1}, Monotone Multiset.card
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.h : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Data.PNat.Basic
Nat.succPNat_le_succPNat : ∀ {m n : ℕ}, m.succPNat ≤ n.succPNat ↔ m ≤ n
-- Init.Data.UInt.IntToBitVec
UInt8.toBitVec64_toUSize : ∀ (n : UInt8) (h : System.Platform.numBits = 64), n.toUSize.toBitVec64 h = BitVec.setWidth 64 n.toBitVec
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The conjunction of two prelocal predicates is prelocal.  -/
TopCat.PrelocalPredicate.and : {X : TopCat} →
  {T : ↑X → Type u_1} → TopCat.PrelocalPredicate T → TopCat.PrelocalPredicate T → TopCat.PrelocalPredicate T
-- Mathlib.Algebra.Divisibility.Units
IsUnit.isPrimal : ∀ {α : Type u_1} [inst : Monoid α] {u : α}, IsUnit u → IsPrimal u
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.binomial_eq : ∀ {α : Type u_1} {f : α → ℕ} {a b : α} [inst : DecidableEq α],
  a ≠ b → Nat.multinomial {a, b} f = (f a + f b).factorial / ((f a).factorial * (f b).factorial)
-- Lean.Elab.DocString
/-- Adds a builtin documentation command.

Should be run during initialization.
 -/
Lean.Doc.addBuiltinDocCommand : Lean.Name → Lean.Name → Lean.Doc.DocCommandExpander → IO Unit
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a : α} {fallback : β}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.Algebra.Group.Basic
add_eq_of_eq_sub : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = c - b → a + b = c
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.isPrefixOfAux.eq_def : ∀ {α : Type u} [inst : BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : ℕ),
  as.isPrefixOfAux bs hle i =
    if h : i < as.size then
      have a := as[i];
      have this := ⋯;
      have b := bs[i];
      if (a == b) = true then as.isPrefixOfAux bs hle (i + 1) else false
    else true
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) {s : Set α},
  MeasurableSet s → m.trim s = m s
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instRespectsSchemeSmoothIsOpenImmersion : CategoryTheory.MorphismProperty.Respects (@AlgebraicGeometry.Smooth) AlgebraicGeometry.IsOpenImmersion
-- Mathlib.Data.NNReal.Defs
NNReal.coe_sSup : ∀ (s : Set NNReal), ↑(sSup s) = sSup (NNReal.toReal '' s)
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.of_arrow_iso_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
  (e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i') (p : X ⟶ Y)
  [hip : CategoryTheory.HasLiftingProperty i p], CategoryTheory.HasLiftingProperty i' p
-- Std.Http.Data.Request
Std.Http.Request.Builder.mk.sizeOf_spec : ∀ (line : Std.Http.Request.Head) (extensions : Std.Http.Extensions),
  sizeOf { line := line, extensions := extensions } = 1 + sizeOf line + sizeOf extensions
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.support_dfinsuppFamily_subset : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] [inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)]
  [inst_9 : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j),
  ((MultilinearMap.dfinsuppFamily f) x).support ⊆ Fintype.piFinset fun i => (x i).support
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ioc' : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, c < b → Set.Iic b ∪ Set.Ioc c d = Set.Iic (max b d)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.conj : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → ∀ (h : Equiv.Perm α), (h * f * h⁻¹).Disjoint (h * g * h⁻¹)
-- Lean.Server.References
/-- Gets the references for `mod`.
The current references in a file worker take precedence over those in .ilean files.
 -/
Lean.Server.References.getModuleRefs? : Lean.Server.References → Lean.Name → Option (Lean.Lsp.DocumentUri × Lean.Lsp.ModuleRefs × Lean.Lsp.Decls)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsLUB.inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G},
  IsLUB s a → IsGLB s⁻¹ a⁻¹
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.instNontrivial : ∀ {α : Type u} [inst : Semiring α] [Nontrivial α], Nontrivial (Ideal α)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X.Hom Y) (e_f : f = f_1) (U : Y.Opens) (V : X.Opens)
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), f.resLE U V e = f_1.resLE U V ⋯
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.isLocalizationMap_of_addGroup : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] {S : AddSubmonoid M} {f : M → G},
  Function.Injective f → (∀ (g : G), ∃ x, ∃ y ∈ S, g = f x - f y) → S.IsLocalizationMap f
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.full : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂]
  (G : CategoryTheory.Functor D₁ D₂) [Φ.IsLocalizedFullyFaithful] [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G], G.Full
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.ofMatrix_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {M : Matrix m n A} {i : m}, CStarMatrix.ofMatrix M i = M i
-- Aesop.Script.ScriptM
Aesop.withOptScriptStep : {α : Type} →
  Lean.MVarId →
    (α → Array Lean.MVarId) → (α → Aesop.Script.TacticBuilder) → Lean.MetaM (Option α) → Aesop.ScriptM (Option α)