mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Derivation.Basic
/-- The composition of a derivation with a linear map as a bilinear map  -/
Derivation.llcomp : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {N : Type u_5} →
                    [inst_6 : AddCommMonoid N] →
                      [inst_7 : Module A N] →
                        [inst_8 : Module R N] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R A N] → (M →ₗ[A] N) →ₗ[A] Derivation R A M →ₗ[A] Derivation R A N
-- Lean.Meta.AppBuilder
/-- Returns `let_body_congr a h`  -/
Lean.Meta.mkLetBodyCongr : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Basic
inv_mul_eq_iff_eq_mul : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a⁻¹ * b = c ↔ b = a * c
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle_apply_mk : ∀ {T : ℝ} (x : ℝ), AddCircle.toCircle ↑x = Circle.exp (2 * Real.pi / T * x)
-- Mathlib.ModelTheory.DirectLimit
/-- Constructor for `FirstOrder.Language.Structure.Sigma` alias.  -/
FirstOrder.Language.Structure.Sigma.mk : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      {G : ι → Type w} →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) → (i : ι) → G i → FirstOrder.Language.Structure.Sigma f
-- Init.Data.Format.Basic
Std.instToFormatFormat : Std.ToFormat Std.Format
-- Mathlib.Logic.Small.Basic
small_of_surjective : ∀ {α : Type v} {β : Type w} [Small.{u, v} α] {f : α → β}, Function.Surjective f → Small.{u, w} β
-- ProofWidgets.Data.Html
Lean.Parser.Category.proofWidgetsJsxElement : Lean.Parser.Category
-- Lean.Syntax
Lean.Syntax.antiquotSuffixSplice? : Lean.Syntax → Option Lean.SyntaxNodeKind
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.of_isEmpty : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] [IsEmpty α] {s : Set α}, DirSupClosedOn D s
-- Mathlib.Algebra.BigOperators.Expect
Fintype.card_mul_expect : ∀ {ι : Type u_1} {M : Type u_4} [inst : Semiring M] [inst_1 : Module ℚ≥0 M] [inst_2 : Fintype ι] (f : ι → M),
  (↑(Fintype.card ι) * Finset.univ.expect fun i => f i) = ∑ i, f i
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.subgroupOfEquivOfLe.congr_simp : ∀ {G : Type u_7} [inst : Group G] {H K : Subgroup G} (h : H ≤ K),
  Subgroup.subgroupOfEquivOfLe h = Subgroup.subgroupOfEquivOfLe h
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- associativity of the tensorator  -/
CategoryTheory.Functor.LaxMonoidal.associativity : ∀ {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}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.ae_le_of_ae_le_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : LE E] {hm : m ≤ m0}
  {f₁ f₂ : α → E}, f₁ ≤ᵐ[μ.trim hm] f₂ → f₁ ≤ᵐ[μ] f₂
-- Mathlib.Topology.Path
Path.refl_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X}, Set.range ⇑(Path.refl a) = {a}
-- Mathlib.Topology.Algebra.Monoid
Continuous.addUnits_map : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : TopologicalSpace M]
  [inst_3 : TopologicalSpace N] (f : M →+ N), Continuous ⇑f → Continuous ⇑(AddUnits.map f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.injOn_tan : Set.InjOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.complex_d_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) = 0
-- Init.Data.BitVec.Bitblast
BitVec.neg_sdiv : ∀ {w : ℕ} {x y : BitVec w}, x ≠ BitVec.intMin w → (-x).sdiv y = -x.sdiv y
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.gt) → Sort u_3)
  (size : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Mathlib.Analysis.Normed.Group.Basic
mul_mem_closedBall_iff_norm : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, a * b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse'.eq_1 : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f)
  (h₂ : Function.RightInverse g ⇑f), f.inverse' g k h₁ h₂ = { toFun := g, map_vadd' := ⋯ }
-- Lean.Elab.DocString
Lean.Doc.Context.mk.injEq : ∀ (suggestionMode suggestionMode_1 : Lean.Doc.SuggestionMode),
  ({ suggestionMode := suggestionMode } = { suggestionMode := suggestionMode_1 }) = (suggestionMode = suggestionMode_1)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The proposition that the topology of `E` is induced by a family of seminorms `p`.  -/
WithSeminorms : {𝕜 : Type u_2} →
  {E : Type u_6} →
    {ι : Type u_9} →
      [inst : NormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] → SeminormFamily 𝕜 E ι → [topology : TopologicalSpace E] → Prop
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α) (cut : α → Ordering),
  RBTree.RBNode.find? cut t.reverse = RBTree.RBNode.find? (fun x => (cut x).swap) t
-- Mathlib.Algebra.Polynomial.CoeffList
Polynomial.head?_coeffList : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R}, P ≠ 0 → P.coeffList.head? = some P.leadingCoeff
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.asHomogeneousIdeal : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] →
          {𝒜 : ℕ → σ} → [inst_3 : GradedRing 𝒜] → ProjectiveSpectrum 𝒜 → HomogeneousIdeal 𝒜
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.trim_le : ∀ {α : Type u_6} [inst : MeasurableSpace α] (self : MeasureTheory.Measure α), self.trim ≤ self.toOuterMeasure
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_toReal_eq : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α NNReal), f.toReal.nnrealPart = f
-- Batteries.Tactic.Lint.Simp
/-- A linter for commutativity lemmas that are marked simp.  -/
Batteries.Tactic.Lint.simpComm : Batteries.Tactic.Lint.Linter
-- Init.Data.Vector.Count
Vector.count_eq_countP' : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a : α}, Vector.count a = Vector.countP fun x => x == a
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instHashableRealizeConstKey : Hashable Lean.Environment.RealizeConstKey✝
-- Mathlib.Logic.Basic
exists_mem_or : ∀ {α : Sort u_1} {p : α → Prop} {P Q : (x : α) → p x → Prop},
  (∃ x, ∃ (h : p x), P x h ∨ Q x h) ↔ (∃ x, ∃ (h : p x), P x h) ∨ ∃ x, ∃ (h : p x), Q x h
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_ofNat_eq_factorial : ∀ (n : ℕ) [inst : (n + 1).AtLeastTwo], Real.Gamma (OfNat.ofNat (n + 1)) = ↑n.factorial
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.withFn.formatter : (Lean.Parser.ParserFn → Lean.Parser.ParserFn) → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtTreeMap.get! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited β] → Std.ExtTreeMap α β cmp → α → β
-- Mathlib.Topology.DenseEmbedding
/-- Variation of `extend_eq` where we ask that `f` has a limit along `comap i (𝓝 b)` for each
`b : β`. This is a strictly stronger assumption than continuity of `f`, but in a lot of cases
you'd have to prove it anyway to use `continuous_extend`, so this avoids doing the work twice.  -/
IsDenseInducing.extend_eq' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] {f : α → γ} (di : IsDenseInducing i),
  (∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) → ∀ (a : α), di.extend f (i a) = f a
-- Mathlib.Tactic.ClickSuggestions.Apply
_private.Mathlib.Tactic.ClickSuggestions.Apply.0.Mathlib.Tactic.ClickSuggestions.tacticSyntax.hasOnlyImplicitArgs : Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₈_isSymm : CartanMatrix.E₈.IsSymm
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The p-adic valuation on integers, sending `p` to `(exp (-1) : ℤᵐ⁰)`  -/
Int.padicValuation : (p : ℕ) → [Fact (Nat.Prime p)] → Valuation ℤ (WithZero (Multiplicative ℤ))
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instBEqState.beq : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Reader.State dir → Std.Http.Protocol.H1.Reader.State dir → Bool
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The cone of strictly positive elements.

Note that this naming diverges from the mathlib convention of `pos` and `nonneg` due to "positive
cone" (`ConvexCone.positive`) being established terminology for the non-negative elements.  -/
ConvexCone.strictlyPositive : (R : Type u_2) →
  (M : Type u_4) →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : PartialOrder M] →
            [IsOrderedAddMonoid M] → [inst_5 : Module R M] → [PosSMulStrictMono R M] → ConvexCone R M
-- Mathlib.Order.BoundedOrder.Basic
Pi.top_def : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Top (α' i)], ⊤ = fun x => ⊤
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesWithinAt_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E} {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
-- Aesop.Script.TacticState
Aesop.Script.TacticState.mk : Array Aesop.GoalWithMVars → Std.HashSet Lean.MVarId → Aesop.Script.TacticState
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_min?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).min?.isSome = true
-- Mathlib.Data.Multiset.Fold
Multiset.fold_zero : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α), Multiset.fold op b 0 = b
-- Mathlib.Algebra.Group.Hom.Defs
/-- `0` is the homomorphism sending all elements to `0`.  -/
instZeroZeroHom : {M : Type u_4} → {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → Zero (ZeroHom M N)
-- Mathlib.Algebra.Order.Group.Basic
zsmul_left_inj : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a : α},
  0 < a → ∀ {m n : ℤ}, m • a = n • a ↔ m = n
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.AEStronglyMeasurable.ae_of_compProd : ∀ {α : Type u_5} {β : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_8}
  [inst : NormedAddCommGroup E] {f : α → β → E},
  MeasureTheory.AEStronglyMeasurable (Function.uncurry f) (μ.compProd κ) →
    ∀ᵐ (x : α) ∂μ, MeasureTheory.AEStronglyMeasurable (f x) (κ x)
-- Mathlib.Order.Interval.Finset.Defs
Finset.subtype_Iic_eq : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderBot α]
  (a : Subtype p), Finset.Iic a = Finset.subtype p (Finset.Iic ↑a)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwPos.mk.injEq : ∀ (relName : Lean.Name) (relation : Lean.Expr) (symm? : Option Bool) (relName_1 : Lean.Name) (relation_1 : Lean.Expr)
  (symm?_1 : Option Bool),
  ({ relName := relName, relation := relation, symm? := symm? } =
      { relName := relName_1, relation := relation_1, symm? := symm?_1 }) =
    (relName = relName_1 ∧ relation = relation_1 ∧ symm? = symm?_1)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Build an algebra morphism from a linear map out of a tensor product, and evidence that on pure
tensors, it preserves multiplication and the identity.

Note that we state `h_one` using `1 ⊗ₜ[R] 1` instead of `1` so that lemmas about `f` applied to pure
tensors can be directly applied by the caller (without needing `TensorProduct.one_def`).
 -/
Algebra.TensorProduct.algHomOfLinearMapTensorProduct : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring C] →
                              [inst_10 : Algebra S C] →
                                (f : TensorProduct R A B →ₗ[S] C) →
                                  (∀ (a₁ a₂ : A) (b₁ b₂ : B),
                                      f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)) →
                                    f (1 ⊗ₜ[R] 1) = 1 → TensorProduct R A B →ₐ[S] C
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertMany_nil : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.insertMany [] = t
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.get? (t.minD fallback) = some (t.minD fallback)
-- Mathlib.Order.CompleteLattice.Basic
sSup_le_sSup_of_isCofinalFor : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s t : Set α}, IsCofinalFor s t → sSup s ≤ sSup t
-- Mathlib.Topology.Maps.Strict.Basic
/-- Embeddings are precisely injective strict maps.  -/
Topology.isEmbedding_iff_isStrictMap_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f ↔ Topology.IsStrictMap f ∧ Function.Injective f
-- Mathlib.Algebra.Polynomial.Reverse
_private.Mathlib.Algebra.Polynomial.Reverse.0.Polynomial.reflect.match_1.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (motive : Polynomial R → Sort u_2) (f : AddMonoidAlgebra R ℕ)
  (h_1 : (f : AddMonoidAlgebra R ℕ) → motive { toFinsupp := f }),
  (match { toFinsupp := f } with
    | { toFinsupp := f } => h_1 f) =
    h_1 f
-- Mathlib.Topology.Bases
Finite.toSecondCountableTopology : ∀ {α : Type u} [t : TopologicalSpace α] [Finite α], SecondCountableTopology α
-- Mathlib.Order.RelSeries
RelSeries.toList.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.toList = List.ofFn x.toFun
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.State.visited : Lean.Expr.FoldRelevantConstantsImpl.State✝ → Lean.PtrSet Lean.Expr
-- Mathlib.Data.Set.Finite.Basic
/-- Construct a `Finite` instance for a `Set` from a `Finset` with the same elements.  -/
Set.Finite.ofFinset : ∀ {α : Type u} {p : Set α} (s : Finset α), (∀ (x : α), x ∈ s ↔ x ∈ p) → p.Finite
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.comp_toFun : ∀ {X Y Z : Bipointed} (f : X.Hom Y) (g : Y.Hom Z) (a : X.X), (f.comp g).toFun a = (g.toFun ∘ f.toFun) a
-- Mathlib.Data.Finsupp.Order
Finsupp.single_le_sum : ∀ {α : Type u_5} {M : Type u_6} {N : Type u_7} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsOrderedAddMonoid N] (f : α →₀ M) {g : α → M → N},
  (0 ≤ fun x1 x2 => g x1 x2) → ∀ (a : α), (fun₀ | a => f a).sum g ≤ f.sum g
-- Mathlib.Data.DFinsupp.Defs
Zero.toOfNat0.hcongr_2 : ∀ (α α' : Type u_1), α = α' → ∀ (inst : Zero α) (inst' : Zero α'), inst ≍ inst' → Zero.toOfNat0 ≍ Zero.toOfNat0
-- Mathlib.Data.TypeVec
TypeVec.prod.mk.eq_1 : ∀ (n : ℕ) (α β : TypeVec.{u} n.succ) (i : Fin2 n), TypeVec.prod.mk i.fs = TypeVec.prod.mk i
-- Init.WF
InvImage.accessible : ∀ {α : Sort u} {β : Sort v} {r : β → β → Prop} {a : α} (f : α → β), Acc r (f a) → Acc (InvImage r f) a
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instMul : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Mul (SpecialLinearGroup R V)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing : Lean.Expr →
  Int.Internal.Linear.Poly →
    Lean.Meta.Grind.Arith.CommRing.RingExpr →
      Lean.Grind.CommRing.Poly → Int.Internal.Linear.Poly → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.of : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} → (j : J) → ↑(F.obj j) → CommRingCat.Colimits.Prequotient F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_norm0 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [inst_1 : LE α] (lhs rhs : α), (lhs ≤ rhs) = (lhs ≤ rhs + ↑0)
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_pos_iff : ∀ (n : Int8), 0 < n.toNatClampNeg ↔ 0 < n
-- Mathlib.Algebra.BigOperators.Pi
RingHom.functions_ext : ∀ {I : Type u_7} [inst : DecidableEq I] {R : I → Type u_8} [inst_1 : (i : I) → NonAssocSemiring (R i)] [Finite I]
  (S : Type u_9) [inst_3 : NonAssocSemiring S] (g h : ((i : I) → R i) →+* S),
  (∀ (i : I) (x : R i), g (Pi.single i x) = h (Pi.single i x)) → g = h
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_apply_ne : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : (i : o) → Matrix (m' i) (n' i) α) {k k' : o} (i : m' k) (j : n' k'),
  k ≠ k' → Matrix.blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hasRightExtension_iff_of_iso₁ : ∀ {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]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H),
  L.HasRightKanExtension F ↔ L'.HasRightKanExtension F
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_add_right_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (x : G), Filter.map (fun h => h + x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Mathlib.Probability.Process.Predictable
/-- **Alias** of `MeasureTheory.IsStronglyPredictable`.

---

A process is said to be predictable if it is measurable with respect to the predictable
σ-algebra.  -/
MeasureTheory.IsPredictable : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      {E : Type u_3} →
        [TopologicalSpace E] → [inst : Preorder ι] → [OrderBot ι] → MeasureTheory.Filtration ι m → (ι → Ω → E) → Prop
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.SatisfiesM_ExceptT_eq.match_1_11.splitter : {α ρ : Type u_1} →
  {p : α → Prop} →
    (motive : { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a } → Sort u_2) →
      (x : { a // (fun x => ∀ (a : α), x = Except.ok a → p a) a }) →
        ((a : α) → (h : ∀ (a_1 : α), Except.ok a = Except.ok a_1 → p a_1) → motive ⟨Except.ok a, h⟩) →
          ((e : ρ) → (property : ∀ (a : α), Except.error e = Except.ok a → p a) → motive ⟨Except.error e, property⟩) →
            motive x
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.AC.Seq → Sort u_1) (s : Lean.Grind.AC.Seq)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x))
  (h_2 : (x : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s))
  (x : Lean.Grind.AC.Var),
  s = Lean.Grind.AC.Seq.var x →
    (match s with
      | Lean.Grind.AC.Seq.var x => h_1 x
      | Lean.Grind.AC.Seq.cons x s => h_2 x s) ≍
      h_1 x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- If a function is the least upper bound of countably many measurable functions,
then it is measurable.  -/
Measurable.isLUB : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  [Countable ι] {f : ι → δ → α} {g : δ → α},
  (∀ (i : ι), Measurable (f i)) → (∀ (b : δ), IsLUB {a | ∃ i, f i b = a} (g b)) → Measurable g
-- Mathlib.Probability.Distributions.SetBernoulli
/-- A random variable `X : Ω → Set ι` is `p`-bernoulli on a set `u : Set ι` if its distribution is
the product over `u` of `p`-bernoulli distributions.  -/
ProbabilityTheory.IsSetBernoulli : {ι : Type u_1} →
  {Ω : Type u_2} → {m : MeasurableSpace Ω} → (Ω → Set ι) → Set ι → ↑unitInterval → MeasureTheory.Measure Ω → Prop
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instQuasiCompactCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.propQCPrecoverage P) S),
  AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover