mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff : ∀ {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] (α β : LieModule.Weight K (↥H) L),
  LieModule.chainTopCoeff (⇑α) β + LieModule.chainBotCoeff (⇑α) β = LieAlgebra.IsKilling.chainLength α β
-- Mathlib.Algebra.Category.Grp.AB
AddMonoidHom.mk'.congr_simp : ∀ {M : Type u_4} {G : Type u_7} [inst : AddGroup G] [inst_1 : AddZeroClass M] (f f_1 : M → G) (e_f : f = f_1)
  (map_add : ∀ (a b : M), f (a + b) = f a + f b), AddMonoidHom.mk' f map_add = AddMonoidHom.mk' f_1 ⋯
-- Mathlib.Order.Bounded
Set.bounded_lt_Iic : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] (a : α), Set.Bounded (fun x1 x2 => x1 < x2) (Set.Iic a)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The order of the torsion group of the `n`-th cyclotomic field is `n` if `n` is even and
`2n` if `n` is odd.
 -/
IsCyclotomicExtension.Rat.torsionOrder_eq : ∀ {n : ℕ} {K : Type u} [inst : Field K] [NeZero n] [inst_2 : NumberField K] [hK : IsCyclotomicExtension {n} ℚ K],
  NumberField.Units.torsionOrder K = if Even n then n else 2 * n
-- Mathlib.Order.RelSeries
/-- For two preorders `α, β`, if `f : α → β` is strictly monotonic, then a strict chain of `α`
can be pushed out to a strict chain of `β` by
`a₀ < a₁ < ... < aₙ ↦ f a₀ < f a₁ < ... < f aₙ`
 -/
LTSeries.map : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → LTSeries α → (f : α → β) → StrictMono f → LTSeries β
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.sparseCasesOnInfoExt : Lean.MapDeclarationExtension Lean.Meta.SparseCasesOnInfo
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.span_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v) (i : ι), (Module.Basis.span hli) i = ⟨v i, ⋯⟩
-- Mathlib.Algebra.Algebra.StrictPositivity
/-- An element of an ordered algebra is *strictly positive* if it is nonnegative and invertible.

NOTE: This definition will be generalized to the non-unital case in the future; do not unfold
the definition and use the API provided instead to avoid breakage when the refactor happens.  -/
IsStrictlyPositive : {A : Type u_1} → [LE A] → [Monoid A] → [Zero A] → A → Prop
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.Option.elim.match_1.eq_1 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (x : α) (x_1 : β) (f : α → β)
  (h_1 : (x : α) → (x_2 : β) → (f : α → β) → motive (some x) x_2 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match some x, x_1, f with
    | some x, x_2, f => h_1 x x_2 f
    | none, y, x => h_2 y x) =
    h_1 x x_1 f
-- Mathlib.Algebra.Exact.Basic
Function.Exact.linearMap_comp_eq_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}, Function.Exact ⇑f ⇑g → g ∘ₗ f = 0
-- Std.Time.Date.Unit.Weekday
/-- Tuesday.  -/
Std.Time.Weekday.tuesday : Std.Time.Weekday
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.
 -/
Std.IterM.fold : {m : Type w → Type w'} →
  {α β γ : Type w} →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → (γ → β → γ) → γ → Std.IterM m β → m γ
-- Init.Data.Iterators.Basic
/-- A well-founded relation such that if `it'` is a successor iterator of `it`, then `Rel it' it`.
 -/
Std.Iterators.FinitenessRelation.Rel : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] → Std.Iterators.FinitenessRelation α m → Std.IterM m β → Std.IterM m β → Prop
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.unchanged.sizeOf_spec : sizeOf Aesop.SimpResult.unchanged = 1
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.ker_lift : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M) (HN : N ≤ φ.ker), (QuotientAddGroup.lift N φ HN).ker = AddSubgroup.map (QuotientAddGroup.mk' N) φ.ker
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The distance from `x` to `s` or `t` is controlled in terms of the Hausdorff distance
between `s` and `t`.  -/
Metric.infEDist_le_infEDist_add_hausdorffEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  Metric.infEDist x t ≤ Metric.infEDist x s + Metric.hausdorffEDist s t
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofHom_apply : ∀ {X Y : Type u} [inst : Group X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : Group Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y] (f : X →ₜ* Y) (x : X),
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.ofHom f)) x = f x
-- Mathlib.Tactic.Linarith.Datatypes
/-- A shorthand for tracing the types of a list of proof terms
when the `trace.linarith` option is set to true.
 -/
Mathlib.Tactic.Linarith.linarithTraceProofs : {α : Type} → [Lean.ToMessageData α] → α → List Lean.Expr → Lean.MetaM Unit
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry.congr_simp : ∀ {α : Type u} {β : α → Type v} (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.isEmpty = false),
  t.minEntry h = t_1.minEntry ⋯
-- Mathlib.RingTheory.Coprime.Lemmas
Finset.prod_dvd_of_coprime : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {z : R} {s : I → R} {t : Finset I},
  (↑t).Pairwise (Function.onFun IsCoprime s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.mk : Lean.InductiveVal → ℕ → Lean.LocalDecl → Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.Meta.Cases.Context
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- **Alias** of `dvd_add`. -/
Dvd.dvd.add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Semigroup α] [LeftDistribClass α] {a b c : α}, a ∣ b → a ∣ c → a ∣ b + c
-- Lean.Meta.Sym.Arith.Types
/-- Inverse function if `fieldInst?` is `some inst`  -/
Lean.Meta.Sym.Arith.CommRing.invFn? : Lean.Meta.Sym.Arith.CommRing → Option Lean.Expr
-- Mathlib.Order.CompleteLattice.Basic
Prod.infSet : (α : Type u_1) → (β : Type u_2) → [InfSet α] → [InfSet β] → InfSet (α × β)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.pullback.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (V : F → F) (x : E), VectorField.pullback 𝕜 f V x = (fderiv 𝕜 f x).inverse (V (f x))
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_mul_left_iff : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {g : α → F}
  {l : Filter α} {f : α → S} {c : S}, c ≠ 0 → ((fun x => c * f x) =O[l] g ↔ f =O[l] g)
-- Mathlib.Probability.Kernel.WithDensity
/-- Auxiliary lemma for `IsSFiniteKernel.withDensity`.
If a kernel `κ` is finite, then `withDensity κ f` is s-finite.  -/
ProbabilityTheory.Kernel.isSFiniteKernel_withDensity_of_isFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsFiniteKernel κ],
  (∀ (a : α) (b : β), f a b ≠ ⊤) → ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.symmetry_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C × D), (CategoryTheory.Prod.symmetry C D).hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The conductor is invariant under `changeLevel`: lifting a Dirichlet character `χ` of level `n`
to a multiple level `m` does not change its conductor.  -/
DirichletCharacter.conductor_changeLevel : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} [NeZero m] (hm : n ∣ m),
  ((DirichletCharacter.changeLevel hm) χ).conductor = χ.conductor
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_sdiff_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L),
  ⟨a, ha⟩ \ ⟨b, hb⟩ = ⟨a \ b, ⋯⟩
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Typecheck a `NormedAddGroupHom` as a morphism in `SemiNormedGrp`.  -/
SemiNormedGrp.ofHom : {M N : Type u} →
  [inst : SeminormedAddCommGroup M] →
    [inst_1 : SeminormedAddCommGroup N] →
      NormedAddGroupHom M N → ({ carrier := M, str := inst } ⟶ { carrier := N, str := inst_1 })
-- Mathlib.Order.Bounds.Basic
/-- The greatest lower bound of a set is also the greatest lower bound of any
coinitial subset.  -/
IsGLB.of_isCoinitialFor : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s t : Set α}, IsGLB s a → t ⊆ s → IsCoinitialFor s t → IsGLB t a
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.compl_path_image_Ioc : ∀ {x y : Circle}, x ≠ y → (⇑(x.path y) '' Set.Ioc 0 1)ᶜ = ⇑(y.path x) '' Set.Ioc 0 1
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Return `true` iff current binder should be merged with the nested
binder, if any, into a single binder group:
* both binders must have same binder info and domain
* they cannot be inst-implicit (`[a b : A]` is not valid syntax)
* `pp.XXBinderTypes` must be the same value for both terms
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.shouldGroupWithNext : Lean.PrettyPrinter.Delaborator.DelabM Bool
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.det_eq_prod_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  LinearMap.det T = ∏ i, ↑(hT.eigenvalues hn i)
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.limRatioMeas_measurable : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ), Measurable (v.limRatioMeas hρ)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRightEquiv_apply : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : MulOneClass M] [inst_1 : Monoid N₁] [inst_2 : Monoid N₂]
  (e : N₁ ≃* N₂) (hmn : M →* N₁), e.monoidHomCongrRightEquiv hmn = e.toMonoidHom.comp hmn
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- A variant of `WeierstrassCurve.j_eq_zero_iff_of_char_three` without assuming a reduced ring.  -/
WeierstrassCurve.j_eq_zero_iff_of_char_three' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [CharP R 3], W.j = 0 ↔ W.b₂ ^ 6 = 0
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- This is the pointwise product of `ArithmeticFunction`s.  -/
ArithmeticFunction.pmul : {R : Type u_1} → [inst : MulZeroClass R] → ArithmeticFunction R → ArithmeticFunction R → ArithmeticFunction R
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- An alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→ₗ[R] N`,
is a multilinear map that vanishes when two of its arguments are equal.  -/
AlternatingMap : (R : Type u_1) →
  [inst : Semiring R] →
    (M : Type u_2) →
      [inst_1 : AddCommMonoid M] →
        [Module R M] →
          (N : Type u_3) → [inst_3 : AddCommMonoid N] → [Module R N] → Type u_7 → Type (max (max u_2 u_3) u_7)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.iSup_eq_closure : ∀ {M : Type u_1} [inst : Add M] {ι : Sort u_3} (p : ι → AddSubsemigroup M),
  ⨆ i, p i = AddSubsemigroup.closure (⋃ i, ↑(p i))
-- Std.Sync.CancellationToken
Std.CancellationReason.shutdown.sizeOf_spec : sizeOf Std.CancellationReason.shutdown = 1
-- Mathlib.Algebra.Order.Floor.Defs
Int.le_ceil : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), a ≤ ↑⌈a⌉
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.mem_unop : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A}
  {S : Subalgebra R Aᵐᵒᵖ}, x ∈ S.unop ↔ MulOpposite.op x ∈ S
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeEquivalence_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cocone.precomposeEquivalence α).counitIso =
    CategoryTheory.NatIso.ofComponents'
      (fun s =>
        CategoryTheory.Limits.Cocone.extInv
          (CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.Cocone.precompose α.hom).comp (CategoryTheory.Limits.Cocone.precompose α.inv)).obj
                s).pt)
          ⋯)
      ⋯
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_inv₀`. -/
AntivaryOn.inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → AntivaryOn f g s → AntivaryOn f⁻¹ g⁻¹ s
-- Mathlib.Data.Set.Functor
Set.image_coe_eq_domRestrict_image : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {δ : Type u_1} {f : α → δ},
  (f '' do
      let a ← γ
      pure ↑a) =
    β.domRestrict f '' γ
-- Mathlib.Data.Setoid.Basic
/-- The first isomorphism theorem for sets: the quotient of α by the kernel of a function f
bijects with f's image.  -/
Setoid.quotientKerEquivRange : {α : Type u_1} → {β : Type u_2} → (f : α → β) → Quotient (Setoid.ker f) ≃ ↑(Set.range f)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.mkInductiveDecl : Array Lean.Expr → Array Lean.Elab.Command.InductiveElabStep1 → Lean.Elab.TermElabM Lean.Elab.Command.FinalizeContext✝
-- Mathlib.Lean.Meta.Basic
/-- Given a metavariable `inst` whose type is a class, tries to synthesize the instance then runs `k`.
If synthesis fails, then runs `k` with `inst` as a local instance and then substitutes `inst`
into the resulting expression.

Example: `reassocExprHom` operates by applying simp lemmas that assume a `Category` instance.
The category might not yet be known, which can prevent simp lemmas from applying.
We can add `inst` as a local instance to deal with this.
However, if the instance is synthesizable, we prefer running `k` directly
so that the local instance doesn't affect typeclass inference.
 -/
Lean.Meta.withEnsuringLocalInstance : {α : Type} → Lean.MVarId → Lean.MetaM (Lean.Expr × α) → Lean.MetaM (Lean.Expr × α)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
EReal.expHomeomorph_symm : EReal.expHomeomorph.symm = ENNReal.logHomeomorph
-- Lean.Server.Requests
/-- Workers execute request handlers in this monad.  -/
Lean.Server.RequestM : Type → Type
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), (e.restr s).target = e.target ∩ ↑e.symm ⁻¹' s
-- Mathlib.MeasureTheory.Order.Lattice
/-- Eta-expanded form of `Measurable.inf` -/
Measurable.fun_inf : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Min M]
  [MeasurableInf₂ M], Measurable f → Measurable g → Measurable fun i => f i ⊓ g i
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_union_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] (s t : Set α), sSup (s ∪ t) ≤ max (sSup s) (sSup t)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] →
      [inst_1 : Top α] → [inst_2 : SemilatticeInf β] → [inst_3 : OrderTop β] → PartialOrder (InfTopHom α β)
-- Init.Core
Prod.lexLt_def : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] (s t : α × β),
  s.lexLt t = (s.1 < t.1 ∨ s.1 = t.1 ∧ s.2 < t.2)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ereal_toENNReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → EReal}, Measurable f → Measurable fun x => (f x).toENNReal
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- If `E` has pairwise pullbacks, this is the canonical map to the minimal `1`-hypercover
from the saturation.  -/
CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → [inst_1 : E.HasPullbacks] → E.saturate ⟶ E.toPreOneHypercover
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k (t₁.getKeyD k fallback)
-- Mathlib.Probability.StrongLaw
/-- Preliminary lemma for the strong law of large numbers for vector-valued random variables,
assuming measurability in addition to integrability. This is weakened to ae measurability in
the full version `ProbabilityTheory.strong_law_ae`.  -/
ProbabilityTheory.strong_law_ae_of_measurable : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E]
  [BorelSpace E] (X : ℕ → Ω → E),
  MeasureTheory.Integrable (X 0) μ →
    MeasureTheory.StronglyMeasurable (X 0) →
      Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
        (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
          ∀ᵐ (ω : Ω) ∂μ,
            Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))
-- Init.Data.List.Basic
List.findFinIdx?.go : {α : Type u} → (α → Bool) → (l l' : List α) → (i : ℕ) → l'.length + i = l.length → Option (Fin l.length)
-- Init.Data.List.Nat.InsertIdx
List.getElem_insertIdx_of_lt : ∀ {α : Type u} {l : List α} {x : α} {i j : ℕ} (hn : j < i) (hk : j < (l.insertIdx i x).length),
  (l.insertIdx i x)[j] = l[j]
-- Mathlib.Order.SupClosed
infClosed_preimage_ofDual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, InfClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ SupClosed s
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- The canonical ring homomorphism from a commutative semiring to the product of its
localizations at all prime ideals. It is always injective.  -/
PrimeSpectrum.toPiLocalization : (R : Type u_1) → [inst : CommSemiring R] → R →ₐ[R] PrimeSpectrum.PiLocalization R
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingConeHomOfDegreewiseSplitXIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (p q : ℤ) (hpq : p + 1 = q),
  CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ p q hpq =
    CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ p q hpq
-- Lean.Meta.Basic
/-- Makes the helper constant `constName` that is derived from `forConst` available in the environment.
`enableRealizationsForConst forConst` must have been called first on this environment branch. If
this is the first environment branch requesting `constName` to be realized (atomically), `realize`
is called with the environment and options at the time of calling `enableRealizationsForConst` if
`forConst` is from the current module and the state just after importing  otherwise, thus helping
achieve deterministic results despite the non-deterministic choice of which thread is tasked with
realization. In other words, the state after calling `realizeConst` is *as if* `realize` had been
called immediately after `enableRealizationsForConst forConst`, though the effects of this call are
visible only after calling `realizeConst`. See below for more details on the replayed effects.

`realizeConst` cannot check what other data is captured in the `realize` closure,
so it is best practice to extract it into a separate function and pay close attention to the passed
arguments, if any. `realize` must return with `constName` added to the environment,
at which point all callers of `realizeConst` with this `constName` will be unblocked
and have access to an updated version of their own environment containing any new constants
`realize` added, including recursively realized constants. Traces, diagnostics, and raw std stream
output are reported at all callers via `Core.logSnapshotTask` (so that the location of generated
diagnostics is deterministic). Note that, as `realize` is run using the options at declaration time
of `forConst`, trace options must be set prior to that (or, for imported constants, on the cmdline)
in order to be active. The environment extension state at the end of `realize` is available to each
caller via `EnvExtension.getState (asyncDecl := constName)`. If `realize` throws an exception or
fails to add `constName` to the environment, an appropriate diagnostic is reported to all callers
but no constants are added to the environment.
 -/
Lean.Meta.realizeConst : Lean.Name → Lean.Name → Lean.MetaM Unit → Lean.MetaM Unit
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.of_surjOn : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} (f : α → β), Set.SurjOn f s t → s.Finite → t.Finite
-- Mathlib.Data.Nat.Prime.Basic
Nat.succ_pred_prime : ∀ {p : ℕ}, Nat.Prime p → p.pred.succ = p
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderInf α] [inst_1 : Preorder β] {f : β → α}
  (a : β), Monotone f → ⨅ x, f ↑x = f a
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.attach_affineCombination_of_injective : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] [inst_3 : DecidableEq P] (s : Finset P) (w : P → k) (f : ↥s → P),
  Function.Injective f →
    (Finset.affineCombination k s.attach f) (w ∘ f) = (Finset.affineCombination k (Finset.image f Finset.univ) id) w
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.intCast : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] (d : ℤ), 0 ≤ d → (↑d).PosSemidef
-- Lean.Data.Lsp.Extra
/-- Controls when dependencies are built on `textDocument/didOpen` notifications.
 -/
Lean.Lsp.DependencyBuildMode : Type
-- Mathlib.Topology.Algebra.Affine
AffineMap.homothety_continuous : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : CommRing R]
  [inst_6 : Module R V] [ContinuousConstSMul R V] (x : P) (t : R), Continuous ⇑(AffineMap.homothety x t)