mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instPosSMulStrictMono : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → PartialOrder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), PosSMulStrictMono α (β i)], PosSMulStrictMono α (Π₀ (i : ι), β i)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNewUnit.eq_2 : ∀ {α : Type u} [inst : BEq α] (l : List ((_ : α) × Unit)) (hd : α) (tl : List α),
  Std.Internal.List.insertListIfNewUnit l (hd :: tl) =
    Std.Internal.List.insertListIfNewUnit (Std.Internal.List.insertEntryIfNew hd () l) tl
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_zero : ∀ {α : Type u} [inst : Zero α], ↑0 = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative
`cosh x`.  -/
Complex.hasStrictDerivAt_sinh : ∀ (x : ℂ), HasStrictDerivAt Complex.sinh (Complex.cosh x) x
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `g` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `f` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₂ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt g x → (MeromorphicAt (f - g) x ↔ MeromorphicAt f x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a b : α},
  cmp a b = Ordering.eq → Std.DTreeMap.Const.get? t a = Std.DTreeMap.Const.get? t b
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- See also `IsUniformInducing.completeSpace_congr`
for a version that works for non-injective maps.  -/
completeSpace_congr : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {e : α ≃ β},
  IsUniformEmbedding ⇑e → (CompleteSpace α ↔ CompleteSpace β)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The left adjoint mate `ᘁf : ᘁY ⟶ ᘁX` of a morphism `f : X ⟶ Y`.  -/
CategoryTheory.«termᘁ__1» : Lean.ParserDescr
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [inst : L.Structure M] {N : Type u_2}
  [inst_1 : L.Structure N] {F : Type u_3} [inst_2 : FunLike F M N] [EmbeddingLike F M N] [L.StrongHomClass F M N]
  {φ : L.BoundedFormula α n},
  φ.IsUniversal → ∀ (f : F) {v : α → M} {xs : Fin n → M}, φ.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ.Realize v xs
-- Init.Data.String.Basic
String.Pos.Raw.IsValidForSlice.ofSlice : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.IsValidForSlice s.toSlice p → String.Pos.Raw.IsValid s p
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.beq.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : BEq β] (t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.beq t₁ t₂ =
    if t₁.size ≠ t₂.size then false else t₁.all fun k v => Std.DTreeMap.Internal.Impl.Const.get? t₂ k == some v
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastShiftLeftConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.ShiftTarget w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst aig target).vec.get idx hidx }⟧ =
    if hidx : idx < target.distance then false
    else ⟦assign, { aig := aig, ref := target.vec.get (idx - target.distance) ⋯ }⟧
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.image_le : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : SSet.RelativeMorphism A B φ),
  A.image f.map ≤ B
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- A version of `Commute.cfcₙ` or `IsSelfAdjoint.commute_cfcₙ` which does not require any
interaction with `star` when the base ring is `ℝ≥0`.  -/
Commute.cfcₙ_nnreal : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : Module ℝ A] [inst_3 : IsScalarTower ℝ A A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A]
  [inst_9 : PartialOrder A] [inst_10 : NonnegSpectrumClass ℝ A] [inst_11 : StarOrderedRing A] {a b : A},
  Commute a b → ∀ (f : NNReal → NNReal), Commute (cfcₙ f a) b
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), AddSubgroup.comap f ⊤ = ⊤
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- If the component maps of `𝒰` are open, `𝒰` is quasi-compact. This in particular
applies if `K` is the fppf topology (i.e., flat and of finite presentation) and hence in
particular for étale and Zariski covers.  -/
AlgebraicGeometry.QuasiCompactCover.of_isOpenMap : ∀ {S : AlgebraicGeometry.Scheme} {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover K S} [AlgebraicGeometry.Scheme.JointlySurjective K],
  (∀ (i : 𝒰.I₀), IsOpenMap ⇑(𝒰.f i)) → AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover
-- Mathlib.Algebra.Module.Lattice
/-- The supremum of two lattices is a lattice.  -/
Submodule.IsLattice.sup : ∀ {R : Type u_1} [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : Module A V] [inst_6 : IsScalarTower R A V]
  (M N : Submodule R V) [Submodule.IsLattice A M] [Submodule.IsLattice A N], Submodule.IsLattice A (M ⊔ N)
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_reverse`. -/
List.SortedGT.of_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedGT → l.SortedLT
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
Submodule.mem_closure_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] {x : M} {s : Submodule R M},
  x ∈ s.closure ↔ x ∈ s.topologicalClosure
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.isoMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X}
  (h : f.obj.left ≅ g.obj.left)
  (w : autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) CategoryTheory.MonoOver.isoMk._auto_1),
  (CategoryTheory.MonoOver.isoMk h w).hom = CategoryTheory.MonoOver.homMk h.hom w
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app : ∀ {X Y Z : SSet.Truncated 2} (xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso X Y Z).hom.app xyz =
    CategoryTheory.CategoryStruct.id
      ((((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod
                (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
            ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse
                  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp
              (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))).obj
        xyz)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_ground_isBase_iff : ∀ {α : Type u_1} {M : Matroid α} {B : Set ↑M.E}, (M.restrictSubtype M.E).IsBase B ↔ M.IsBase (Subtype.val '' B)
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal : ∀ {R : Type u} [inst : CommSemiring R] (t : Set (PrimeSpectrum R)) (I : Ideal R),
  t ⊆ PrimeSpectrum.zeroLocus ↑I ↔ I ≤ PrimeSpectrum.vanishingIdeal t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.LinearAlgebra.Pi
/-- `Function.extend s f 0` as a bundled linear map.  -/
Function.ExtendByZero.linearMap : (R : Type u) → {ι : Type x} → {η : Type u_1} → [inst : Semiring R] → (ι → η) → (ι → R) →ₗ[R] η → R
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_eq_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).isEmpty = true ↔
      ∀ (k : α) (h : Std.Internal.List.containsKey k l = true), f k (Std.Internal.List.getValueCast k l h) = false)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.preservesColimit_restrictScalars : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_1, u_3} J] (F : CategoryTheory.Functor J (ModuleCat S))
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat S) AddCommGrpCat))],
  CategoryTheory.Limits.PreservesColimit F (ModuleCat.restrictScalars f)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiff.cle_arrowCongr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂}
  {g : M → F₃ ≃L[𝕜] F₄},
  (ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n fun x => ↑(f x).symm) →
    (ContMDiff I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n fun x => ↑(g x)) →
      ContMDiff I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n fun y => ↑((f y).arrowCongr (g y))
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- Implementation detail.  -/
MonoidAlgebra.rTensorEquivAlgEquiv.invFun : {R : Type u_1} →
  {M : Type u_2} →
    {S : Type u_4} →
      {A : Type u_5} →
        {B : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring A] →
                [inst_3 : CommSemiring B] →
                  [inst_4 : Algebra R S] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : IsScalarTower R S A] →
                            [inst_9 : CommMonoid M] →
                              MonoidAlgebra (TensorProduct R A B) M →ₐ[S] TensorProduct R A (MonoidAlgebra B M)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq.eq_1 : Lean.Grind.CommRing.instBEqMon.beq Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit = true
-- Mathlib.Data.Sym.Sym2
Sym2.diag_diagElem : ∀ {α : Type u_1} {z : Sym2 α} (h : z.IsDiag), Sym2.diag (z.diagElem h) = z
-- Init.Data.Fin.Lemmas
Fin.pred.congr_simp : ∀ {n : ℕ} (i i_1 : Fin (n + 1)) (e_i : i = i_1) (h : i ≠ 0), i.pred h = i_1.pred ⋯
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- When `P = ∃ f₁ ... fₙ, body`, where `exs = [f₁, ..., fₙ]`, this function takes
`act : body` and proves `P` using `Exists.intro`.

Example:
```
exs = []: act
exs = [b]:
  P := ∃ b, body
  Exists.intro b act
exs = [b, c]:
  P := ∃ b c, body
  Exists.intro b (Exists.intro c act)
...
```  -/
ExistsAndEq.withNestedExistsIntro : {P body : Q(Prop)} → List ExistsAndEq.VarQ → Lean.MetaM Q(«$body») → Lean.MetaM Q(«$P»)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- `NonUnitalAlgHom` to `⊤ : NonUnitalSubalgebra R A`.  -/
NonUnitalAlgebra.toTop : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [inst_3 : IsScalarTower R A A] → [inst_4 : SMulCommClass R A A] → A →ₙₐ[R] ↥⊤
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_1 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_1 ()
-- Batteries.Data.Float.Basic
/-- Returns `v, exp` integers such that `f = v * 2^exp`.
(`e` is not minimal, but `v.abs` will be at most `2^53 - 1`.)
Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`).  -/
Float.toRatParts : Float → Option (ℤ × ℤ)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂)
  {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₁.getKey k ⋯
-- Mathlib.LinearAlgebra.Complex.Module
map_imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {B : Type u_2} {F : Type u_3} [inst_4 : AddCommGroup B] [inst_5 : Module ℂ B] [inst_6 : StarAddMonoid B]
  [inst_7 : StarModule ℂ B] [inst_8 : FunLike F A B] [StarHomClass F A B] [LinearMapClass F ℂ A B] (f : F) (x : A),
  f ↑(imaginaryPart x) = ↑(imaginaryPart (f x))
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.tensorObj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = (X ⨿ Y)
-- Mathlib.RepresentationTheory.Basic
Representation.asAlgebraHom_of : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G), ρ.asAlgebraHom ((MonoidAlgebra.of k G) g) = ρ g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Given two groups that are generated by elements `g` and `g'` of the same order,
we obtain an isomorphism sending `g` to `g'`.  -/
mulEquivOfOrderOfEq : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : Group G] →
      [inst_1 : Group G'] →
        {g : G} →
          (∀ (x : G), x ∈ Subgroup.zpowers g) →
            {g' : G'} → (∀ (x : G'), x ∈ Subgroup.zpowers g') → orderOf g = orderOf g' → G ≃* G'
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_one_left : ∀ {G : Type u_1} [inst : Group G] (g : G), ⁅1, g⁆ = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForwardIsoPost_hom_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) (f : CategoryTheory.Over X)
  (X_1 : CategoryTheory.Over f),
  (CategoryTheory.Over.iteratedSliceForwardIsoPost X f).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Over.mk (CategoryTheory.Over.Hom.left X_1.hom))
-- Mathlib.Order.Filter.Cofinite
/-- Given a collection of filters `l i : Filter (α i)` and sets `s i ∈ l i`,
if all but finitely many of `s i` are the whole space,
then their indexed product `Set.pi Set.univ s` belongs to the filter `Filter.pi l`.  -/
Filter.univ_pi_mem_pi : ∀ {ι : Type u_1} {α : ι → Type u_4} {s : (i : ι) → Set (α i)} {l : (i : ι) → Filter (α i)},
  (∀ (i : ι), s i ∈ l i) → (∀ᶠ (i : ι) in Filter.cofinite, s i = Set.univ) → Set.univ.pi s ∈ Filter.pi l
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_sum_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {Ω : ι → Type u_3} {mΩ : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {X : (i : ι) → Ω i → ℝ},
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 (μ i)) →
    ProbabilityTheory.variance (∑ i, fun ω => X i (ω i)) (MeasureTheory.Measure.pi μ) =
      ∑ i, ProbabilityTheory.variance (X i) (μ i)
-- Init.Data.Array.Lemmas
Array.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u_1} {xs : Array α}, xs.isEmpty = false ↔ ∃ x, x ∈ xs
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.compProd_eq_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ],
  μ.compProd κ = μ.bind ⇑(ProbabilityTheory.Kernel.id.prod κ)
-- Mathlib.MeasureTheory.Group.IntegralConvolution
MeasureTheory.integral_conv : ∀ {M : Type u_1} {F : Type u_2} [inst : AddMonoid M] {mM : MeasurableSpace M} [MeasurableAdd₂ M]
  [inst_2 : NormedAddCommGroup F] {μ ν : MeasureTheory.Measure M} {f : M → F} [inst_3 : NormedSpace ℝ F]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν],
  MeasureTheory.Integrable f (μ.conv ν) → ∫ (x : M), f x ∂μ.conv ν = ∫ (x : M), ∫ (y : M), f (x + y) ∂ν ∂μ
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.cone_x : ∀ {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.HasLimit F],
  (CategoryTheory.Limits.limit.cone F).pt = CategoryTheory.Limits.limit F
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.eqOn : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj), Set.EqOn (Prod.fst ∘ ↑e) proj e.source
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.id_apply_of_ne : ∀ (R : Type u) [inst : Semiring R] (M : CategoryTheory.Mat R) (i j : M.obj),
  i ≠ j → CategoryTheory.CategoryStruct.id M i j = 0
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_eq_zero_iff_eq_neg : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit b → (a + b = 0 ↔ a = -b)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instSemigroupWithZero : {𝕜 : Type u_1} → [inst : NonUnitalSeminormedRing 𝕜] → SemigroupWithZero ↑(Metric.ball 0 1)
-- Mathlib.Topology.Compactness.Compact
Pi.isCompact_iff_of_isClosed : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : Set ((i : ι) → X i)},
  IsClosed s → (IsCompact s ↔ ∀ (i : ι), IsCompact (Function.eval i '' s))
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierTransformInv : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : InnerProductSpace ℝ E] →
        [FiniteDimensional ℝ E] →
          [inst_3 : MeasurableSpace E] →
            [BorelSpace E] →
              [inst_5 : AddCommGroup F] →
                [inst_6 : Module ℂ F] →
                  [inst_7 : TopologicalSpace F] →
                    [IsTopologicalAddGroup F] →
                      [ContinuousConstSMul ℂ F] →
                        FourierTransformInv (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.zpowers_one_eq_bot : ∀ {G : Type u_1} [inst : Group G], Subgroup.zpowers 1 = ⊥
-- Mathlib.Algebra.Group.Defs
/-- Addition is commutative in a commutative additive magma.  -/
AddCommSemigroup.add_comm : ∀ {G : Type u} [self : AddCommSemigroup G] (a b : G), a + b = b + a
-- Init.Data.BitVec.Lemmas
BitVec.shiftRight_sub_one_eq_shiftConcat : ∀ {w wn : ℕ} (n : BitVec w), 0 < wn → n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1))
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.runM : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ →
      Lean.Elab.ContextInfo →
        Lean.LocalContext →
          Lean.Server.Completion.M✝ Unit → Lean.Server.CancellableM (Array Lean.Lsp.ResolvableCompletionItem)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isSome_minKey?_modifyKey_eq_isSome : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β}
  {l : List ((_ : α) × β)},
  (Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l)).isSome = (Std.Internal.List.minKey? l).isSome
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → aig.Ref → aig.RefVec w → aig.RefVec w → Std.Sat.AIG.RefVec.IfInput aig w
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTrustSubtypeMk : Lean.Options → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P Q : Fin 3 → R),
  W'.addXYZ P Q = ![W'.addX P Q, W'.addY P Q, WeierstrassCurve.Jacobian.addZ P Q]
-- Mathlib.Data.PEquiv
PEquiv.instFunLikeOption : {α : Type u} → {β : Type v} → FunLike (α ≃. β) α (Option β)
-- Mathlib.Topology.Order.OrderClosed
/-- If `α` is a topological space and a preorder, `ClosedIciTopology α` means that `Ici a` is
closed for all `a : α`.  -/
ClosedIciTopology : (α : Type u_1) → [TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.Data.Seq.Basic
Stream'.Seq.set_nil : ∀ {α : Type u} (n : ℕ) (x : α), Stream'.Seq.nil.set n x = Stream'.Seq.nil
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.Nondegenerate.rank_rad_polar_le : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P},
  QuadraticMap.Nondegenerate → Module.rank R ↥(LinearMap.ker Q.polarBilin) ≤ 1
-- Init.Data.Nat.Lemmas
Nat.pow_mul' : ∀ (a m n : ℕ), a ^ (m * n) = (a ^ n) ^ m
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_def_le_sqrt : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
isLUB_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
  BddAbove (Set.range f) → IsLUB (Set.range f) (⨆ i, f i)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.locallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.LocallySmall.{w, v, u} C