mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.inner_condExpL2_left_eq_right : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) {f g : ↥(MeasureTheory.Lp E 2 μ)},
  inner 𝕜 (↑((MeasureTheory.condExpL2 E 𝕜 hm) f)) g = inner 𝕜 f ↑((MeasureTheory.condExpL2 E 𝕜 hm) g)
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.toMulLeftReflectLE : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α], MulLeftReflectLE α
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.mem : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X} {s : Set X}, Convexity.IsStarConvexSet R x s → s.Nonempty → x ∈ s
-- Mathlib.Logic.IsEmpty.Defs
IsEmpty.exists_iff : ∀ {α : Sort u} [IsEmpty α] {p : α → Prop}, (∃ a, p a) ↔ False
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_counitIso_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.prodOpEquiv C).counitIso.hom.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.Topology.Category.Stonean.Basic
/-- Every Stonean space is projective in `CompHaus`  -/
Stonean.instProjectiveCompHausCompHaus : ∀ (X : Stonean), CategoryTheory.Projective (Stonean.toCompHaus.obj X)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.IsFiltered.IsEventuallyConstant.mk : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C},
  (∃ i, F.IsEventuallyConstantFrom i) → CategoryTheory.IsFiltered.IsEventuallyConstant F
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.Ordinal.CNF.coeff.eq_1 : ∀ (b o : Ordinal.{u_1}),
  Ordinal.CNF.coeff b o = { entries := List.map Prod.toSigma (Ordinal.CNF b o), nodupKeys := ⋯ }.lookupFinsupp
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add.eq_2 : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (x : W.Point),
  (x = WeierstrassCurve.Affine.Point.zero → False) → x.add WeierstrassCurve.Affine.Point.zero = x
-- Mathlib.Tactic.Spread
/-- Mathlib extension to preserve old behavior of structure instances.
We need to be able to `let` some implementation details that are still local instances.
Normally implementation detail fvars are not local instances,
but we need them to be implementation details so that `simp` will see them as "reducible" fvars.
 -/
elabLetImplDetail : Lean.Elab.Term.TermElab
-- Aesop.Rule.Name
Aesop.DisplayRuleName.normSimp.sizeOf_spec : sizeOf Aesop.DisplayRuleName.normSimp = 1
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instRepresentablyFlatOverForget : ∀ (S : AlgebraicGeometry.Scheme), CategoryTheory.RepresentablyFlat (AlgebraicGeometry.Scheme.ProEt.forget S)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_zero_of_mem`.

---

If a point `x` belongs to `s`, then its edist to `s` vanishes  -/
EMetric.infEdist_zero_of_mem : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ s → Metric.infEDist x s = 0
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Identity map as an `AffineIsometryEquiv`.  -/
AffineIsometryEquiv.refl : (𝕜 : Type u_1) →
  {V : Type u_2} →
    (P : Type u_10) →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] → [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → P ≃ᵃⁱ[𝕜] P
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_ext_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {f : J → C} {X Y : C}
  {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (⨁ f) Y},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)) →
    g = h
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.isRadical_radical : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsRadical (UniqueFactorizationMonoid.radical a)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.sizeLt.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Analytic.Basic
/-- A function `f : 𝕜 → E` has `p` as power series expansion at a point `z₀` iff it is the sum of
`p` in a neighborhood of `z₀`. This makes some proofs easier by hiding the fact that
`HasFPowerSeriesAt` depends on `p.radius`.  -/
hasFPowerSeriesAt_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in nhds 0, HasSum (fun n => z ^ n • p.coeff n) (f (z₀ + z))
-- Mathlib.Data.Finset.Defs
Finset.instPartialOrder : {α : Type u_1} → PartialOrder (Finset α)
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Int.gcd`.
Uses positivity of the left term, if available, then tries the right term.  -/
Mathlib.Meta.Positivity.evalIntGCD : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Topology.Compactness.Compact
IsCompact.elim_nhds_subcover' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ (U : (x : X) → x ∈ s → Set X), (∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) → ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.self_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
  (F' : CategoryTheory.Limits.MonoFactorisation f), (CategoryTheory.Limits.IsImage.self f).lift F' = F'.e
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x y : CategoryTheory.CatCenter C),
  (∀ (X : C), x.app X = y.app X) → x = y
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_eq_norm_sq_to_K : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), inner 𝕜 x x = ↑‖x‖ ^ 2
-- Plausible.Testable
/-- The maximum size of the values to generate.
 -/
Plausible.Configuration.maxSize : Plausible.Configuration → ℕ
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsDirectedOrderSubtypeSetCarrierObjPartOrdEmbIsCardinalFilteredWithTopPropSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular], IsDirectedOrder (Subtype (J.PropSetWithTop κ'))
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instMetricSpace : (p : ℕ) → [hp : Fact (Nat.Prime p)] → MetricSpace ℤ_[p]
-- Std.Http.Data.Headers
/-- Replaces the last value for the given header name.
If the header is absent, returns the headers unchanged.
 -/
Std.Http.Headers.replaceLast : Std.Http.Headers → Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Headers
-- Mathlib.RingTheory.Flat.EquationalCriterion
Equiv.isTrivialRelation_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : Fintype ι] {f : ι → R} {x : ι → M} {κ : Type u_4} [inst_4 : Fintype κ] (e : κ ≃ ι),
  Module.IsTrivialRelation (f ∘ ⇑e) (x ∘ ⇑e) ↔ Module.IsTrivialRelation f x
-- Mathlib.Control.EquivFunctor.Instances
EquivFunctorFinset : EquivFunctor Finset
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mul_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {x y : A}, x ∈ S → y ∈ S → x * y ∈ S
-- Init.Data.UInt.Lemmas
UInt32.ofNatLT_mul : ∀ {a b : ℕ} (ha : a < 2 ^ 32) (hb : b < 2 ^ 32) (hab : a * b < 2 ^ 32),
  UInt32.ofNatLT (a * b) hab = UInt32.ofNatLT a ha * UInt32.ofNatLT b hb
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.lowerSemicontinuous : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {f : α → γ}, Continuous f → LowerSemicontinuous f
-- Mathlib.Order.Partition.Finpartition
/-- The empty finpartition.  -/
Finpartition.empty : (α : Type u_1) → [inst : Lattice α] → [inst_1 : OrderBot α] → Finpartition ⊥
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_eq_one : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G.diam = 1 ↔ G = ⊤
-- Mathlib.Algebra.Order.Group.Equiv
ofLexMulEquiv.eq_1 : ∀ (α : Type u_1) [inst : Mul α], ofLexMulEquiv α = { toEquiv := ofLex, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The category of multicoforks is equivalent to the category of coforks over `∐ I.left ⇉ ∐ I.right`.
It then follows from `CategoryTheory.IsColimit.ofPreservesCoconeInitial` (or `reflects`) that
it preserves and reflects colimit cocones.
 -/
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct I.left] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] →
            CategoryTheory.Limits.Multicofork I ≌ CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.mk.injEq : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (toEquiv : G ≃ H)
  (map_add_const' : ∀ (x : G), toEquiv.toFun (x + a) = toEquiv.toFun x + b) (toEquiv_1 : G ≃ H)
  (map_add_const'_1 : ∀ (x : G), toEquiv_1.toFun (x + a) = toEquiv_1.toFun x + b),
  ({ toEquiv := toEquiv, map_add_const' := map_add_const' } =
      { toEquiv := toEquiv_1, map_add_const' := map_add_const'_1 }) =
    (toEquiv = toEquiv_1)
-- Init.Data.Vector.Lemmas
Vector.mem_of_mem_push_of_mem : ∀ {α : Type u_1} {n : ℕ} {a b : α} {xs : Vector α n}, a ∈ xs.push b → b ∈ xs → a ∈ xs
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.HasDetPlusMinusOne.det_eq : ∀ {n : Type u_1} {inst : Fintype n} {inst_1 : DecidableEq n} {R : Type u_2} {inst_2 : CommRing R}
  {Γ : Subgroup (GL n R)} [self : Γ.HasDetPlusMinusOne] {g : GL n R},
  g ∈ Γ → Matrix.GeneralLinearGroup.det g = 1 ∨ Matrix.GeneralLinearGroup.det g = -1
-- Mathlib.MeasureTheory.Order.Group.Lattice
measurable_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α] [MeasurableInv α]
  [MeasurableSup₂ α], Measurable mabs
-- Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.isFiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))) [CategoryTheory.IsFiltered I],
  (∀ (i : I), CategoryTheory.Limits.IsIndObject (F.obj i)) →
    CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda (CategoryTheory.Limits.colimit F))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.covconv_swap : ∀ {N : Type u_2} {r : N → N → Prop} [inst : AddGroup N] [CovariantClass N N (Function.swap fun x1 x2 => x1 + x2) r],
  ContravariantClass N N (Function.swap fun x1 x2 => x1 + x2) r
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_natCast : ∀ {R : Type u} {M : Type v} [inst : AddMonoidWithOne R] [inst_1 : AddMonoid M] (n : ℕ), (↑n).fst = ↑n
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.neg_llr : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → -MeasureTheory.llr μ ν =ᵐ[μ] MeasureTheory.llr ν μ
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNSMul : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddMonoid M] → [ContinuousAdd M] → SMul ℕ (SeparationQuotient M)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.iSup_toSubmodule_eq_top : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} {N : ι → LieSubmodule R L M},
  ⨆ i, ↑(N i) = ⊤ ↔ ⨆ i, N i = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Nonneg.instIsometricContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A],
  IsometricContinuousFunctionalCalculus NNReal A fun x => 0 ≤ x
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ}, (Std.HashMap.map f m).size = m.size
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node3L_size : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  (l.node3L x m y r).size = l.size + m.size + r.size + 2
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance between a set and itself is zero.  -/
Metric.hausdorffDist_self_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, Metric.hausdorffDist s s = 0
-- Mathlib.Data.NNRat.Defs
/-- Form the quotient `n / d` where `n d : ℕ`.

See also `Rat.divInt` and `mkRat`.  -/
NNRat.divNat : ℕ → ℕ → ℚ≥0
-- Mathlib.Logic.Encodable.Basic
instDecidableEqULower : {α : Type u_1} → [inst : Encodable α] → DecidableEq (ULower α)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.subcomplex_le_filtration : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) {j : ι}
  (c : f.Cell j) {i : ι}, j < i → (↑(P.p c.s)).subcomplex ≤ f.filtration i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_erase!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], (Std.DTreeMap.Internal.Impl.erase! k t).get! k = default
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.polynomialX.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R),
  W.polynomialX =
    Polynomial.C (Polynomial.C W.a₁) * Polynomial.X -
      Polynomial.C (Polynomial.C 3 * Polynomial.X ^ 2 + Polynomial.C (2 * W.a₂) * Polynomial.X + Polynomial.C W.a₄)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instMulActionWithZero : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {R : Type u_2} →
            [inst_3 : MonoidWithZero R] →
              [inst_4 : MulActionWithZero R β] →
                [ContinuousConstSMul R β] → MulActionWithZero R (ZeroAtInftyContinuousMap α β)
-- Batteries.Data.DList.Lemmas
Batteries.DList.ofThunk_coe : ∀ {α : Type u_1} {l : List α}, Batteries.DList.ofThunk { fn := fun x => l } = Batteries.DList.ofList l
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.node`.  -/
Tree.node : {α : Type u} → α → Tree α → Tree α → Tree α
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      ((CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso hc).hom =
    c.ι.app j
-- Mathlib.Data.Quot
Quot.instInhabited_mathlib : {α : Sort u_1} → (r : α → α → Prop) → [Inhabited α] → Inhabited (Quot r)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- A locally finite measure on a `σ`-compact topological space admits a finite spanning sequence
of open sets.  -/
MeasureTheory.Measure.finiteSpanningSetsInOpen : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    [SigmaCompactSpace α] →
      {x : MeasurableSpace α} →
        (μ : MeasureTheory.Measure α) → [MeasureTheory.IsLocallyFiniteMeasure μ] → μ.FiniteSpanningSetsIn {K | IsOpen K}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.w₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁ f₁ = h.p
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.Indep.disjoint_loops : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → Disjoint I M.loops
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Avoiding a fixed family of patterns is a closed
condition (in the product topology on `G → A`).

Since each occurrence set `{ x | p.occursInAt x v }` is open (when `A` is discrete),
its complement `{ x | ¬ p.occursInAt x v }` is closed; `forbidden F` is the intersection
of these closed sets over `p ∈ F` and `v ∈ G`.  -/
SymbolicDynamics.FullShift.isClosed_forbidden : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : AddMonoid G]
  [IsLeftCancelAdd G] [DiscreteTopology A] (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  IsClosed (SymbolicDynamics.FullShift.forbidden F)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂AddMonoidHom_apply : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) (p : Polynomial R),
  (Polynomial.eval₂AddMonoidHom f x) p = Polynomial.eval₂ f x p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ((∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.homQuotientZSMulOfHom_comp_of_rightInverse : ∀ {A B : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ),
  Function.RightInverse ⇑g ⇑f →
    (QuotientAddGroup.homQuotientZSMulOfHom f n).comp (QuotientAddGroup.homQuotientZSMulOfHom g n) =
      AddMonoidHom.id (B ⧸ (zsmulAddGroupHom n).range)
-- Batteries.Data.BitVec.Lemmas
BitVec.getLsb_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnLE f).getLsb i = f i
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- Given a Mayer-Vietoris square `S` and a presheaf of types, this is the
map from `P.obj (op S.X₄)` to the explicit fibre product of
`P.map S.f₁₂.op` and `P.map S.f₁₃.op`.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toPullbackObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        (S : J.MayerVietorisSquare) →
          (P : CategoryTheory.Functor Cᵒᵖ (Type v')) →
            P.obj (Opposite.op S.X₄) → CategoryTheory.Limits.Types.PullbackObj (P.map S.f₁₂.op) (P.map S.f₁₃.op)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndep.iCondIndepSets : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω}
  {s : ι → Set (Set Ω)},
  (∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) →
    ProbabilityTheory.iCondIndep m' hm' m μ → ProbabilityTheory.iCondIndepSets m' hm' s μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_iff_isSome_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, a ∈ t ↔ (t.get? a).isSome = true
-- Mathlib.Order.Atoms
IsCoatom.iInf_le : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Order.Coframe α] {f : ι → α} {a : α}, IsCoatom a → (iInf f ≤ a ↔ ∃ i, f i ≤ a)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_undef : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, ¬MeasureTheory.Integrable f μ → ∫ (a : α), f a ∂μ = 0
-- Init.Data.List.Basic
List.instAppend : {α : Type u} → Append (List α)
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Icc_pure_pure : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Filter.TendstoIxxClass Set.Icc (pure a) (pure a)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.mk.sizeOf_spec : ∀ {α : Type u_6} [inst : MeasurableSpace α] [inst_1 : SizeOf α] (toOuterMeasure : MeasureTheory.OuterMeasure α)
  (m_iUnion :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure (f i))
  (trim_le : toOuterMeasure.trim ≤ toOuterMeasure),
  sizeOf { toOuterMeasure := toOuterMeasure, m_iUnion := m_iUnion, trim_le := trim_le } = 1 + sizeOf toOuterMeasure
-- Mathlib.Topology.Algebra.AffineSubspace
AffineSubspace.coe_subtypeA : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : AffineSubspace R P) [inst_5 : Nonempty ↥s],
  ⇑s.subtypeA = Subtype.val
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.proofInstInfo : Lean.Meta.Sym.State → Lean.PHashMap Lean.Name (Option Lean.Meta.Sym.ProofInstInfo)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.neg.match_1.splitter : {R : Type u_1} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      (motive : W'.Point → Sort u_2) →
        (x : W'.Point) →
          (Unit → motive WeierstrassCurve.Affine.Point.zero) →
            ((x y : R) → (h : W'.Nonsingular x y) → motive (WeierstrassCurve.Affine.Point.some x y h)) → motive x
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.BimonObjAux_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.ComonObj.comul = CategoryTheory.ComonObj.comul.hom
-- Lean.Attributes
Lean.AttributeKind.local : Lean.AttributeKind
-- Mathlib.SetTheory.Cardinal.ENat
/-- Unbundled version of `Cardinal.toENat`.  -/
Cardinal.toENatAux : Cardinal.{u} → ℕ∞
-- Mathlib.Topology.Defs.Basic
BaireSpace.baire_property : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : BaireSpace X] (f : ℕ → Set X),
  (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.isIntegral_gen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
  IsIntegral A pb.gen
-- Std.Do.SPred.Laws
Std.Do.SPred.forall_elim : ∀ {σs : List (Type u)} {α : Sort u_1} {Ψ : α → Std.Do.SPred σs} (a : α), (∀ a, Ψ a) ⊢ₛ Ψ a