mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- **Alias** of `Submodule.ClosedComplemented.of_finiteDimensional_quotient`. -/
Submodule.ClosedComplemented.of_quotient_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {p : Submodule 𝕜 E}, IsClosed ↑p → ∀ [hq : FiniteDimensional 𝕜 (E ⧸ p)], p.ClosedComplemented
-- Init.Data.BitVec.Lemmas
BitVec.toInt_zero : ∀ {w : ℕ}, (0#w).toInt = 0
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.refl_apply : ∀ (R : Type u_4) [inst : Mul R] [inst_1 : Add R] (x : R), (RingEquiv.refl R) x = x
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AffineEquiv.pointReflection_midpoint_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), (AffineEquiv.pointReflection R (midpoint R x y)) y = x
-- Mathlib.Analysis.Normed.Group.Basic
norm_of_subsingleton : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] [Subsingleton E] (a : E), ‖a‖ = 0
-- Mathlib.Data.Finset.Defs
Finset.val_injective : ∀ {α : Type u_1}, Function.Injective Finset.val
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- If a weighted sum is zero and one of the weights is `-1`, the corresponding point is
the affine combination of the other points with the given weights.  -/
Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w : ι → k} {p : ι → P},
  (s.weightedVSub p) w = 0 →
    ∀ {i : ι} [inst_3 : DecidablePred fun x => x ≠ i],
      i ∈ s → w i = -1 → (Finset.affineCombination k ({x ∈ s | x ≠ i}) p) w = p i
-- Mathlib.Topology.Closure
closure_empty_iff : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s = ∅ ↔ s = ∅
-- Mathlib.FieldTheory.Normal.Closure
/-- The normal closure of `K/F` in `L/F`.  -/
IntermediateField.normalClosure : (F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] → [inst_2 : Field L] → [Algebra F K] → [inst_4 : Algebra F L] → IntermediateField F L
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- If `f : α →ₛ β` is a simple function and `g : β → α →ₛ γ` is a family of simple functions,
then `f.bind g` binds the first argument of `g` to `f`. In other words, `f.bind g a = g (f a) a`.  -/
MeasureTheory.SimpleFunc.bind : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        MeasureTheory.SimpleFunc α β → (β → MeasureTheory.SimpleFunc α γ) → MeasureTheory.SimpleFunc α γ
-- Init.Data.Bool
Bool.cond_false_left : ∀ (c f : Bool), (bif c then false else f) = (!c && f)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_le_of_ae_lt : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {β : Type u_4} [inst_2 : Preorder β] {f g : α → β}, (∀ᵐ (x : α) ∂μ, f x < g x) → f ≤ᵐ[μ] g
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.concreteCategory : {R : Type u} →
  [inst : CommRing R] → CategoryTheory.ConcreteCategory (BialgCat R) fun x1 x2 => x1.carrier →ₐc[R] x2.carrier
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- For any element j of a field `F`, there exists an elliptic curve over `F`
with j-invariant equal to j (see `WeierstrassCurve.ofJ_j`).
Its coefficients are given explicitly (see `WeierstrassCurve.ofJ0`, `WeierstrassCurve.ofJ1728`
and `WeierstrassCurve.ofJNe0Or1728`).  -/
WeierstrassCurve.ofJ : {F : Type u_2} → [Field F] → F → [DecidableEq F] → WeierstrassCurve F
-- Mathlib.Data.Finsupp.Notation
/-- `fun₀ | i => a` is notation for `Finsupp.single i a`, and with multiple match arms,
`fun₀ ... | i => a` is notation for `Finsupp.update (fun₀ ...) i a`.

As a result, if multiple match arms coincide, the last one takes precedence. 

If the expected type is `Π₀ i, α i` (`DFinsupp`)
  and `Mathlib/Data/DFinsupp/Notation.lean` is imported,
  then this is notation for `DFinsupp.single` and  `Dfinsupp.update` instead. -/
Finsupp.fun₀ : Lean.Parser.Parser
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Turn a constant into an HTML with hover info.
This avoids the `@` that may appear when using `exprToHtml`.  -/
Mathlib.Tactic.ClickSuggestions.constToHtml : Lean.Name → Lean.MetaM ProofWidgets.Html
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
/-- If a commutative square `sq` is a pushout square,
then `sq.pushoutCocone` is a colimit.  -/
CategoryTheory.Square.IsPushout.isColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {sq : CategoryTheory.Square C} → sq.IsPushout → CategoryTheory.Limits.IsColimit sq.pushoutCocone
-- Mathlib.Data.W.Cardinal
/-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
is at most the maximum of the cardinality of `α` and `ℵ₀`  -/
WType.cardinalMk_le_max_aleph0_of_finite : ∀ {α : Type u} {β : α → Type u} [∀ (a : α), Finite (β a)], Cardinal.mk (WType β) ≤ max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_eq_of_ne' : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] {i j : ι}
  (r : G i), i ≠ j → (RestrictedProduct.mulSingle A i r) j = 1
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A natural isomorphism between the functor `map (F ⋙ G) ` and `map F ⋙ map G `.  -/
CategoryTheory.WithInitial.mapComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      {E : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                CategoryTheory.WithInitial.map (F.comp G) ≅
                  (CategoryTheory.WithInitial.map F).comp (CategoryTheory.WithInitial.map G)
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under integer division.  -/
Dioph.div_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v / g v
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuous_unique : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [inst : Unique ι]
  {F : ι → X → α}, Equicontinuous F ↔ Continuous (F default)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₀₁.τ₃ = CategoryTheory.Limits.kernel.ι g
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.forget_obj : ∀ (S : AlgebraicGeometry.Scheme)
  (X :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.id AlgebraicGeometry.Scheme)
      (CategoryTheory.Functor.fromPUnit S) @AlgebraicGeometry.WeaklyEtale ⊤ ⊤),
  (AlgebraicGeometry.Scheme.ProEt.forget S).obj X = X.toComma
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.ncard_primesOver_mul_card_inertia_mul_finrank : ∀ {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] (p : Ideal R)
  [inst_7 : p.IsPrime] (P : Ideal S) [P.LiesOver p] [P.IsPrime] [PerfectField p.ResidueField],
  (p.primesOver S).ncard * Nat.card ↥(Ideal.inertia G P) * P.inertiaDeg R = Nat.card G
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.flatMapAfter.eq_1 : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] (f : β → Std.Iter γ)
  (it₁ : Std.Iter β) (it₂ : Option (Std.Iter γ)),
  Std.Iter.flatMapAfter f it₁ it₂ =
    (Std.IterM.flatMapAfter (fun b => (f b).toIterM) it₁.toIterM (Std.Iter.toIterM <$> it₂)).toIter
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.Hom.line.injEq : ∀ {J : Type w} (a a_1 : J),
  (CategoryTheory.Limits.WalkingParallelFamily.Hom.line a = CategoryTheory.Limits.WalkingParallelFamily.Hom.line a_1) =
    (a = a_1)
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` monovary together (e.g. they are both
monotone/antitone), the product of their sum is less than the size of the set times their scalar
product.  -/
MonovaryOn.sum_mul_sum_le_card_mul_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f g : ι → α}, MonovaryOn f g ↑s → (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑s.card * ∑ i ∈ s, f i * g i
-- Mathlib.Probability.Kernel.Disintegration.Unique
/-- A finite kernel which satisfies the disintegration property is almost everywhere equal to the
disintegration kernel.  -/
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  (κ : ProbabilityTheory.Kernel α Ω) [ProbabilityTheory.IsFiniteKernel κ],
  ρ = ρ.fst.compProd κ → ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] (x : ↥X),
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).Flat
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_zero_iff_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b : α},
      a ∈ s →
        b ∈ s →
          a ≤ b →
            (variationOnFromTo f s a b = 0 ↔
              ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc a b → edist (f x) (f y) = 0)
-- Mathlib.Algebra.Order.Module.Defs
SMulPosStrictMono.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero β] [inst_6 : Zero γ] [SMulPosStrictMono α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → f 0 = 0 → SMulPosStrictMono α β
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.image_ofSimplex : ∀ {X Y : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (f : X ⟶ Y),
  (SSet.Subcomplex.ofSimplex x).image f =
    SSet.Subcomplex.ofSimplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.nondegenerate_transpose_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Finite n], M.transpose.Nondegenerate ↔ M.Nondegenerate
-- Lean.Message
/-- Represents a constant name such that hovering and "go to definition" works.
If there is no such constant in the environment, the name is simply formatted, but sanitized if it is a hygienic name.
Use `MessageData.ofName` if hovers are undesired.

If `fullNames` is true, then pretty prints as if `pp.fullNames` is true.
Otherwise, pretty prints using the current user setting for `pp.fullNames`.
 -/
Lean.MessageData.ofConstName : Lean.Name → optParam Bool false → Lean.MessageData
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_nonneg : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α), 0 ≤ G.edgeDensity s t
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
Cardinal.SharplyLT.isCardinalAccessible_cardinalDirectedPoset : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [inst_1 : Fact κ₂.IsRegular],
  κ₁.SharplyLT κ₂ → CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.funUnique_symm_apply : ∀ (α : Type u_8) (β : Type u_9) [inst : Unique α] [inst_1 : MeasurableSpace β],
  ⇑(MeasurableEquiv.funUnique α β).symm = uniqueElim
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.addSCC.add : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → List α → List α → Lean.SCC.M α Unit
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.ofMessage? : Lean.JsonRpc.Message → Option (Lean.JsonRpc.Response Lean.Json)