mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X : C)
  (i₁ i₂ : (data X).I₀) {Y₀ : C₀} (p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)) (p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)),
  CategoryTheory.CategoryStruct.comp p₁ ((data X).f i₁) = CategoryTheory.CategoryStruct.comp p₂ ((data X).f i₂) →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i₁)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p₁) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i₂)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p₂)
-- Lean.Elab.InfoTree.Main
Lean.Elab.TermInfo.runMetaM : {α : Type} → Lean.Elab.TermInfo → Lean.Elab.ContextInfo → Lean.MetaM α → IO α
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  [toContainsIdentities : W.ContainsIdentities] [toIsStableUnderComposition : W.IsStableUnderComposition],
  W.IsMultiplicative
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_inter : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  t ∈ nhds x → mfderiv[s ∩ t] f x = mfderiv[s] f x
-- Mathlib.Tactic.ClickSuggestions.FindPremises
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.mk.injEq : ∀
  (rw :
    Array
      (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma))
  (grw :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma))
  (app :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma))
  (appAt :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma))
  (rw_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma))
  (grw_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma))
  (app_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma))
  (appAt_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)),
  ({ rw := rw, grw := grw, app := app, appAt := appAt } =
      { rw := rw_1, grw := grw_1, app := app_1, appAt := appAt_1 }) =
    (rw = rw_1 ∧ grw = grw_1 ∧ app = app_1 ∧ appAt = appAt_1)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instVAdd.eq_1 : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : VAdd K V], WithLp.instVAdd p K V = Equiv.vadd K (WithLp.equiv p V)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_map : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A), ↑(Subalgebra.map f S) = ⇑f '' ↑S
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_eq_assemble₁ : ∀ {b : ByteArray} (hb : 1 ≤ b.size)
  (h : ByteArray.utf8DecodeChar?.parseFirstByte b[0] = ByteArray.utf8DecodeChar?.FirstByte.done),
  b.utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₁ b[0] h
-- Mathlib.Topology.Inseparable
/-- A collection of equivalent definitions of `x ⤳ y`. The public API is given by `iff` lemmas
below.  -/
specializes_TFAE : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x y : X),
  [x ⤳ y, pure x ≤ nhds y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm_inv_mul_lt' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖a⁻¹ * b‖ < r
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isOpen_singleton_iff : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] {x : α}, IsOpen {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for isomorphisms in `ComposableArrows C 0`.  -/
CategoryTheory.ComposableArrows.isoMk₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.ComposableArrows C 0} →
      (F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ≅
          G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1) →
        (F ≅ G)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.sum_add_tsum_compl : ∀ {ι : Type u_4} (s : Finset ι) (f : ι → ENNReal), ∑ i ∈ s, f i + ∑' (i : ↑(↑s)ᶜ), f ↑i = ∑' (i : ι), f i
-- Lean.Elab.DefView
Lean.Elab.DefViewElabHeaderData.mk.injEq : ∀ (shortDeclName declName : Lean.Name) (levelNames : List Lean.Name) (binderIds : Array Lean.Syntax) (numParams : ℕ)
  (type : Lean.Expr) (shortDeclName_1 declName_1 : Lean.Name) (levelNames_1 : List Lean.Name)
  (binderIds_1 : Array Lean.Syntax) (numParams_1 : ℕ) (type_1 : Lean.Expr),
  ({ shortDeclName := shortDeclName, declName := declName, levelNames := levelNames, binderIds := binderIds,
        numParams := numParams, type := type } =
      { shortDeclName := shortDeclName_1, declName := declName_1, levelNames := levelNames_1, binderIds := binderIds_1,
        numParams := numParams_1, type := type_1 }) =
    (shortDeclName = shortDeclName_1 ∧
      declName = declName_1 ∧
        levelNames = levelNames_1 ∧ binderIds = binderIds_1 ∧ numParams = numParams_1 ∧ type = type_1)
-- Mathlib.Algebra.Group.Defs
CommMonoid.toMonoid : {M : Type u} → [self : CommMonoid M] → Monoid M
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioc_sub_one_left_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] [NoMinOrder α] (a b : α), Finset.Ioc (a - 1) b = Finset.Icc a b
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_ne_zero : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  x ≠ -1 → n ≠ 0 → ∑ i ∈ Finset.range n, x ^ i ≠ 0
-- Mathlib.Order.WithBot
WithBot.coe_eq_coe : ∀ {α : Type u_1} {a b : α}, ↑a = ↑b ↔ a = b
-- Mathlib.Order.Interval.Set.LinearOrder
/-- **Alias** of `Set.Ioi_sdiff_Ioi`. -/
Set.Ioi_diff_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a \ Set.Ioi b = Set.Ioc a b
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.nhds_eq : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
  nhds f =
    ⨅ s ∈ 𝔖,
      ⨅ V ∈ uniformity β, Filter.principal {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V}
-- Mathlib.Tactic.Ring.Common
/-- Evaluates expression `e` of type `α` into a normalized representation as a polynomial.
This is the main driver of `ring`, which calls out to `evalAdd`, `evalMul` etc.

* `rc` tells us how to normalize constants in `α`.
* `rcℕ` tells us how to normalize constants in exponents.
 -/
Mathlib.Tactic.Ring.Common.eval : Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompute bt sα →
            Mathlib.Tactic.Ring.Common.Cache sα →
              (e : Q(«$α»)) →
                Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) e)
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.toMonoidHom_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β), (↑↑f).toFun = ⇑f
-- Mathlib.Data.Fin.Rev
Fin.rev_lt_iff : ∀ {n : ℕ} {i j : Fin n}, i.rev < j ↔ j.rev < i
-- Mathlib.Topology.UniformSpace.Compact
/-- On a compact uniform space, the topology determines the uniform structure, entourages are
exactly the neighborhoods of the diagonal.  -/
nhdsSet_diagonal_eq_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] [CompactSpace α], nhdsSet (Set.diagonal α) = uniformity α
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.zero_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : StarAddMonoid A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : StarAddMonoid B] (a : A), 0 a = 0
-- Init.Data.SInt.Bitwise
Int8.neg_eq_not_add : ∀ (a : Int8), -a = ~~~a + 1
-- Init.Data.Int.DivMod.Lemmas
Int.lt_ediv_of_mul_lt : ∀ {a b c : ℤ}, 0 ≤ b → b ∣ c → a * b < c → a < c / b
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_eq_omega_natCast : ∀ {o : Ordinal.{u}} {n : ℕ}, Ordinal.lift.{v, u} o = Ordinal.omega ↑n ↔ o = Ordinal.omega ↑n
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_of_subsingleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [h : Subsingleton E] (f : E → F) (x : E), HasFDerivAt f 0 x
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.ensureType : Lean.Expr → Lean.MetaM Unit
-- Lean.Data.Lsp.Internal
/-- LSP type for `Lean.OpenDecl`.  -/
Lean.Lsp.OpenNamespace : Type
-- Mathlib.Data.Num.Basic
/-- `bit1 n` appends a `1` to the end of `n`, where `bit1 n = n1`.  -/
Num.bit1 : Num → Num
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.AlmostMono.mk : {α : Type u_5} →
  {ι : Type u_6} →
    {κ : Type u_7} →
      {C : (ι → Option α) → κ} →
        (line : Combinatorics.Line (Option α) ι) →
          (color : κ) → (∀ (x : α), C (↑line (some x)) = color) → Combinatorics.Line.AlmostMono C
-- Mathlib.Order.UpperLower.Closure
/-- **Alias** of the reverse direction of `bddBelow_upperClosure`. -/
BddBelow.upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow s → BddBelow ↑(upperClosure s)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.AEStronglyMeasurable.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {a : α} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel β γ} {δ : Type u_5}
  [inst : TopologicalSpace δ] {f : γ → δ},
  MeasureTheory.AEStronglyMeasurable f ((η.comp κ) a) → ∀ᵐ (x : β) ∂κ a, MeasureTheory.AEStronglyMeasurable f (η x)
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a formal power series is exactly `n` some coefficient
of degree `n` is nonzero,
and the `d`th coefficient is `0` for all `d` such that `degree d < n`.  -/
MvPowerSeries.order_eq_nat : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {n : ℕ},
  f.order = ↑n ↔
    (∃ d, (MvPowerSeries.coeff d) f ≠ 0 ∧ Finsupp.degree d = n) ∧
      ∀ (d : σ →₀ ℕ), Finsupp.degree d < n → (MvPowerSeries.coeff d) f = 0
-- Mathlib.Data.DFinsupp.Order
DFinsupp.support_tsub : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : (i : ι) → Sub (α i)]
  [inst_4 : ∀ (i : ι), OrderedSub (α i)] {f g : Π₀ (i : ι), α i} [inst_5 : DecidableEq ι]
  [inst_6 : (i : ι) → (x : α i) → Decidable (x ≠ 0)], (f - g).support ⊆ f.support
-- Mathlib.Data.Set.Card
Set.encard_empty : ∀ {α : Type u_1}, ∅.encard = 0
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.setRed.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      ((c : RBTree.RBColor) →
          (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)) →
        (Unit → motive RBTree.RBNode.nil) → motive x
-- Mathlib.RingTheory.RingHom.Finite
RingHom.localization_away_map_finite : ∀ (R S R' S' : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing R'] [inst_3 : CommRing S']
  [inst_4 : Algebra R R'] (f : R →+* S) [inst_5 : Algebra S S'] (r : R) [inst_6 : IsLocalization.Away r R']
  [inst_7 : IsLocalization.Away (f r) S'], f.Finite → (IsLocalization.Away.map R' S' f r).Finite
-- Mathlib.GroupTheory.Congruence.Defs
Con.comap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y)
  (c : Con N), Con.comap f H c = { toSetoid := Setoid.comap f c.toSetoid, mul' := ⋯ }
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.congr_arg : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η : ApplicativeTransformation F G) {α : Type u} {x y : F α}, x = y → (fun {α} => η.app α) x = (fun {α} => η.app α) y
-- Mathlib.Topology.Algebra.Module.EmbeddingOfLocal
LinearMap.isInducing_of_restrict_nhds_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜₁]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜₁ E]
  [inst_5 : Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} {f : E →ₛₗ[σ] F} [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F]
  [IsTopologicalAddGroup E] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] [RingHomIsometric σ]
  {V : Set E}, V ∈ nhds 0 → Topology.IsInducing (V.domRestrict ⇑f) → Topology.IsInducing ⇑f
-- Mathlib.Order.Lex
instDecidableEqLex : (α : Type u_2) → [DecidableEq α] → DecidableEq (Lex α)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
/-- An element of a minimal prime is a zero divisor.  -/
notMem_nonZeroDivisors_of_mem_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R} {q : Ideal R}, x ∈ q → q ∈ minimalPrimes R → x ∉ nonZeroDivisors R
-- Std.Net.Addr
Std.Net.SocketAddressV4.instToString : ToString Std.Net.SocketAddressV4
-- Mathlib.Analysis.Convex.GaugeRescale
mapsTo_gaugeRescale_interior : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {s t : Set E}, t ∈ nhds 0 → Convex ℝ t → Set.MapsTo (gaugeRescale s t) (interior s) (interior t)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_zero_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (i : σ), MvPolynomial.coeff 0 (MvPolynomial.X i) = 0
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.hasLimitCompEvaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (k : K) [CategoryTheory.Limits.HasLimit (F.flip.obj k)],
  CategoryTheory.Limits.HasLimit (F.comp ((CategoryTheory.evaluation K C).obj k))
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_hom_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g) {Z : F.obj a ⟶ F.obj b} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map₂ η.hom) (CategoryTheory.CategoryStruct.comp (F.map₂ η.inv) h) = h
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.isTopologicalBasis : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u →
    ∀ {B : (i : ι) → Set (Set ↥(u i))},
      (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (B i)) →
        TopologicalSpace.IsTopologicalBasis (⋃ i, (fun x => Subtype.val '' x) '' B i)
-- Mathlib.Algebra.Quaternion
Quaternion.coe_nnratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ≥0), ↑↑q = ↑q
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.const.eq_2 : ∀ (n : ℕ), Nat.Partrec.Code.const n.succ = Nat.Partrec.Code.succ.comp (Nat.Partrec.Code.const n)
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.integer_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K],
  (S.integer K).toSubring =
    ⨅ v, ⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.toSubring
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText : Inhabited Lean.Meta.Tactic.TryThis.SuggestionText
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.syntheticMVars : Lean.Elab.Term.State → Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.exists_of_simplex : ∀ {X : SSet} (s : X.obj (Opposite.op { len := 2 })), ∃ x₀ x₁ x₂ e₀₁ e₁₂ e₀₂ h, h.simplex = s
-- Lean.Parser.Syntax
Lean.Parser.Command.syntaxAbbrev : Lean.Parser.Parser
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hom_id : ∀ {M : AddCommMonCat}, AddCommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id M) = AddMonoidHom.id ↑M
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as
an algebra to a direct sum of components.  -/
DirectSum.decomposeAlgEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (𝒜 : ι → Submodule R A) → [inst_5 : GradedAlgebra 𝒜] → A ≃ₐ[R] DirectSum ι fun i => ↥(𝒜 i)
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_comap : ∀ {E : Type v} [inst : Field E] (A : Subfield E) {L : Type v} [inst_1 : Field L] (f : L →+* E) (B : Subfield L),
  (Subfield.comap f A).relrank B = A.relrank (Subfield.map f B)
-- Lean.Meta.Tactic.Grind.Intro
/-- Asserts all facts in the `goal` fact queue.
Returns `true` if the queue was not empty and `false` otherwise.
 -/
Lean.Meta.Grind.Action.assertAll : Lean.Meta.Grind.Action
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObj_src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).src = (X.src ⨯ Y.src)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_inv_eq : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a b : A) {x : NNReal},
  x ≠ 0 →
    autoParam (0 ≤ a) CFC.nnrpow_inv_eq._auto_1 →
      autoParam (0 ≤ b) CFC.nnrpow_inv_eq._auto_3 → (a ^ x⁻¹ = b ↔ b ^ x = a)
-- Mathlib.Analysis.Convex.Extrema
/-- A local minimum of a convex function is a global minimum.  -/
IsMinOn.of_isLocalMin_of_convex_univ : ∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [inst_5 : AddCommGroup β] [inst_6 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_8 : Module ℝ β] [IsOrderedModule ℝ β] [PosSMulReflectLE ℝ β] {f : E → β} {a : E},
  IsLocalMin f a → ConvexOn ℝ Set.univ f → ∀ (x : E), f a ≤ f x
-- Mathlib.Data.Seq.Computation
Computation.instMembership : {α : Type u} → Membership α (Computation α)
-- Mathlib.Algebra.Ring.Parity
neg_one_pow_eq_one_iff_even : ∀ {R : Type u_4} [inst : Monoid R] [inst_1 : HasDistribNeg R] {n : ℕ}, -1 ≠ 1 → ((-1) ^ n = 1 ↔ Even n)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLastD.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → α → Sort u_2) (a : α) (as : List α) (x : α) (h_1 : (a₀ : α) → motive [] a₀)
  (h_2 : (a : α) → (as : List α) → (x : α) → motive (a :: as) x),
  (match a :: as, x with
    | [], a₀ => h_1 a₀
    | a :: as, x => h_2 a as x) =
    h_2 a as x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A category `HasBinaryProducts` if it has all limits of shape `Discrete WalkingPair`,
i.e. if it has a product for every pair of objects.  -/
CategoryTheory.Limits.HasBinaryProducts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital ring homomorphism from a `Ring` to a `SeminormedRing` induces a
`SeminormedRing` structure on the domain.

See note [reducible non-instances]  -/
SeminormedRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : Ring R] → [inst_2 : SeminormedRing S] → [NonUnitalRingHomClass F R S] → F → SeminormedRing R
-- Mathlib.Order.LiminfLimsup
Filter.le_limsup_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.le_limsup_iff._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.le_limsup_iff._auto_3 →
      (x ≤ Filter.limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence to a constant function is equivalent to convergence in `p ×ˢ ⊤`.  -/
tendsto_prod_top_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {c : β},
  Filter.Tendsto (↿F) (p ×ˢ ⊤) (nhds c) ↔ TendstoUniformly F (fun x => c) p
-- Mathlib.Topology.Order.Basic
nhds_bot_order : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : OrderBot α] [OrderTopology α],
  nhds ⊥ = ⨅ l, ⨅ (_ : ⊥ < l), Filter.principal (Set.Iio l)
-- Mathlib.Analysis.MeanInequalities
NNReal.inner_le_Lp_mul_Lq_tsum : ∀ {ι : Type u} {f g : ι → NNReal} {p q : ℝ},
  p.HolderConjugate q →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ q) →
        ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)