mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Basic
/-- In a complete space, a function is integrable if and only if its integral sums form a Cauchy
net. Here we restate this fact in terms of `∀ ε > 0, ∃ r, ...`.  -/
BoxIntegral.integrable_iff_cauchy_basis : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F],
  BoxIntegral.Integrable I l f vol ↔
    ∀ ε > 0,
      ∃ r,
        (∀ (c : NNReal), l.RCond (r c)) ∧
          ∀ (c₁ c₂ : NNReal) (π₁ π₂ : BoxIntegral.TaggedPrepartition I),
            l.MemBaseSet I c₁ (r c₁) π₁ →
              π₁.IsPartition →
                l.MemBaseSet I c₂ (r c₂) π₂ →
                  π₂.IsPartition → dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε
-- Mathlib.Topology.Order.OrderClosed
not_tendsto_nhds_of_tendsto_atBot : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [NoBotOrder α] [inst_2 : TopologicalSpace α] [ClosedIicTopology α]
  {l : Filter β} [l.NeBot] {f : β → α}, Filter.Tendsto f l Filter.atBot → ∀ (a : α), ¬Filter.Tendsto f l (nhds a)
-- Mathlib.RingTheory.WittVector.Compare
PadicInt.lift.congr_simp : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f f_1 : (k : ℕ) → R →+* ZMod (p ^ k)} (e_f : f = f_1)
  [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1),
  PadicInt.lift f_compat = PadicInt.lift ⋯
-- Lean.Data.FuzzyMatching
/-- Heuristic to rate a match.  -/
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.matchResult : String → String → ℕ → ℕ → Lean.FuzzyMatching.CharRole → Lean.FuzzyMatching.CharRole → Lean.FuzzyMatching.Score✝ → Int16
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.smul_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (s : Set M),
  a • Submodule.span R s = Submodule.span R (a • s)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_inv : ∀ {ι : Type u_2} {G : Type u_4} [inst : DivisionCommMonoid G] {m : Multiset ι} {f : ι → G},
  (Multiset.map (fun i => (f i)⁻¹) m).prod = (Multiset.map f m).prod⁻¹
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Promise.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (prom : IO.PromisePointed✝.type) (h : Nonempty α),
  sizeOf { prom := prom, h := h } = 1 + sizeOf prom + sizeOf h
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_of : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (i : ι) (m : M), ((DirectSum.of (fun x => M) i) m).toAddMonoidAlgebra = AddMonoidAlgebra.single i m
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step6 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (G' : Type u) [inst : Group G'] [Finite G'],
        Nat.card G' < Nat.card G →
          ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
      (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G], IsPGroup (Nat.card ↥N).minFac ↥N
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁_self : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q : Turing.TM2.Stmt Γ Λ σ}, q ∈ Turing.TM2.stmts₁ q
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk_surjective : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X}, Function.Surjective Path.Homotopic.Quotient.mk
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.constOfIsEmptyLIE_symm_apply : ∀ (𝕜 : Type u) (E : Type wE) (F : Type wF) (ι : Type v) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι] (f : E [⋀^ι]→L[𝕜] F),
  (ContinuousAlternatingMap.constOfIsEmptyLIE 𝕜 E F ι).symm f = f 0
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.MetavarContext.LevelMVarToParam.main.visitApp : Lean.Expr → Array Lean.Expr → Lean.MetavarContext.LevelMVarToParam.M Lean.Expr
-- Init.Data.BitVec.Lemmas
BitVec.getElem_zero : ∀ {i w : ℕ} (h : i < w), (0#w)[i] = false
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.Y_sub_polynomialY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, Polynomial.X - W'.polynomialY = W'.negPolynomial
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.brecOn.go : {motive : Mathlib.Tactic.Linarith.CompSource → Sort u} →
  (t : Mathlib.Tactic.Linarith.CompSource) →
    ((t : Mathlib.Tactic.Linarith.CompSource) → Mathlib.Tactic.Linarith.CompSource.below t → motive t) →
      motive t ×' Mathlib.Tactic.Linarith.CompSource.below t
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The sum type `X ⊕ Y` is a binary coproduct for `X` and `Y`.  -/
CategoryTheory.Limits.Types.binaryCoproductColimit : (X Y : Type u) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.binaryCoproductCocone X Y)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the condition that the denominator belongs to the given morphism property  -/
CategoryTheory.MorphismProperty.LeftFraction.hs : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (self : W.LeftFraction X Y), W self.s
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNat_of_lt' : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNat n).toNat = n
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_top : ∀ {V : Type u_1} (v : V) [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.neighborFinset v = {v}ᶜ
-- Mathlib.LinearAlgebra.Dimension.Free
OrzechProperty.bijective_of_surjective_of_finrank_le : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [OrzechProperty R]
  [Module.Finite R M] [Module.Finite R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f → Module.finrank R M ≤ Module.finrank R M' → Function.Bijective ⇑f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
nonpos_of_add_le_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightReflectLE α] {a b : α}, a + b ≤ b → a ≤ 0
-- Lean.ExtraModUses
_private.Lean.ExtraModUses.0.Lean.isExtraRevModUseExt : Lean.SimplePersistentEnvExtension Unit Unit
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- If elements of a list commute with each other, then their product does not
depend on the order of elements.  -/
List.Perm.prod_eq' : ∀ {M : Type u_4} [inst : Monoid M] {l₁ l₂ : List M}, l₁.Perm l₂ → List.Pairwise Commute l₁ → l₁.prod = l₂.prod
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.slice_eq_startPos : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, p₀.slice p₀ p₁ ⋯ h = (s.slice p₀ p₁ ⋯).startPos
-- Mathlib.Topology.Compactness.LocallyCompact
Topology.IsClosedEmbedding.locallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactSpace Y]
  {f : X → Y}, Topology.IsClosedEmbedding f → LocallyCompactSpace X
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] (f : NumberField.mixedEmbedding.realMixedSpace K → E),
  ∫ (x : NumberField.mixedEmbedding.realMixedSpace K) in (NumberField.mixedEmbedding.polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f (↑(NumberField.mixedEmbedding.polarCoordReal K).symm x) =
    ∫ (x : NumberField.mixedEmbedding.realMixedSpace K), f x
-- Mathlib.Topology.Inseparable
specializes_iff_closure_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ closure {y} ⊆ closure {x}
-- Init.Data.Array.Lemmas
Array.foldr_eq_foldl_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β → β} {b : β},
  Array.foldr f b xs = Array.foldl (fun x y => f y x) b xs.reverse
-- Init.Control.Lawful.MonadLift.Lemmas
instMonadLiftTOfMonadLift_instMonadLiftTOfPure : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [inst : Monad m] [inst_1 : Monad n] {x : MonadLift m n}
  [LawfulMonadLift m n], instMonadLiftTOfMonadLift Id m n = Id.instMonadLiftTOfPure
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.card_support_C_mul_X_pow_le_one : ∀ {R : Type u} [inst : Semiring R] {c : R} {n : ℕ}, (Polynomial.C c * Polynomial.X ^ n).support.card ≤ 1
-- Mathlib.Analysis.Convex.Cone.TensorProduct
/-- If `C₁` is a proper cone and `C₂` is a simplicial and generating cone, then their minimal
and maximal tensor products are equal.  -/
PointedCone.minTensorProduct_eq_max_of_simplicial_generating_right : ∀ {E : Type u_1} {F : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] [FiniteDimensional ℝ F]
  [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] (C₁ : ProperCone ℝ F) (C₂ : PointedCone ℝ E),
  C₂.IsSimplicial → Submodule.span ℝ ↑C₂ = ⊤ → (↑C₁).minTensorProduct C₂ = (↑C₁).maxTensorProduct C₂
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))),
  AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine.symm I = AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop I
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c c' : CategoryTheory.Limits.PushoutCocone f g} (e : c ≅ c') (x₁ : X₁)
  (x₂ : X₂),
  (CategoryTheory.ConcreteCategory.hom c.inl) x₁ = (CategoryTheory.ConcreteCategory.hom c.inr) x₂ →
    (CategoryTheory.ConcreteCategory.hom c'.inl) x₁ = (CategoryTheory.ConcreteCategory.hom c'.inr) x₂
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_nat : ∀ {R : Type u_1} [inst : Semiring R] (s : Set R), Algebra.adjoin ℕ s = subalgebraOfSubsemiring (Subsemiring.closure s)
-- Std.Time.Date.ValidDate
/-- Transforms a `Day.Ordinal.OfYear` into a tuple of a `Month` and a `Day`.
 -/
Std.Time.ValidDate.ofOrdinal : {leap : Bool} → Std.Time.Day.Ordinal.OfYear leap → Std.Time.ValidDate leap
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instDecidableLtOrdinal : {x y : Std.Time.Minute.Ordinal} → Decidable (x < y)
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.addEquiv_symm_map_smul_smul : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [inst_4 : Module S M] (r : R) (s : S) (x : M),
  (RestrictScalars.addEquiv R S M).symm ((r • s) • x) = r • (RestrictScalars.addEquiv R S M).symm (s • x)
-- Mathlib.Topology.Sheaves.Alexandrov
/-- This is the main construction in this file showing that the right Kan extension
of `F : X ⥤ C` along `principals : X ⥤ (Opens X)ᵒᵖ` is a sheaf, by showing that a certain
cone is a limit cone.

See `isSheaf_principalsKanExtension` for the main application.
 -/
Alexandrov.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasLimits C] →
      {X : TopCat} →
        [inst_2 : Preorder ↑X] →
          [inst_3 : Topology.IsUpperSet ↑X] →
            (F : CategoryTheory.Functor (↑X) C) →
              (α : Type v) →
                (Us : α → TopologicalSpace.Opens ↑X) →
                  CategoryTheory.Limits.IsLimit
                    ((Alexandrov.principalsKanExtension F).mapCone
                      (TopCat.Presheaf.SheafCondition.opensLeCoverCocone Us).op)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- `MvPowerSeries.constantCoeff` is continuous  -/
MvPowerSeries.WithPiTopology.continuous_constantCoeff : ∀ {σ : Type u_1} (R : Type u_2) [inst : TopologicalSpace R] [inst_1 : Semiring R],
  Continuous ⇑MvPowerSeries.constantCoeff
-- Mathlib.Geometry.Manifold.Riemannian.Basic
eventually_enorm_mfderivWithin_symm_extChartAt_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M),
  ∃ C > 0,
    ∀ᶠ (y : E) in nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I),
      ‖mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
-- Init.Data.FloatArray.Basic
FloatArray.foldl : {β : Type v} → (β → Float → β) → β → (as : FloatArray) → optParam ℕ 0 → optParam ℕ as.size → β
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If `K` is of characteristic `0` and there is a primitive `n`-th root of unity in `K`,
then `cyclotomic n K` comes from a unique polynomial with integer coefficients.  -/
Polynomial.unique_int_coeff_of_cycl : ∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] [CharZero K] {ζ : K} {n : ℕ+},
  IsPrimitiveRoot ζ ↑n → ∃! P, Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' (↑n) K
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.coroot_mem_corootSpace : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (α : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.coroot α ∈ LieAlgebra.corootSpace ⇑α
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toCostructuredArrow_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (j : J),
  c.toCostructuredArrow.obj j = CategoryTheory.CostructuredArrow.mk (c.ι.app j)
-- Mathlib.Data.Finsupp.BigOperators
Multiset.support_sum_subset : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] (s : Multiset (ι →₀ M)),
  s.sum.support ⊆ (Multiset.map Finsupp.support s).sup
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_map_prodMk₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α},
  AEMeasurable Y μ → (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
-- Mathlib.Geometry.Euclidean.Volume.Measure
Isometry.euclideanHausdorffMeasure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  [inst_3 : EMetricSpace Y] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℕ},
  Isometry f →
    ∀ (s : Set X),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d) (f '' s) =
        (MeasureTheory.Measure.euclideanHausdorffMeasure d) s
-- Init.Data.Option.Lemmas
Option.guard_le_some : ∀ {α : Type u_1} [inst : LE α], (∀ (x : α), x ≤ x) → ∀ {x : α} {p : α → Bool}, Option.guard p x ≤ some x
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumMap_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language}
  {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ℕ) (a : L.Relations _n ⊕ L₁.Relations _n),
  (ϕ.sumMap ψ).onRelation a = Sum.map (fun f => ϕ.onRelation f) (fun f => ψ.onRelation f) a
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instCompleteLattice : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → CompleteLattice (ConvexCone R M)
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.mul_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M}, Continuous f → ∀ (b : M), Continuous fun x => f x * b
-- Mathlib.Topology.Sets.VietorisTopology
/-- The Vietoris topology has a basis consisting of sets of the form
`{s | s ⊆ U₁ ∪ … ∪ Uₙ, s ∩ U₁ ≠ ∅, …, s ∩ Uₙ ≠ ∅}`, where `U₁, …, Uₙ` are open sets.  -/
TopologicalSpace.vietoris.isTopologicalBasis : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.IsTopologicalBasis
    ((fun u => {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen U})
-- Lean.Elab.Term.TermElabM
/-- Tactic metavariable arising from an autoparam for a structure field.  -/
Lean.Elab.Term.TacticMVarKind.fieldAutoParam : Lean.Name → Lean.Name → Lean.Elab.Term.TacticMVarKind
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_mul_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (p m n : ℕ) [inst_1 : ExpChar R p] (x : R),
  (iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fromProd_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y),
  ((CategoryTheory.Comma.fromProd L R).map f).left = f.1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Rco α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Rco α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_neg : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Neg β] (f : UniformOnFun α β 𝔖),
  (UniformOnFun.toFun 𝔖) (-f) = -(UniformOnFun.toFun 𝔖) f
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- Product of affine spaces is associative up to continuous affine isomorphism.  -/
ContinuousAffineEquiv.prodAssoc : (k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      (P₃ : Type u_4) →
        {V₁ : Type u_6} →
          {V₂ : Type u_7} →
            {V₃ : Type u_8} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V₁] →
                  [inst_2 : Module k V₁] →
                    [inst_3 : AddTorsor V₁ P₁] →
                      [inst_4 : TopologicalSpace P₁] →
                        [inst_5 : AddCommGroup V₂] →
                          [inst_6 : Module k V₂] →
                            [inst_7 : AddTorsor V₂ P₂] →
                              [inst_8 : TopologicalSpace P₂] →
                                [inst_9 : AddCommGroup V₃] →
                                  [inst_10 : Module k V₃] →
                                    [inst_11 : AddTorsor V₃ P₃] →
                                      [inst_12 : TopologicalSpace P₃] → (P₁ × P₂) × P₃ ≃ᴬ[k] P₁ × P₂ × P₃
-- Mathlib.Computability.Language
Language.kstar_eq_iSup_pow : ∀ {α : Type u_1} (l : Language α), KStar.kstar l = ⨆ i, l ^ i
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
min_le_of_mul_le_sq : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b c : M},
  a * b ≤ c ^ 2 → min a b ≤ c
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.toOverSectionsAdj_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (I : C) [inst_2 : CategoryTheory.Closed I]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : C),
  (CategoryTheory.Over.toOverSectionsAdj I).unit.app X =
    { toFun := CategoryTheory.Over.sectionsCurry, invFun := CategoryTheory.Over.sectionsUncurry, left_inv := ⋯,
        right_inv := ⋯ }
      (CategoryTheory.CategoryStruct.id ((CategoryTheory.toOver I).obj X))
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalRingWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [NonUnitalRing α] → NonUnitalRing (WithConv (Matrix m n α))
-- Lean.Server.Completion.EligibleHeaderDecls
/-- Returns the declarations in the header for which `allowCompletion env decl` is true, caching them
if not already cached.
 -/
Lean.Server.Completion.getEligibleHeaderDecls : Lean.Environment → Lean.MetaM Lean.Server.Completion.EligibleHeaderDecls
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- **Alias** of `CategoryTheory.SimplicialObject.Homotopy.congr_sSetHomologyMap`.

---

Simplicially homotopic maps of simplicial sets induce the same map on
homology of the singular chain complex (with coefficients in `R`).
The assumption is in `SimplicialObject.Homotopy`,
see also `SSet.Homotopy.congr_homologyMap` for the
variant using `SSet.Homotopy` as an assumption.
 -/
CategoryTheory.SimplicialObject.Homotopy.congr_homologyMap_singularChainComplexFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {X Y : SSet} {f g : X ⟶ Y}
  [inst_3 : CategoryTheory.CategoryWithHomology C] (H : CategoryTheory.SimplicialObject.Homotopy f g) (R : C) (n : ℕ),
  SSet.homologyMap f R n = SSet.homologyMap g R n
-- Mathlib.CategoryTheory.Monoidal.CommComon_
/-- The trivial commutative comonoid object. We later show this is initial in `CommComon C`.  -/
CategoryTheory.CommComon.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommComon C
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_prod : ∀ {b : ℝ} {α : Type u_1} (s : Finset α) (f : α → ℝ),
  (∀ x ∈ s, f x ≠ 0) → Real.logb b (∏ i ∈ s, f i) = ∑ i ∈ s, Real.logb b (f i)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) {ι : Type u_1} (Z : ι → C)
  (g : (i : ι) → Z i ⟶ X) [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasPullback (g i) f],
  (CategoryTheory.Presieve.ofArrows (fun i => CategoryTheory.Limits.pullback (g i) f) fun x =>
      CategoryTheory.Limits.pullback.snd (g x) f) =
    CategoryTheory.Presieve.pullbackArrows f (CategoryTheory.Presieve.ofArrows Z g)
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.ModelTheory.Quotients
/-- The underlying first-order structure  -/
FirstOrder.Language.Prestructure.toStructure : {L : FirstOrder.Language} → {M : Type u_1} → (s : Setoid M) → [self : L.Prestructure s] → L.Structure M