mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f},
  (m.alter k f)[k] = (f m[k]?).get ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformly.summableLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasSumLocallyUniformly f g → SummableLocallyUniformly f
-- Lean.Util.LeanOptions
Lean.LeanOptions.fromOptions? : Lean.Options → Option Lean.LeanOptions
-- Mathlib.Topology.DenseEmbedding
Dense.comap_val_nhds_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, Dense s → ∀ (a : α), (Filter.comap Subtype.val (nhds a)).NeBot
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.mk.sizeOf_spec : ∀ (ex : Lean.Exception) (patternIdx : ℕ) (pathToIndex : List ℕ),
  sizeOf { ex := ex, patternIdx := patternIdx, pathToIndex := pathToIndex } =
    1 + sizeOf ex + sizeOf patternIdx + sizeOf pathToIndex
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.norm_uncurryMid : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1))
  (f : Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G), ‖ContinuousLinearMap.uncurryMid p f‖ = ‖f‖
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase_eq_balanceR! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceR! k v l r
-- Mathlib.CategoryTheory.Sites.Spaces
/-- The Grothendieck pretopology associated to a topological space.  -/
Opens.pretopology : (T : Type u) → [inst : TopologicalSpace T] → CategoryTheory.Pretopology (TopologicalSpace.Opens T)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLTOrdinal : LT Std.Time.Nanosecond.Ordinal
-- Std.Time.Format.Modifier
Std.Time.Modifier.Q.sizeOf_spec : ∀ (presentation : Std.Time.Number ⊕ Std.Time.Text), sizeOf (Std.Time.Modifier.Q presentation) = 1 + sizeOf presentation
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hom_ext_of_isRightKanExtension : ∀ {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]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] {G : CategoryTheory.Functor D H} (γ₁ γ₂ : G ⟶ F'),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₁) α = CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₂) α →
    γ₁ = γ₂
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).K = kf.pt
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.coe_copy : ∀ {M : Type u_4} {N : Type u_5} {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : M → N) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.Limits.Sifted
/-- If the `colim` functor `(C ⥤ Type) ⥤ Type` preserves finite products, then `C` is sifted.  -/
CategoryTheory.IsSifted.of_colim_preservesFiniteProducts : ∀ (C : Type u) [inst : CategoryTheory.SmallCategory C]
  [h : CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim], CategoryTheory.IsSifted C
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.antisymm : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β}, f ≤ᶠ[l] g → g ≤ᶠ[l] f → f =ᶠ[l] g
-- Mathlib.Analysis.Convolution
/-- The symmetric definition of convolution where the bilinear operator is multiplication.  -/
MeasureTheory.convolution_mul_swap : ∀ {𝕜 : Type u𝕜} {G : Type uG} {x : G} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G]
  [MeasurableAdd G] [inst_7 : NormedSpace ℝ 𝕜] {f g : G → 𝕜},
  MeasureTheory.convolution f g (ContinuousLinearMap.mul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) * g t ∂μ
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.userPreSimprocs : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.χ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type (max u v))} (m m_1 : F ⟶ G) (e_m : m = m_1) [inst_1 : CategoryTheory.Mono m],
  CategoryTheory.Sheaf.χ m = CategoryTheory.Sheaf.χ m_1
-- Init.Data.Vector.Lemmas
Vector.foldlM_mk : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] {f : β → α → m β} {b : β}
  {xs : Array α} (h : xs.size = n), Vector.foldlM f b (Vector.mk xs h) = Array.foldlM f b xs
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivWithinAt_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {f' : F} {s t : Set E} {x v : E},
  s =ᶠ[nhds x] t → (HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).unitIso =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso✝
-- Mathlib.Topology.Order.LeftRightLim
rightLim_eq_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T2Space β] {f : α → β} {a : α} {y : β} [h : (nhdsWithin a (Set.Ioi a)).NeBot],
  Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds y) → Function.rightLim f a = y
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.equivMulOpposite_apply : ∀ {M : Type u_2} [inst : Monoid M] (f : M →ₑ[id] M), MulActionHom.End.equivMulOpposite f = MulOpposite.op (f 1)
-- Init.Data.Float.Float32
/-- Computes the square root of a floating-point number.

This function has a logical model in terms of `Float32.Model`. It is implemented in compiled code by
the C function `sqrtf`.
 -/
Float32.sqrt : Float32 → Float32
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_naturality_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f))
      (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f)
-- Mathlib.Topology.Inseparable
/-- A set is stable under generalization iff it is an intersection of open sets.  -/
stableUnderGeneralization_iff_exists_sInter_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.revSkip?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos res : s.Pos},
  pos.revSkip? p = some res ↔ ∃ (h : pos ≠ s.startPos), res = pos.prev h ∧ p ((pos.prev h).get ⋯) = true
-- Mathlib.Data.TypeVec
TypeVec.eq_nilFun : ∀ {α : TypeVec.{u_1} 0} {β : TypeVec.{u_2} 0} (f : α.Arrow β), f = TypeVec.nilFun
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk'_surjective : ∀ {X : SSet} {A : X.Subcomplex} (s : A.N),
  ∃ t, ∃ (ht : t.simplex ∉ A.obj (Opposite.op { len := t.dim })), s = { toN := t, notMem := ht }
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_symm_nhdsWithin_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  Filter.map (↑(extChartAt I x).symm) (nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)) = nhds x
-- Mathlib.Tactic.Widget.Calc
/-- Parameters for the calc widget.  -/
CalcParams : Type
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformlyOn.neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn (-F) (-f) l s
-- Mathlib.Topology.Bornology.Basic
/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions.  -/
Bornology.ofBounded : {α : Type u_4} →
  (B : Set (Set α)) →
    ∅ ∈ B → (∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B) → (∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) → (∀ (x : α), {x} ∈ B) → Bornology α
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisionAt.smul : ∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A},
  f.IsWeierstrassDivisionAt g q r I → ∀ (a : A), (a • f).IsWeierstrassDivisionAt g (a • q) (a • r) I
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_comp_algebraMap : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)),
  (RatFunc.liftRingHom φ hφ).comp (algebraMap (Polynomial K) (RatFunc K)) = φ
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The top morphism in the pushout square in the definition of `pushoutObj f πX`.  -/
CategoryTheory.SmallObject.functorObjTop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πX ⟶ X
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
/-- In a real vector space, a function `f` that approximates a linear equivalence on a subset `s`
can be extended to a homeomorphism of the whole space.  -/
ApproximatesLinearOn.exists_homeomorph_extension : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : FiniteDimensional ℝ F] {s : Set E} {f : E → F} {f' : E ≃L[ℝ] F} {c : NNReal},
  ApproximatesLinearOn f (↑f') s c →
    Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹ → ∃ g, Set.EqOn f (⇑g) s
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Lean.Elab.TerminationMeasure.elab.parameters : ℕ → Lean.MessageData
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_symm : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph W) (e : V ≃ W),
  SimpleGraph.map (⇑e.symm.toEmbedding) G = SimpleGraph.comap (⇑e.toEmbedding) G
-- Mathlib.Data.Set.Subsingleton
Set.exists_eq_singleton_iff_nonempty_subsingleton : ∀ {α : Type u} {s : Set α}, (∃ a, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.Core.mk : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : Norm E], SeminormedSpace.Core 𝕜 E → (∀ (x : E), ‖x‖ = 0 ↔ x = 0) → NormedSpace.Core 𝕜 E
-- Mathlib.NumberTheory.NumberField.Cyclotomic.PID
/-- If `IsCyclotomicExtension {3} ℚ K` then `𝓞 K` is a principal ideal domain.  -/
IsCyclotomicExtension.Rat.three_pid : ∀ (K : Type u) [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The identity affine map acts as the identity.  -/
AffineMap.coe_id : ∀ (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1], ⇑(AffineMap.id k P1) = id
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.mkDerivation_X : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] [inst_4 : IsScalarTower R (Polynomial R) A] (a : A),
  ((Polynomial.mkDerivation R) a) Polynomial.X = a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentColorOptions.toJson : Lean.Lsp.DocumentColorOptions → Lean.Json
-- Mathlib.NumberTheory.PythagoreanTriples
/-- The zeroth Pythagorean triple is all zeros.  -/
PythagoreanTriple.zero : PythagoreanTriple 0 0 0
-- Mathlib.Data.Real.Basic
Real.ofCauchy_sup : ∀ (a b : CauSeq ℚ abs), { cauchy := ⟦a ⊔ b⟧ } = max { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }
-- Batteries.Data.Fin.Lemmas
Fin.get_find?_eq_true : ∀ {n : ℕ} {p : Fin n → Bool} (h : (Fin.find? p).isSome = true), p ((Fin.find? p).get h) = true
-- Init.Data.Iterators.Lemmas.Consumers.Access
Std.Iter.atIdxSlow?_eq_match : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Productive α Id] {n : ℕ} {it : Std.Iter β},
  Std.Iter.atIdxSlow? n it =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      match n with
      | 0 => some out
      | n.succ => Std.Iter.atIdxSlow? n it'
    | Std.IterStep.skip it' => Std.Iter.atIdxSlow? n it'
    | Std.IterStep.done => none
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.swap_parallelComp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y}
  {η : ProbabilityTheory.Kernel Z T},
  (ProbabilityTheory.Kernel.swap Y T).comp (κ.parallelComp η) =
    (η.parallelComp κ).comp (ProbabilityTheory.Kernel.swap X Z)
-- Lean.Syntax
Lean.Syntax.getIdAt : Lean.Syntax → ℕ → Lean.Name
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_mono : ∀ {α : Type u_1} {s t : Set α}, t.Finite → s ⊆ t → Nat.card ↑s ≤ Nat.card ↑t
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_monomial : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (m : Option S₁ →₀ ℕ) (r : R),
  (MvPolynomial.optionEquivLeft R S₁) ((MvPolynomial.monomial m) r) =
    (Polynomial.monomial (m none)) ((MvPolynomial.monomial m.some) r)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_support : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (g : Γ), (s.coeff g).support = Set.Finite.toFinset ⋯
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- If `Ω` is a Borel space, then the Lévy-Prokhorov distance `levyProkhorovDist` makes
`ProbabilityMeasure Ω` into a metric space. The instance is recorded on the type synonym
`LevyProkhorov (ProbabilityMeasure Ω) := ProbabilityMeasure Ω`.

Note: For this metric to give the topology of convergence in distribution, one must
furthermore assume that `Ω` is separable.  -/
MeasureTheory.LevyProkhorov.levyProkhorovDist_metricSpace_probabilityMeasure : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : PseudoEMetricSpace Ω] →
      [OpensMeasurableSpace Ω] →
        [BorelSpace Ω] → MetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.ProbabilityMeasure Ω))
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.card_of_cycleType_eq_zero_iff : ∀ (α : Type u_1) [inst : DecidableEq α] [inst_1 : Fintype α] {m : Multiset ℕ},
  {g | g.cycleType = m}.card = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
eqOn_of_cfc_eq_cfc : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {f g : R → R} {a : A},
  cfc f a = cfc g a →
    autoParam (ContinuousOn f (spectrum R a)) eqOn_of_cfc_eq_cfc._auto_1 →
      autoParam (ContinuousOn g (spectrum R a)) eqOn_of_cfc_eq_cfc._auto_3 →
        autoParam (p a) eqOn_of_cfc_eq_cfc._auto_5 → Set.EqOn f g (spectrum R a)
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.MatchClone.toNatLit?.loop : Lean.Expr → OptionT Id ℕ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (x : List ((_ : α) × β)),
  Std.Internal.List.getValue? a x =
    match x with
    | [] => none
    | ⟨k, v⟩ :: l => bif k == a then some v else Std.Internal.List.getValue? a l
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.hasPullback_of_right : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f], CategoryTheory.Limits.HasPullback g f
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.ensureNoPrec : Lean.Syntax → Lean.Elab.Term.ToParserDescrM Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The square of the sine of `π / 3` is `3 / 4` (this is sometimes more convenient than the
result for cosine itself).  -/
Real.sq_sin_pi_div_three : Real.sin (Real.pi / 3) ^ 2 = 3 / 4
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Every `M` is a direct sum of objects from `C`, and `F` preserves biproducts.  -/
CategoryTheory.Mat_.additiveObjIsoBiproduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) →
              [inst_4 : F.Additive] →
                (M : CategoryTheory.Mat_ C) → F.obj M ≅ ⨁ fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂Grp_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommGrp C} (f : A ⟶ B),
  ((CategoryTheory.CommGrp.forget₂Grp C).map f).hom = f.hom.hom
-- Mathlib.Analysis.SpecialFunctions.Arsinh
HasFDerivAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : StrongDual ℝ E},
  HasFDerivAt f f' a → HasFDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector.  -/
Orthonormal.inner_left_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v →
    ∀ (l : ι → 𝕜) {s : Finset ι} {i : ι}, i ∈ s → inner 𝕜 (∑ i ∈ s, l i • v i) (v i) = (starRingEnd 𝕜) (l i)
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_Iio_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Iio a)) (Filter.principal (Set.Iio a))
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddMonoid M],
  AddMonoidAlgebra.mapRingHom M (RingHom.id R) = RingHom.id (AddMonoidAlgebra R M)
-- Batteries.Data.List.Pairwise
List.pwFilter_cons_of_pos : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] {a : α} {l : List α},
  (∀ b ∈ List.pwFilter R l, R a b) → List.pwFilter R (a :: l) = a :: List.pwFilter R l
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.mul_continuous : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] [inst_5 : NormedRing R]
  [SecondCountableTopologyEither X R] {f g : X → R},
  Continuous g → MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable (fun x => f x * g x) μ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ),
  t.natTransTruncLEOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.truncLE a)
-- Init.Data.Array.Lemmas
Array.finIdxOf?_toList : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α},
  List.finIdxOf? a xs.toList = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)
-- Lean.Elab.InfoTree.Basic
/-- Helper function for propagating the tactic metavariable context to its children nodes.
We need this function because we preserve `TacticInfo` nodes during backtracking *and* their
children. Moreover, we backtrack the metavariable context to undo metavariable assignments.
`TacticInfo` nodes save the metavariable context before/after the tactic application, and
can be pretty printed without any extra information. This is not the case for `TermInfo` nodes.
Without this function, the formatting method would often fail when processing `TermInfo` nodes
that are children of `TacticInfo` nodes that have been preserved during backtracking.
Saving the metavariable context at `TermInfo` nodes is also not a good option because
at `TermInfo` creation time, the metavariable context often miss information, e.g.,
a TC problem has not been resolved, a postponed subterm has not been elaborated, etc.

See `Term.SavedState.restore`.
 -/
Lean.Elab.Info.updateContext? : Option Lean.Elab.ContextInfo → Lean.Elab.Info → Option Lean.Elab.ContextInfo
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_univ : ∀ {α : Type u} [inst : TopologicalSpace α] (x : α), connectedComponentIn Set.univ x = connectedComponent x
-- Mathlib.Data.Complex.Basic
Complex.im_nnratCast : ∀ (q : ℚ≥0), (↑q).im = 0