mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.mk : Lean.Grind.Config →
  Lean.Meta.Grind.ExtensionStateArray →
    Lean.PArray Lean.Meta.Grind.EMatchTheorem →
      Lean.PArray Lean.Meta.Grind.InjectiveTheorem →
        Lean.PArray Lean.Expr →
          Lean.Meta.Grind.SymbolPriorities →
            Lean.Meta.Simp.Context →
              Array Lean.Meta.Simprocs → Option (Array Lean.Meta.Grind.AnchorRef) → Lean.Meta.Grind.Params
-- Mathlib.CategoryTheory.Monoidal.Preadditive
/-- The isomorphism showing how tensor product on the left distributes over direct sums.  -/
CategoryTheory.leftDistributor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [CategoryTheory.MonoidalPreadditive C] →
          [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            {J : Type} →
              [inst_5 : Finite J] →
                (X : C) →
                  (f : J → C) →
                    CategoryTheory.MonoidalCategoryStruct.tensorObj X (⨁ f) ≅
                      ⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)
-- Mathlib.Analysis.Fourier.PoissonSummation
/-- If `f` is `O(x ^ (-b))` at infinity, then so is the function
`fun x ↦ ‖f.restrict (Icc (x + R) (x + S))‖` for any fixed `R` and `S`.  -/
isBigO_norm_Icc_restrict_atTop : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : C(ℝ, E)} {b : ℝ},
  0 < b →
    (⇑f =O[Filter.atTop] fun x => |x| ^ (-b)) →
      ∀ (R S : ℝ), (fun x => ‖ContinuousMap.restrict (Set.Icc (x + R) (x + S)) f‖) =O[Filter.atTop] fun x => |x| ^ (-b)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_nonpos : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Preorder M] [AddLeftMono M]
  {f : ι → M}, f ≤ 0 → ∑ i, f i ≤ 0
-- Init.Data.Random
instInhabitedStdGen : Inhabited StdGen
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.contains a = false → t.getKeyD a fallback = fallback
-- Mathlib.Algebra.Lie.Ideal
/-- Note that this is not a special case of `LieSubmodule.subsingleton_of_bot`. Indeed, given
`I : LieIdeal R L`, in general the two lattices `LieIdeal R I` and `LieSubmodule R L I` are
different (though the latter does naturally inject into the former).

In other words, in general, ideals of `I`, regarded as a Lie algebra in its own right, are not the
same as ideals of `L` contained in `I`.  -/
LieIdeal.subsingleton_of_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  Subsingleton (LieIdeal R ↥⊥)
-- Mathlib.FieldTheory.KrullTopology
/-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
`Gal(L/K)` induced by the group filter basis `galGroupBasis K L`.  -/
krullTopology : (K : Type u_1) →
  (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → TopologicalSpace Gal(L/K)
-- Mathlib.LinearAlgebra.Matrix.Defs
IsLeftRegular.matrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] {k : α}, IsLeftRegular k → IsSMulRegular (Matrix m n α) k
-- Init.Notation
/-- `if let pat := d then t else e` is a shorthand syntax for:
```
match d with
| pat => t
| _ => e
```
It matches `d` against the pattern `pat` and the bindings are available in `t`.
If the pattern does not match, it returns `e` instead.
 -/
termIfLet : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_alter_eq_add_one : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, k ∉ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size + 1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsScalarTower_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] [inst_4 : Mul M] [inst_5 : ContinuousMul M]
  [IsScalarTower R M M], IsScalarTower R C(α, M) C(α, M)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append.sizeOf_spec : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : SizeOf ι]
  [inst_2 : (a : ι) → SizeOf (M a)] {i j k l : ι} (_w₁ : Monoid.CoprodI.NeWord M i j) (_hne : j ≠ k)
  (_w₂ : Monoid.CoprodI.NeWord M k l),
  sizeOf (_w₁.append _hne _w₂) = 1 + sizeOf i + sizeOf j + sizeOf k + sizeOf l + sizeOf _w₁ + sizeOf _w₂
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.isZariskiLocalAtTarget : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  [P.IsMultiplicative],
  (∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion g],
      P (CategoryTheory.CategoryStruct.comp f g) → P f) →
    AlgebraicGeometry.IsZariskiLocalAtTarget P
-- Std.Sync.Mutex
/-- Wakes up a single other thread executing `wait`.  -/
Std.Condvar.notifyOne : Std.Condvar → BaseIO Unit
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.summable_of_sum_range_le : ∀ {f : ℕ → NNReal} {c : NNReal}, (∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) → Summable f
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.instInhabitedSearchStep.default : {s : String.Slice} → String.Slice.Pattern.SearchStep s
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_one : ∀ {α : Type u_2} {x : NonAssocSemiring α}, ⇑1 = id
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.instHasContDiffBumpOfFiniteDimensionalReal : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E], HasContDiffBump E
-- Mathlib.ModelTheory.Definability
Set.Definable.mono : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {B : Set M} {s : Set (α → M)},
  A.Definable L s → A ⊆ B → B.Definable L s
-- Mathlib.Topology.JacobsonSpace
TopologicalSpace.IsOpenCover.jacobsonSpace_iff : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_1} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover U → (JacobsonSpace X ↔ ∀ (i : ι), JacobsonSpace ↥(U i))
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instUnique : (p : ENNReal) → (V : Type u_4) → [Unique V] → Unique (WithLp p V)
-- Mathlib.Order.Filter.Bases.Basic
Filter.comap_hasBasis : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter β),
  (Filter.comap f l).HasBasis (fun s => s ∈ l) fun s => f ⁻¹' s
-- Mathlib.FieldTheory.Finite.Trace
/-- An explicit formula for the trace map: `trace[L/K](x) = ∑ i < [L:K], x ^ ((#K) ^ i)`.  -/
FiniteField.algebraMap_trace_eq_sum_pow : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [Finite L] [inst_3 : Algebra K L] (x : L),
  (algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i
-- Mathlib.Logic.Basic
exists_apply_eq_apply2 : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {f : α → β → γ} {a : α} {b : β}, ∃ x y, f x y = f a b
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.toIsTopologicalGroup : ∀ {α : Type u} [inst : Group α] (self : GroupTopology α), IsTopologicalGroup α
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.natAbs_valMinAbs_le : ∀ {n : ℕ} [NeZero n] (x : ZMod n), x.valMinAbs.natAbs ≤ n / 2
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasStrictDerivAt.neg` -/
HasStrictDerivAt.fun_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun i => -f i) (-f') x
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalsEquivMonoOverTerminal_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C],
  (CategoryTheory.subterminalsEquivMonoOverTerminal C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.MonoOver.isoMk
          (CategoryTheory.Iso.refl
            (({ obj := fun X => { obj := X.obj.left, property := ⋯ },
                          map := fun {X Y} f => CategoryTheory.ObjectProperty.homMk f.hom.left, map_id := ⋯,
                          map_comp := ⋯ }.comp
                      {
                        obj := fun X =>
                          { obj := CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj), property := ⋯ },
                        map := fun {X Y} f => CategoryTheory.MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                  X).obj.left)
          ⋯)
      ⋯
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (p : ι → Prop) [inst_1 : DecidablePred p]
  (f : Π₀ (i : ι), β i), DFinsupp.filter p (-f) = -DFinsupp.filter p f
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
/-- Monoidal structure on `F`, given that `F` lifts along `L` to a monoidal functor `G`,
where `L` is a monoidal localization functor.
 -/
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [inst_4 : CategoryTheory.MonoidalCategory D] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (L : CategoryTheory.Functor C D) →
                    (W : CategoryTheory.MorphismProperty C) →
                      [L.IsLocalization W] →
                        [L.Monoidal] →
                          (F : CategoryTheory.Functor D E) →
                            (G : CategoryTheory.Functor C E) →
                              [G.Monoidal] →
                                [W.ContainsIdentities] → [CategoryTheory.Localization.Lifting L W G F] → F.Monoidal
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_presieve₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)}, E.IsStronglySheafFor F → CategoryTheory.Presieve.IsSheafFor F E.presieve₀
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The image of `𝓞 K` as a subring of `ℂ^n`.  -/
NumberField.canonicalEmbedding.integerLattice : (K : Type u_1) → [inst : Field K] → Subring ((K →+* ℂ) → ℂ)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_mapHomologicalComplexObjIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] {Z : HomologicalComplex D c}
  (h : HomologicalComplex.homotopyCofiber ((H.mapHomologicalComplex c).map φ) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.homotopyCofiber.inr φ))
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjIso φ H).hom h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr ((H.mapHomologicalComplex c).map φ)) h
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_def : ∀ (n : ℕ) {p : ℕ}, Nat.Prime p → n.factorization p = padicValNat p n
-- Init.SizeOf
Lean.Syntax.ident.sizeOf_spec : ∀ (info : Lean.SourceInfo) (rawVal : Substring.Raw) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved),
  sizeOf (Lean.Syntax.ident info rawVal val preresolved) =
    1 + sizeOf info + sizeOf rawVal + sizeOf val + sizeOf preresolved
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_toAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toAffineEquiv = ⇑e
-- Lean.AuxRecursor
Lean.NoConfusionInfo.regular : ℕ → ℕ → ℕ → Lean.NoConfusionInfo
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- Compose an `EvenHom` with an `AlgHom` on the output.  -/
CliffordAlgebra.EvenHom.compr₂ : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} →
            {A : Type u_3} →
              {B : Type u_4} →
                [inst_3 : Ring A] →
                  [inst_4 : Ring B] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] → CliffordAlgebra.EvenHom Q A → (A →ₐ[R] B) → CliffordAlgebra.EvenHom Q B
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.isStrictOrder : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [inst_2 : PartialOrder N],
  IsStrictOrder (Lex (α →₀ N)) fun x1 x2 => x1 < x2
-- Mathlib.Order.Heyting.Basic
/-- `(· \ a)` is left adjoint to `(· ⊔ a)`  -/
BiheytingAlgebra.sdiff_le_iff : ∀ {α : Type u_4} [self : BiheytingAlgebra α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a.fmod b = a
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux.fun_cases_unfolding : ∀ (i : ℤ) (hi : i ≠ 0) (acc : ℕ) (motive : (k : ℕ) → i.natAbs ≤ k → ℕ → Prop),
  (∀ (k : ℕ),
      k + 1 ≠ 0 →
        ∀ (hk : i.natAbs ≤ k + 1) (h : i % 2 = 0),
          i.natAbs ≤ k.succ → motive k.succ hk (Int.trailingZeros.aux k (i / 2) ⋯ ⋯ (acc + 1))) →
    (∀ (k : ℕ), k + 1 ≠ 0 → ∀ (hk : i.natAbs ≤ k + 1), ¬i % 2 = 0 → i.natAbs ≤ k.succ → motive k.succ hk acc) →
      ∀ (k : ℕ) (hk : i.natAbs ≤ k), motive k hk (Int.trailingZeros.aux k i hi hk acc)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Satisfying the inhabited linter.  -/
TopCat.inhabitedPrelocalPredicate : (X : TopCat) → (T : Type u_3) → [TopologicalSpace T] → Inhabited (TopCat.PrelocalPredicate fun x => T)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.is_local_nhds : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P → ∀ {s u : Set H} {x : H} {f : H → H'}, u ∈ nhdsWithin x s → (P f s x ↔ P f (s ∩ u) x)
-- Batteries.Data.BitVec.Lemmas
_private.Batteries.Data.BitVec.Lemmas.0.Fin.succ.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin n → Sort u_1) (i : ℕ) (h : i < n) (h_1 : (i : ℕ) → (h : i < n) → motive ⟨i, h⟩),
  (match ⟨i, h⟩ with
    | ⟨i, h⟩ => h_1 i h) =
    h_1 i h
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun.eq_1 : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat),
  X.toΓSpecFun x =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))
-- Init.Data.List.Nat.TakeDrop
List.drop_replicate : ∀ {α : Type u_1} {a : α} {i n : ℕ}, List.drop i (List.replicate n a) = List.replicate (n - i) a
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.coneEquiv_functor_obj_π_app_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {t : CategoryTheory.Limits.Cone K} (Y : J),
  (CategoryTheory.WithTerminal.coneEquiv.functor.obj t).π.app (CategoryTheory.WithTerminal.of Y) =
    CategoryTheory.Over.Hom.left (t.π.app Y)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.mk : (carrier : Type u) → [str : AddCommMonoid carrier] → AddCommMonCat