mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.alterₘ : {α : Type u} →
  {β : Type v} →
    [BEq α] →
      [Hashable α] →
        (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → (Option β → Option β) → Std.DHashMap.Internal.Raw₀ α fun x => β
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousWithinAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α},
  UpperHemicontinuousWithinAt f s x ↔
    ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Mathlib.Data.NNRat.Defs
NNRat.mk_zero : ⟨0, ⋯⟩ = 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_inj : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁.edgeSet = G₂.edgeSet ↔ G₁ = G₂
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.withTopCoe : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.IsSuccPrelimit x → Order.IsSuccPrelimit ↑x
-- Mathlib.Algebra.Group.Action.TransferInstance
Equiv.addAction.eq_1 : ∀ (M : Type u_1) {α : Type u_4} {β : Type u_5} [inst : AddMonoid M] (e : α ≃ β) [inst_1 : AddAction M β],
  Equiv.addAction M e = { toVAdd := Equiv.vadd M e, add_vadd := ⋯, zero_vadd := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.getKey a ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.instFactEqNatFinrankFin : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] (n : ℕ), Fact (Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n)
-- Mathlib.Data.Num.Bitwise
instDecidableEqSNum : DecidableEq SNum
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.comp_left : ∀ {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 Z : CategoryTheory.Comma L R} {f : X ⟶ Y} {g : Y ⟶ Z},
  (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- A property ensuring that the tangent cone to `s` at any of its points spans a dense subset of
the whole space. The main role of this property is to ensure that the differential along `s` is
unique, hence this name. The uniqueness it asserts is proved in `UniqueDiffOn.eq` in
`Mathlib/Analysis/Calculus/FDeriv/Basic.lean`.  -/
UniqueDiffOn : (R : Type u) →
  {E : Type v} → [inst : Semiring R] → [inst_1 : AddCommGroup E] → [Module R E] → [TopologicalSpace E] → Set E → Prop
-- Mathlib.Algebra.Exact.Basic
Function.Exact.comp_injective : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {P' : Type u_7} {f : M → N} {g : N → P} (g' : P → P') [inst : Zero P]
  [inst_1 : Zero P'], Function.Exact f g → Function.Injective g' → g' 0 = 0 → Function.Exact f (g' ∘ g)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- The natural map from `characterSpace ℂ (elemental ℂ x)` to `spectrum ℂ x` given
by evaluating `φ` at `x`. This is essentially just evaluation of the `gelfandTransform` of `x`,
but because we want something in `spectrum ℂ x`, as opposed to
`spectrum ℂ ⟨x, elemental.self_mem ℂ x⟩` there is slightly more work to do.  -/
StarAlgebra.elemental.characterSpaceToSpectrum : {A : Type u_1} →
  [inst : CStarAlgebra A] → (x : A) → ↑(WeakDual.characterSpace ℂ ↥(StarAlgebra.elemental ℂ x)) → ↑(spectrum ℂ x)
-- Mathlib.Algebra.Group.End
Equiv.Perm.mul_refl : ∀ {α : Type u_4} (e : Equiv.Perm α), e * Equiv.refl α = e
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.addCommMonoid : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → AddCommMonoid (LieSubalgebra R L)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α}
  {h' : k ∈ t.insertManyIfNewUnit l} (contains : k ∈ t), (t.insertManyIfNewUnit l).getKey k h' = t.getKey k contains
-- Mathlib.Data.EReal.Inv
_private.Mathlib.Data.EReal.Inv.0.EReal.exists_lt_mul_right_of_nonneg : ∀ {a b c : EReal}, 0 ≤ a → 0 ≤ c → c < a * b → ∃ b' ∈ Set.Ioo 0 b, c < a * b'
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqVarId : BEq Lean.IR.VarId
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.norm_approxBounded_le : ∀ {α : Type u_1} {β : Type u_5} {f : α → β} [inst : SeminormedAddCommGroup β] [inst_1 : NormedSpace ℝ β]
  {m : MeasurableSpace α} {c : ℝ} (hf : MeasureTheory.StronglyMeasurable f),
  0 ≤ c → ∀ (n : ℕ) (x : α), ‖(hf.approxBounded c n) x‖ ≤ c
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.ex_iff_not_all_not : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α (n + 1)),
  T.Iff φ.ex φ.not.all.not
-- Mathlib.Order.SupClosed
infClosed_pi : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → SemilatticeInf (α i)] {s : Set ι} {t : (i : ι) → Set (α i)},
  (∀ i ∈ s, InfClosed (t i)) → InfClosed (s.pi t)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- If the distances between distinct points in a (pseudo) metric space
are uniformly bounded away from zero, then the space has discrete topology.  -/
DiscreteTopology.of_forall_le_dist : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] {r : ℝ},
  0 < r → (Pairwise fun x1 x2 => r ≤ dist x1 x2) → DiscreteTopology α
-- Std.Http.Data.Chunk
Std.Http.Chunk.instDecidableEqExtensionValue.decEq : (x x_1 : Std.Http.Chunk.ExtensionValue) → Decidable (x = x_1)
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_one_nnnorm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], LipschitzWith 1 nnnorm
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.ker_codRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p), (↑(f.codRestrict p h)).ker = (↑f).ker
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instVAdd'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : VAdd M β],
  Filter.Germ.instVAdd' = { vadd := Filter.Germ.map₂ fun x1 x2 => x1 +ᵥ x2 }
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_inv_apply : ∀ {M N : CommMonCat} (e : M ≅ N) (s : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.mem_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] {s : Set M} {x : M},
  x ∈ SubAddAction.closure R s ↔ ∀ (p : SubAddAction R M), s ⊆ ↑p → x ∈ p
-- Lean.Expr
Lean.Expr.updateConst! : Lean.Expr → List Lean.Level → Lean.Expr
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable, `f` has a bottom element, and `f =O[atTop] g`, for some
`g` integrable at `atTop`, then `f` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : LinearOrder α] [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated]
  [OrderBot α],
  MeasureTheory.LocallyIntegrable f μ →
    f =O[Filter.atTop] g → MeasureTheory.IntegrableAtFilter g Filter.atTop μ → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor on `CommGrpCat.{u}` creates `u`-small limits.
 -/
CommGrpCat.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} CommGrpCat.uliftFunctor
-- Batteries.Data.List.Basic
/-- A version of `List.sublists` that has faster runtime performance but worse kernel performance  -/
List.sublistsFast : {α : Type u_1} → List α → List (List α)
-- Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
/-- Any `StrictSegal` simplicial set is a `Quasicategory`.  -/
SSet.StrictSegal.quasicategory : ∀ {X : SSet} (sx : X.StrictSegal), X.Quasicategory
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_const_iff_isFiniteMeasure_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {c : ε},
  ‖c‖ₑ ≠ 0 → ‖c‖ₑ ≠ ⊤ → (MeasureTheory.HasFiniteIntegral (fun x => c) μ ↔ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq_of_le : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] {i : ι} {ω : Ω}, ↑i ≤ τ ω → MeasureTheory.stoppedProcess u τ i ω = u i ω
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.mk.sizeOf_spec : ∀ (kind : WantedRefKind✝) (binderType : Lean.TSyntax `term) (isClass : Bool) (deps : Array WantedDep✝)
  (transparent : Option (Lean.TSyntax `term)),
  sizeOf { kind := kind, binderType := binderType, isClass := isClass, deps := deps, transparent := transparent } =
    1 + sizeOf kind + sizeOf binderType + sizeOf isClass + sizeOf deps + sizeOf transparent
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearMap.isBigO_comp : ∀ {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_5} {G : Type u_6} [inst : SeminormedAddCommGroup F]
  [inst_1 : SeminormedAddCommGroup G] [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NontriviallyNormedField 𝕜₃]
  [inst_4 : NormedSpace 𝕜₂ F] [inst_5 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomIsometric σ₂₃] {α : Type u_7}
  (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α), (fun x' => g (f x')) =O[l] f
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_X_pow : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) {s : σ} {n : ℕ}, MvPolynomial.eval₂ f g (MvPolynomial.X s ^ n) = g s ^ n
-- Mathlib.Algebra.Group.AddChar
/-- An additive character maps `0` to `1`.  -/
AddChar.map_zero_eq_one : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M), ψ 0 = 1
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_le_eRk_add_eRk_sdiff : ∀ {α : Type u_1} {X Y : Set α} (M : Matroid α), Y ⊆ X → M.eRk X ≤ M.eRk Y + M.eRk (X \ Y)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
/-- Evaluating a pushout amounts to taking the pushout of the evaluations.  -/
CategoryTheory.Limits.pushoutObjIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor D C} →
          [inst_2 : CategoryTheory.Limits.HasPushouts C] →
            (f : F ⟶ G) →
              (g : F ⟶ H) →
                (d : D) → (CategoryTheory.Limits.pushout f g).obj d ≅ CategoryTheory.Limits.pushout (f.app d) (g.app d)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algebraMap_X : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K],
  (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = RatFunc.X
-- Std.Time.Internal.Bounded
/-- Expand the bottom of the bounded to a number `nhi` is `hi` is less or equal to the previous higher bound.
 -/
Std.Time.Internal.Bounded.LE.expandTop : {lo hi nhi : ℤ} → Std.Time.Internal.Bounded.LE lo hi → hi ≤ nhi → Std.Time.Internal.Bounded.LE lo nhi
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.StrongHomClass.toEquiv_invFun : ∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : EquivLike F M N] [inst_3 : L.StrongHomClass F M N] (a : F) (a_1 : N),
  (FirstOrder.Language.StrongHomClass.toEquiv a).invFun a_1 = EquivLike.inv a a_1
-- Init.Data.Range.Polymorphic.UInt
USize.succMany?_ofBitVec : ∀ {k : ℕ} {x : BitVec System.Platform.numBits},
  Std.PRange.succMany? k { toBitVec := x } = USize.ofBitVec <$> Std.PRange.succMany? k x
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.reflectsMonomorphisms_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Faithful], F.ReflectsMonomorphisms
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.coe_countAddMonoidHom : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), ⇑(Multiset.countAddMonoidHom a) = Multiset.count a
-- Mathlib.Topology.MetricSpace.Isometry
/-- On pseudometric spaces, a map is an isometry if and only if it preserves distances.  -/
isometry_iff_dist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
/-- The multispan index in the category associated to the complete lattice `T`
given by the objects `u i` and the minima `v i j = u i ⊓ u j`,
when `d : MulticoequalizerDiagram x u v`.  -/
CompleteLattice.MulticoequalizerDiagram.multispanIndex : {T : Type u} →
  [inst : CompleteLattice T] →
    {ι : Type u_1} →
      {x : T} →
        {u : ι → T} →
          {v : ι → ι → T} →
            CompleteLattice.MulticoequalizerDiagram x u v →
              CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) T
-- Mathlib.Algebra.Order.Ring.Abs
abs_lt_of_sq_lt_sq' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a ^ 2 < b ^ 2 → 0 ≤ b → -b < a ∧ a < b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : Inhabited α] [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.union m₂).getKey! k = m₁.getKey! k
-- Mathlib.Data.List.AList
/-- The singleton association list.  -/
AList.singleton : {α : Type u} → {β : α → Type v} → (a : α) → β a → AList β
-- Init.Prelude
instLTUInt32 : LT UInt32
-- Lean.Elab.Tactic.Try
/-- Atomic tactics with library suggestions.

Note: We previously included `simp_all? +suggestions` here, but removed it due to performance issues.
We would like to restore it in the future once `simp_all? +suggestions` is faster for general use.
 -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkAtomicWithSuggestionsStx : Lean.CoreM (Lean.TSyntax `tactic)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) (a : B),
  (CategoryTheory.Pseudofunctor.mkOfOplax F F').mapId a = F'.mapIdIso a
-- Init.SimpLemmas
ite_congr : ∀ {α : Sort u_1} {b c : Prop} {x y u v : α} {s : Decidable b} [inst : Decidable c],
  b = c → (c → x = u) → (¬c → y = v) → (if b then x else y) = if c then u else v
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- If the top-right element of a block matrix is invertible, then the whole matrix is invertible
iff the corresponding Schur complement is.  -/
Matrix.isUnit_fromBlocks_iff_of_invertible₁₁ : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
  {D : Matrix n n α} [inst_5 : Invertible A], IsUnit (Matrix.fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.false.sizeOf_spec : sizeOf Lean.Grind.AC.StartsWithResult.false✝ = 1
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The single functors on `DerivedCategory.Plus C` are induced by the
single functors on `DerivedCategory C`.  -/
DerivedCategory.Plus.singleFunctorιIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) →
          (DerivedCategory.Plus.singleFunctor C n).comp DerivedCategory.Plus.ι ≅ DerivedCategory.singleFunctor C n
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j - f k) κ μ
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instInsertProdOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → [EquivBEq α] → [LawfulHashable α] → Insert (α × β) (Std.Internal.IndexMultiMap α β)
-- Mathlib.NumberTheory.Height.NumberField
NumberField.totalWeight_pos : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 0 < Height.totalWeight K
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
norm_exp_mul_sq_le : ∀ {τ : ℂ},
  0 < τ.im → ∀ (n : ℤ), ‖Complex.exp (↑Real.pi * Complex.I * ↑n ^ 2 * τ)‖ ≤ Real.exp (-Real.pi * τ.im) ^ n.natAbs
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a division  -/
SubgroupClass.div : {G : Type u_5} →
  {S : Type u_6} → [inst : DivInvMonoid G] → [inst_1 : SetLike S G] → [SubgroupClass S G] → {H : S} → Div ↥H
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.trans.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Add α] [inst_4 : Add β] [inst_5 : Add γ] (f : α ≃+o β) (g : β ≃+o γ),
  f.trans g = { toAddEquiv := (↑f).trans ↑g, map_le_map_iff' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_eq_top : ∀ {α : Type u_1} {M : Matroid α} [M.RankInfinite], M.eRank = ⊤
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_pow_interval : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s : NonemptyInterval α)
  (n : ℕ), ↑(s ^ n) = ↑s ^ n
-- Mathlib.Algebra.Group.Conj
/-- The setoid of the relation `IsAddConj` iff there
is an additive unit `u` such that `u + x = y + u`  -/
IsAddConj.setoid : (α : Type u_1) → [AddMonoid α] → Setoid α
-- Mathlib.LinearAlgebra.Complex.Module
/-- The standard decomposition of `ℜ a + Complex.I • ℑ a = a` of an element of a star module over
`ℂ` into a linear combination of self adjoint elements.  -/
realPart_add_I_smul_imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : A), ↑(realPart a) + Complex.I • ↑(imaginaryPart a) = a
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The data of all `i`th iterations for `i : J` such that `i ≤ j`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.F : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {Φ : CategoryTheory.SmallObject.SuccStruct C} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] →
                [inst_5 : WellFoundedLT J] → {j : J} → Φ.Iteration j → CategoryTheory.Functor (↑(Set.Iic j)) C
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.mk_toOrderHom : ∀ {a b : SimplexCategory} (f : a.Hom b), SimplexCategory.Hom.mk f.toOrderHom = f
-- Init.Data.Range.Polymorphic.NatLemmas
Array.range'_eq_toArray_rco : ∀ {m n : ℕ}, Array.range' m n = (m...m + n).toArray
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_injective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N},
  Function.Injective ⇑f → Function.Injective (AddSubsemigroup.map f)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.monic_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (n : ℕ), p.degree ≤ ↑n → p.coeff n = 1 → p.Monic
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.continuousOn_mul_of_subset : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {A K : Set X} [inst_3 : NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R},
  ContinuousOn g K →
    MeasureTheory.IntegrableOn g' A μ →
      IsCompact K → MeasurableSet A → A ⊆ K → MeasureTheory.IntegrableOn (fun x => g x * g' x) A μ
-- Batteries.Classes.Order
Std.instTransCmpByKey : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (cmp : β → β → Ordering) [Std.TransCmp cmp],
  Std.TransCmp (Ordering.byKey f cmp)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) → [comon : CategoryTheory.ComonObj X] → CategoryTheory.Comon C
-- Mathlib.Algebra.Group.Finsupp
/-- Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.
 -/
Finsupp.mapRange.addMonoidHom : {ι : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} → [inst : AddCommMonoid M] → [inst_1 : AddCommMonoid N] → (M →+ N) → (ι →₀ M) →+ ι →₀ N
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- A variant of `jointly_surjective` for `x : colimit F`.  -/
CategoryTheory.Limits.Types.jointly_surjective' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F] (x : CategoryTheory.Limits.colimit F),
  ∃ j y, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) y = x
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.coe_essSup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f → ↑(essSup f μ) = essSup (fun x => ↑(f x)) μ
-- Std.Http.Data.Body.Empty
/-- Non-blocking receive. Empty bodies are always at EOF.
 -/
Std.Http.Body.Empty.tryRecv : Std.Http.Body.Empty → Std.Async.Async (Option (Option Std.Http.Chunk))
-- Lean.Server.References
/-- Adds `ref` to `i`.
If `i` has no `definition` and `ref` is a declaration, it becomes the `definition`.
If `i` already has a `definition` and `ref` is also a declaration, it is not added to `i`.
Otherwise, `ref` is added to `i.usages`.
 -/
Lean.Server.RefInfo.addRef : Lean.Server.RefInfo → Lean.Server.Reference → Lean.Server.RefInfo
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
/-- Conditionally complete partial orders (with infima) are partial orders
where every nonempty, directed set which is bounded below has a greatest lower bound.  -/
ConditionallyCompletePartialOrderInf : Type u_3 → Type u_3
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.ζ_def_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]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.AddMonObj X] {Z : D}
  (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.AddMonObj.zero) h)