mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.YClass_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [Nontrivial R] (y : Polynomial R),
  WeierstrassCurve.Affine.CoordinateRing.YClass W' y ≠ 0
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**, algebra form: an Artinian simple algebra is isomorphic
to a matrix algebra over a division algebra.  -/
IsSimpleRing.exists_algEquiv_matrix_divisionRing : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSimpleRing R]
  [IsArtinianRing R], ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
-- Init.Data.Option.Lemmas
Option.map_max : ∀ {α : Type u_1} {β : Type u_2} [inst : Max α] [inst_1 : Max β] {o o' : Option α} {f : α → β},
  (∀ (x y : α), f (x ⊔ y) = f x ⊔ f y) → Option.map f (o ⊔ o') = Option.map f o ⊔ Option.map f o'
-- Init.Data.List.Basic
/-- Removes the first element of a list for which `p` returns `true`. If no element satisfies `p`, then
the list is returned unchanged.

Examples:
  * `[2, 1, 2, 1, 3, 4].eraseP (· < 2) = [2, 2, 1, 3, 4]`
  * `[2, 1, 2, 1, 3, 4].eraseP (· > 2) = [2, 1, 2, 1, 4]`
  * `[2, 1, 2, 1, 3, 4].eraseP (· > 8) = [2, 1, 2, 1, 3, 4]`
 -/
List.eraseP : {α : Type u} → (α → Bool) → List α → List α
-- Lean.Meta.Sym.Canon
/-- `withCaching` + `canonInstDec'`  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInstDec : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.isEmpty : Lean.Meta.MVarRenaming → Bool
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A finite union of countably compact sets is countably compact.  -/
Set.Finite.isCountablyCompact_biUnion : ∀ {ι : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] {s : Set ι} {f : ι → Set E},
  s.Finite → (∀ i ∈ s, IsCountablyCompact (f i)) → IsCountablyCompact (⋃ i ∈ s, f i)
-- Mathlib.ModelTheory.Semantics
/-- A special case of `realize_restrictFreeVar`, included because we can add the `simp` attribute
to it  -/
FirstOrder.Language.BoundedFormula.realize_restrictFreeVar' : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [inst_1 : DecidableEq α] {n : ℕ}
  {φ : L.BoundedFormula α n} {s : Set α} (h : ↑φ.freeVarFinset ⊆ s) {v : α → M} {xs : Fin n → M},
  (φ.restrictFreeVar (Set.inclusion h)).Realize (v ∘ Subtype.val) xs ↔ φ.Realize v xs
-- Mathlib.Algebra.GradedMonoid
/-- `GMul` implies `Mul (GradedMonoid A)`.  -/
GradedMonoid.GMul.toMul : {ι : Type u_1} → (A : ι → Type u_2) → [inst : Add ι] → [GradedMonoid.GMul A] → Mul (GradedMonoid A)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (x : α), ↑{x} = {x}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.darts_takeUntil_prefix_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).darts <+: p.darts
-- Mathlib.Data.List.Sigma
List.mem_keys : ∀ {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)}, a ∈ l.keys ↔ ∃ b, ⟨a, b⟩ ∈ l
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
QuotientGroup.borelSpace : ∀ {G : Type u_3} [inst : TopologicalSpace G] [PolishSpace G] [inst_2 : Group G] [IsTopologicalGroup G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [N.Normal] [IsClosed ↑N], BorelSpace (G ⧸ N)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.indep_insert_sdiff_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep I → f ∈ M.closure I → e ∈ M.closure (insert f I \ {e}) → e ∈ insert f I → M.Indep (insert f I \ {e})
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_insertMany_list : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => (a == b) = false) l →
        (∀ a ∈ m, l.contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.RingTheory.HopfAlgebra.Convolution
HopfAlgebra.antipode_mul_antidistrib : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a b : A),
  (HopfAlgebraStruct.antipode R) (a * b) = (HopfAlgebraStruct.antipode R) b * (HopfAlgebraStruct.antipode R) a
-- Init.Core
Prod.map_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ),
  (Prod.map f g x).2 = g x.2
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toNonUnitalStarAlgHom_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) (a : A₁), e.toNonUnitalStarAlgHom a = e a
-- Mathlib.Data.Num.Basic
ZNum.instMod : Mod ZNum
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.eval.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (l : { l // Profinite.NobelingProof.Products.isGood C l }),
  Profinite.NobelingProof.GoodProducts.eval C l = Profinite.NobelingProof.Products.eval C ↑l
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.exists_small_elementarySubstructure : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M], ∃ S, Small.{max u v, w} ↥S
-- Mathlib.Data.Set.Basic
Set.Nonempty.not_subset_empty : ∀ {α : Type u} {s : Set α}, s.Nonempty → ¬s ⊆ ∅
-- Mathlib.LinearAlgebra.SesquilinearForm.Star
apply_eq_star_dotProduct_toMatrix₂_mulVec : ∀ {R : Type u_1} {M : Type u_2} {n : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Fintype n] [inst_5 : DecidableEq n] {B : M →ₗ⋆[R] M →ₗ[R] R} (b : Module.Basis n R M)
  (x y : M), (B x) y = star ⇑(b.repr x) ⬝ᵥ ((LinearMap.toMatrix₂ b b) B).mulVec ⇑(b.repr y)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightHom_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (g : P.Aut),
  (RootPairing.Equiv.coweightHom P) g = MulOpposite.op (RootPairing.Equiv.coweightEquiv P P g)
-- Init.Data.Vector.Find
Vector.findSome?_push : ∀ {α : Type u_1} {n : ℕ} {a : α} {α_1 : Type u_2} {f : α → Option α_1} {xs : Vector α n},
  Vector.findSome? f (xs.push a) = (Vector.findSome? f xs).or (f a)
-- Mathlib.Algebra.Order.Star.Basic
/-- An ordered \*-ring is a \*-ring with a partial order such that the nonnegative elements
constitute precisely the `AddSubmonoid` generated by elements of the form `star s * s`.

If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, it may be more
convenient to declare instances using `StarOrderedRing.of_nonneg_iff`.  -/
StarOrderedRing : (R : Type u_3) → [inst : NonUnitalSemiring R] → [PartialOrder R] → [StarRing R] → Prop
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instFinitenessRelation : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α m β] →
          [Std.Iterators.Finite α m] →
            {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
              Std.Iterators.FinitenessRelation (Std.Iterators.Types.DropWhile α m β P) m
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty Cᵒᵖ),
  (P ⊔ Q).unop = P.unop ⊔ Q.unop
-- Mathlib.Order.CompleteLattice.Finset
/-- Intersection of an indexed family of sets `s : ι → Set α` is equal to the intersection of the
intersections of finite subfamilies. This version works for `ι : Sort*`. See also
`iInter_eq_iInter_finset` for a version that assumes `ι : Type*` but avoids `PLift`s in the
right-hand side.  -/
Set.iInter_eq_iInter_finset' : ∀ {α : Type u_2} {ι' : Sort u_7} (s : ι' → Set α), ⋂ i, s i = ⋂ t, ⋂ i ∈ t, s i.down
-- Lean.Meta.ArgsPacker.Basic
Lean.Meta.ArgsPacker.mk.inj : ∀ {varNamess varNamess_1 : Array (Array Lean.Name)},
  { varNamess := varNamess } = { varNamess := varNamess_1 } → varNamess = varNamess_1
-- Mathlib.Topology.Inseparable
Specializes.map_of_continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  x ⤳ y → ContinuousAt f y → f x ⤳ f y
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.boundedFilterSubmodule.congr_simp : ∀ (𝕜 : Type u_1) {α : Type u_2} {β : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedAddCommGroup β]
  [inst_2 : Module 𝕜 β] [inst_3 : IsBoundedSMul 𝕜 β] (l l_1 : Filter α),
  l = l_1 → Filter.boundedFilterSubmodule 𝕜 l = Filter.boundedFilterSubmodule 𝕜 l_1
-- Mathlib.Algebra.Ring.Prod
/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`.  -/
RingEquiv.prodProdProdComm : (R : Type u_1) →
  (R' : Type u_2) →
    (S : Type u_3) →
      (S' : Type u_4) →
        [inst : NonAssocSemiring R] →
          [inst_1 : NonAssocSemiring S] →
            [inst_2 : NonAssocSemiring R'] → [inst_3 : NonAssocSemiring S'] → (R × R') × S × S' ≃+* (R × S) × R' × S'
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated subgroups is finitely generated.  -/
Subgroup.FG.prod : ∀ {G : Type u_3} [inst : Group G] {G' : Type u_5} [inst_1 : Group G'] {P : Subgroup G} {Q : Subgroup G'},
  P.FG → Q.FG → (P.prod Q).FG
-- Mathlib.Algebra.Order.Star.Basic
star_left_conjugate_lt_conjugate : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a b : R}, a < b → ∀ {c : R}, IsRegular c → star c * a * c < star c * b * c
-- Std.Sat.AIG.CachedGates
/-- Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
 -/
Std.Sat.AIG.mkBEqCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mapOrderEmbedding_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f)
  (N : LieSubmodule R L M), (LieSubmodule.mapOrderEmbedding hf) N = LieSubmodule.map f N
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A wrapper for promoting any type to a category,
with the only morphisms being equalities.
 -/
CategoryTheory.Discrete : Type u₁ → Type u₁
-- Mathlib.Order.Filter.CountableInter
/-- Construct a filter with countable intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the countable intersection property.  -/
Filter.ofCountableInter : {α : Type u_2} →
  (l : Set (Set α)) →
    (∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l) → (∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) → Filter α
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
WithLp.measurable_toLp : ∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X], Measurable (WithLp.toLp p)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.mul.sizeOf_spec : ∀ {R : Type u} [inst : SizeOf R] (a b : Rack.PreEnvelGroup R), sizeOf (a.mul b) = 1 + sizeOf a + sizeOf b
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
the number is too large.

Returns `2^8 - 1` for natural numbers greater than or equal to `2^8`.
 -/
UInt8.ofNatClamp : ℕ → UInt8
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.ofDigits.match_1.splitter : (motive : List ℕ → Sort u_1) → (x : List ℕ) → (Unit → motive []) → ((h : ℕ) → (t : List ℕ) → motive (h :: t)) → motive x
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is strictly monotone on a left neighborhood of
`a` and the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`,
then `f` is continuous at `a` from the left.  -/
StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  StrictMonoOn f s →
    s ∈ nhdsWithin a (Set.Iic a) →
      closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.LinearAlgebra.Determinant
/-- To show `P (LinearMap.det f)` it suffices to consider `P (Matrix.det (toMatrix _ _ f))` and
`P 1`.  -/
LinearMap.det_cases : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M]
  [inst_3 : DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M),
  (∀ (s : Finset M) (b : Module.Basis (↥s) A M), P ((LinearMap.toMatrix b b) f).det) → P 1 → P (LinearMap.det f)
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.ofSubring.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (T : Subring R) (p : Polynomial ↥T),
  Polynomial.ofSubring T p = ∑ i ∈ p.support, (Polynomial.monomial i) ↑(p.coeff i)
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : CategoryTheory.ShortComplex.QuasiIso φ]
  [hφ' : CategoryTheory.ShortComplex.QuasiIso φ'],
  CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `F` is of exponential characteristic `q`, then `F⟮x⟯ / F` is a purely inseparable extension
if and only if `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`.  -/
IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
  {x : E}, IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The forget functor `MonoOver X ⥤ Over X` is fully faithful.  -/
CategoryTheory.MonoOver.fullyFaithfulForget : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (X : C) → (CategoryTheory.MonoOver.forget X).FullyFaithful
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
/-- Projection from `s : Set α` to `α` sending each order connected component of `s` to a single
point of this component.  -/
Set.ordConnectedProj : {α : Type u_1} → [LinearOrder α] → (s : Set α) → ↑s → α
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.mk.sizeOf_spec : ∀ (bottomUps higherOrders funBinders provideds : Array Bool) (namedArgs : Array Lean.Name),
  sizeOf
      { bottomUps := bottomUps, higherOrders := higherOrders, funBinders := funBinders, provideds := provideds,
        namedArgs := namedArgs } =
    1 + sizeOf bottomUps + sizeOf higherOrders + sizeOf funBinders + sizeOf provideds + sizeOf namedArgs
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = true ↔ ∀ (a : α), m.contains a = false)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.instIsSplitEpiR : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y),
  CategoryTheory.IsSplitEpi h.r
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (t.alter k f).contains k' = t.contains k'
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.mk : {C : Type u₁} → (ι : Type) → [fintype : Fintype ι] → (ι → C) → CategoryTheory.Mat_ C
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The `C : R → R[X]` case of **Chevalley's theorem** with complexity bound.  -/
ChevalleyThm.chevalley_polynomialC : ∀ {R : Type u_6} [inst : CommRing R] (M : Submodule ℤ R),
  1 ∈ M →
    ∀ (S : PrimeSpectrum.ConstructibleSetData (Polynomial R)),
      (∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M) →
        ∃ T,
          PrimeSpectrum.comap Polynomial.C '' S.toSet = T.toSet ∧
            ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_liminf_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} [Countable ι] [inst : Preorder ι]
  (f : ι → α → ENNReal),
  essSup (fun x => Filter.liminf (fun n => f n x) Filter.atTop) μ ≤
    Filter.liminf (fun n => essSup (fun x => f n x) μ) Filter.atTop