mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Bitwise
USize.and_zero : ∀ {a : USize}, a &&& 0 = 0
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An injective presentation of an object `X` consists of a monomorphism `f : X ⟶ J`
to some injective object `J`.
 -/
CategoryTheory.InjectivePresentation.mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.InjectivePresentation X),
  CategoryTheory.Mono self.f
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.IsClique.card_le_chromaticNumber : ∀ {V : Type u} {G : SimpleGraph V} {s : Finset V}, G.IsClique ↑s → ↑s.card ≤ G.chromaticNumber
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.toList_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rightInverse_ofMultiset_roots : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R],
  Function.RightInverse (⇑Polynomial.ofMultiset) Polynomial.roots
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Eventually.expGrowthSup_le : ∀ {u : ℕ → ENNReal} {a : EReal}, (∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp) → ExpGrowth.expGrowthSup u ≤ a
-- Lean.Environment
/-- Private module data.  -/
Lean.OLeanLevel.private : Lean.OLeanLevel
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom_ne_zero : ∀ (n : ℕ), n.centralBinom ≠ 0
-- Mathlib.Topology.Sheaves.Presheaf
/-- The category of `C`-valued presheaves on a (bundled) topological space `X`.  -/
TopCat.Presheaf : (C : Type u) → [CategoryTheory.Category.{v, u} C] → TopCat → Type (max u v w)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
exists_pos_add_of_lt : ∀ {α : Type u} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] {a b : α},
  a < b → ∃ c, ∃ (_ : 0 < c), a + c = b
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_single_of_forall_mul_ne : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m m' : M} [inst_1 : Mul M] (r : R) (x : MonoidAlgebra R M),
  (∀ (d : M), d * m ≠ m') → (x * MonoidAlgebra.single m r).coeff m' = 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.inc : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Bool →
        Bool →
          Lean.Compiler.LCNF.Code pu →
            autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_15 →
              Lean.Compiler.LCNF.Code pu
-- Mathlib.CategoryTheory.Limits.Cones
/-- Precomposing a cocone by the composite natural transformation `α ≫ β` is the same as
precomposing by `β` and then by `α`.  -/
CategoryTheory.Limits.Cocone.precomposeComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G H : CategoryTheory.Functor J C} →
          (β : H ⟶ G) →
            (α : G ⟶ F) →
              CategoryTheory.Limits.Cocone.precompose (CategoryTheory.CategoryStruct.comp β α) ≅
                (CategoryTheory.Limits.Cocone.precompose α).comp (CategoryTheory.Limits.Cocone.precompose β)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.map_apply_ιMulti : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] N) (m : Fin n → M),
  (ExteriorAlgebra.map f) ((ExteriorAlgebra.ιMulti R n) m) = (ExteriorAlgebra.ιMulti R n) (⇑f ∘ m)
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A preadditive category has a kernel for `f - g` if it has an equalizer for `f` and `g`.  -/
CategoryTheory.Preadditive.hasKernel_of_hasEqualizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y)
  [CategoryTheory.Limits.HasEqualizer f g], CategoryTheory.Limits.HasKernel (f - g)
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.factorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesIso₀_hom_comp_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).hom (groupCohomology.shortComplexH0 A).f =
    CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0) (groupCohomology.cochainsIso₀ A).hom
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.le_of_count_ne_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {m p : Associates α},
  m ≠ 0 → Irreducible p → p.count m.factors ≠ 0 → p ≤ m
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_mul_left : ∀ {α : Type u_2} [inst : MulOneClass α] (s : Set α) {t : Set α}, 1 ∈ t → s ⊆ s * t
-- Mathlib.Topology.Connected.PathConnected
PathConnectedSpace.exists_path_through_family' : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PathConnectedSpace X] {n : ℕ} (p : Fin (n + 1) → X),
  ∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, (t₁ \ t₂).getKey! k = if k ∈ t₂ then default else t₁.getKey! k
-- Mathlib.Algebra.Quaternion
Quaternion.instDistribMulAction : {S : Type u_1} →
  {R : Type u_3} →
    [inst : CommRing R] → [inst_1 : Semiring S] → [DistribMulAction S R] → DistribMulAction S (Quaternion R)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Bornology α] [inst_1 : Bornology β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toFun : α → β) (comap_cobounded_le' : Filter.comap toFun (Bornology.cobounded β) ≤ Bornology.cobounded α),
  sizeOf { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' } = 1
-- Std.Data.HashSet.Basic
Std.HashSet.instInter : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Inter (Std.HashSet α)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- `minpoly.algEquiv` sends the generator of `K⟮x⟯` to the generator of `K⟮y⟯`.  -/
minpoly.algEquiv_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L}
  (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y),
  (minpoly.algEquiv hx h_mp) (IntermediateField.AdjoinSimple.gen K x) = IntermediateField.AdjoinSimple.gen K y
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_3),
  (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f = X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[1] ⟶ Λ[2, 0]` which avoids `2`.  -/
SSet.horn₂₀.ι₀₁ : SSet.stdSimplex.obj { len := 1 } ⟶ (SSet.horn 2 0).toSSet
-- Std.Data.DHashMap.RawDef
/-- Folds the given function over the mappings in the hash map in some order.  -/
Std.DHashMap.Raw.fold : {α : Type u} → {β : α → Type v} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → Std.DHashMap.Raw α β → δ
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.termFrontFace_ : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An `n`-preprimitive action is `m`-preprimitive for `m ≤ n`.  -/
MulAction.isMultiplyPreprimitive_of_le : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {n : ℕ},
  MulAction.IsMultiplyPreprimitive M α n → ∀ {m : ℕ}, m ≤ n → ↑n ≤ ENat.card α → MulAction.IsMultiplyPreprimitive M α m
-- Mathlib.FieldTheory.KummerExtension
autEquivZmod_symm_apply_natCast : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1)
  [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L},
  α ^ n = (algebraMap K L) a →
    ∀ [inst_4 : NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℕ),
      ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
-- Mathlib.Probability.Kernel.WithDensity
/-- If a kernel `κ` is finite and a function `f : α → β → ℝ≥0∞` is bounded, then `withDensity κ f`
is finite.  -/
ProbabilityTheory.Kernel.isFiniteKernel_withDensity_of_bounded : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsFiniteKernel κ] {B : ENNReal},
  B ≠ ⊤ → (∀ (a : α) (b : β), f a b ≤ B) → ProbabilityTheory.IsFiniteKernel (κ.withDensity f)
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionData.mk : Lean.Name → Lean.Expr → List ℕ → Bool → Bool → Simps.ProjectionData
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_union_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.leftIso_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y),
  (CategoryTheory.Comma.leftIso α).hom = α.hom.left
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.Over.sections_obj : ∀ {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)] (X : CategoryTheory.Over I),
  (CategoryTheory.Over.sections I).obj X =
    CategoryTheory.ChosenPullbacksAlong.pullbackObj ((CategoryTheory.ihom I).map X.hom)
      (CategoryTheory.curryRightUnitorHom I)
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.lt_iff : ∀ {X : Type u_1} [inst : PartialOrder X] (A B : PartialOrder.NonemptyFiniteChains X), A < B ↔ A.finset ⊂ B.finset
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.addSubMap.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R),
  W.addSubMap =
    ![MvPolynomial.X 0 ^ 2 - MvPolynomial.C W.b₄ * MvPolynomial.X 0 * MvPolynomial.X 2 -
          MvPolynomial.C W.b₆ * MvPolynomial.X 1 * MvPolynomial.X 2 -
        MvPolynomial.C W.b₈ * MvPolynomial.X 2 ^ 2,
      MvPolynomial.C 2 * MvPolynomial.X 1 * MvPolynomial.X 0 +
            MvPolynomial.C W.b₂ * MvPolynomial.X 0 * MvPolynomial.X 2 +
          MvPolynomial.C W.b₄ * MvPolynomial.X 1 * MvPolynomial.X 2 +
        MvPolynomial.C W.b₆ * MvPolynomial.X 2 ^ 2,
      MvPolynomial.X 1 ^ 2 - MvPolynomial.C 4 * MvPolynomial.X 0 * MvPolynomial.X 2]
-- Init.Data.Nat.Lemmas
Nat.eq_zero_of_le_div_two : ∀ {n : ℕ}, n ≤ n / 2 → n = 0
-- Mathlib.Topology.Neighborhoods
OrderTop.tendsto_atTop_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} [inst_1 : PartialOrder α] [inst_2 : OrderTop α] (f : α → X),
  Filter.Tendsto f Filter.atTop (nhds (f ⊤))
-- Mathlib.Order.Fin.Basic
Fin.castOrderIso_apply : ∀ {m n : ℕ} (eq : n = m) (i : Fin n), (Fin.castOrderIso eq) i = Fin.cast eq i
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCompIso_inv_app_hom₃ : ∀ {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.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift ℤ] (G : CategoryTheory.Functor D E) [inst_7 : G.CommShift ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCompIso G).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.obj₃))
-- Mathlib.NumberTheory.ZetaValues
summable_bernoulli_fourier : ∀ {k : ℕ}, 2 ≤ k → Summable fun n => -↑k.factorial / (2 * ↑Real.pi * Complex.I * ↑n) ^ k
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.map.eq_1 : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G)
  (e : G ≃* H), b.map e = { repr := e.symm.trans b.repr }
-- Mathlib.Data.Finmap
Multiset.keys_cons : ∀ {α : Type u} {β : α → Type v} {a : α} {b : β a} {s : Multiset (Sigma β)}, (⟨a, b⟩ ::ₘ s).keys = a ::ₘ s.keys
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The linear isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    TensorProduct (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
                        (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.Cotangent ≃ₗ[S]
                      P.toExtension.Cotangent
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedGoal.default : Lean.Meta.Grind.Goal
-- Batteries.Data.String.Lemmas
String.utf8ByteSize_ofList : ∀ (cs : List Char), (String.ofList cs).utf8ByteSize = String.utf8Len cs
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as a filter
basis, for any basis `𝓑` of `𝓤 β`.  -/
UniformFun.hasBasis_nhds_of_basis : ∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (f : UniformFun α β) {p : ι → Prop}
  {s : ι → Set (β × β)},
  (uniformity β).HasBasis p s → (nhds f).HasBasis p fun i => {g | (f, g) ∈ UniformFun.gen α β (s i)}
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.isOpen_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {a : A}, IsOpen ↑(ProjectiveSpectrum.basicOpen 𝒜 a)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimIsoFlipCompWhiskerColim_inv_app_app : ∀ {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] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (X : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X_1 : K),
  (CategoryTheory.Limits.colimIsoFlipCompWhiskerColim.inv.app X).app X_1 =
    (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation X X_1).inv
-- Mathlib.Order.Filter.Ultrafilter.Basic
/-- **Alias** of `Filter.notMem_hyperfilter_of_finite`. -/
Set.Finite.notMem_hyperfilter : ∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → s ∉ Filter.hyperfilter α
-- Lean.CoreM
Lean.MonadDeclNameGenerator.setDeclNGen : {m : Type → Type} → [self : Lean.MonadDeclNameGenerator m] → Lean.DeclNameGenerator → m Unit
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_add_left_deg : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n k : ℕ),
  f.natDegree ≤ m → f.resultant g (m + k) n = (-1) ^ (n * k) * g.coeff n ^ k * f.resultant g m n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_add_inter : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [inst_2 : DecidableEq α] (a : α) (s t : Finset α),
  {a} + s ∩ t = ({a} + s) ∩ ({a} + t)
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a `CommMonoid` under pointwise operations if `α` is.  -/
Filter.commMonoid : {α : Type u_2} → [CommMonoid α] → CommMonoid (Filter α)
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_Ioo_nat : ∀ (a b : ℕ), (Set.Ioo a b).ncard = b - a - 1
-- Lean.Elab.AssertExists
/-- `assert_not_exists d₁ d₂ ... dₙ` is a command that asserts that the declarations named
`d₁ d₂ ... dₙ` *do not exist* in the current import scope.

Be careful to use names (e.g. `Rat`) rather than notations (e.g. `ℚ`).

It may be used (sparingly!) to enforce plans that certain files are independent of each other.

If you encounter an error on an `assert_not_exists` command while developing a library,
it is probably because you have introduced new import dependencies to a file.
In this case, you should refactor your work
(for example by creating new files rather than adding imports to existing files).
You should *not* delete the `assert_not_exists` statement without careful discussion ahead of time.

`assert_not_exists` statements should generally live at the top of the file, after the module doc.
 -/
Lean.Elab.Command.elabAssertNotExists : Lean.Elab.Command.CommandElab
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.ext_iff : ∀ {α : Type u_4} {x y : Hypergraph α}, x = y ↔ x.vertexSet = y.vertexSet ∧ x.edgeSet = y.edgeSet
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.instInhabitedNonUnitalStarSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [IsScalarTower R A A] → [SMulCommClass R A A] → [StarModule R A] → Inhabited (NonUnitalStarSubalgebra R A)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The cone associated to the pullback of `f` and `g`  -/
CategoryTheory.Limits.pullback.cone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) → (g : Y ⟶ Z) → [CategoryTheory.Limits.HasPullback f g] → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.Data.FunLike.Equiv
EquivLike.injective : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E), Function.Injective ⇑e
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) {S : Type u_7}
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] [IsDomain R]
  [Module.IsTorsionFree R M] [NeZero 2] {i j : ι}, P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toZeroLEOneClass : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsStrictOrderedRing R], ZeroLEOneClass R
-- Mathlib.Data.Set.Restrict
Set.domRestrict_eq_domRestrict_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, s.domRestrict f₁ = s.domRestrict f₂ ↔ Set.EqOn f₁ f₂ s
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.sum_add_distrib' : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), (Cardinal.sum fun i => f i + g i) = Cardinal.sum f + Cardinal.sum g
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.mul_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x x' y : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F x x' → RingCat.Colimits.Relation F (x.mul y) (x'.mul y)
-- Std.Time.DateTime.Timestamp
/-- Represents an exact point in time as a UNIX Epoch timestamp.
 -/
Std.Time.Timestamp : Type
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mulMon_nc_go_NonnegCoeffs : ∀ {p : Lean.Grind.CommRing.Poly} {k : ℤ} (m : Lean.Grind.CommRing.Mon) {acc : Lean.Grind.CommRing.Poly},
  k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs → (Lean.Grind.CommRing.Poly.mulMon_nc.go k m p acc).NonnegCoeffs
-- Init.Data.Dyadic.Basic
Dyadic.toRat_mul : ∀ (x y : Dyadic), (x * y).toRat = x.toRat * y.toRat
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α],
  (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).counitIso.hom = CategoryTheory.eqToHom ⋯
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul_toFun : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ' V β) (ab : α × β),
  (s.smul t) ab = (HahnModule.of R).symm (s ab.1 • (HahnModule.of R) (t ab.2))
-- Mathlib.Algebra.Group.Shrink
Shrink.instMulOneClass : {α : Type u_2} → [inst : Small.{v, u_2} α] → [MulOneClass α] → MulOneClass (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y`
(as an instance).  -/
CategoryTheory.Limits.IsInitial.ofUnique : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) → [h : (Y : C) → Unique (X ⟶ Y)] → CategoryTheory.Limits.IsInitial X
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- The spectrum of a selfadjoint is real  -/
IsSelfAdjoint.val_re_map_spectrum : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A},
  IsSelfAdjoint a → spectrum ℂ a = Complex.ofReal ∘ Complex.re '' spectrum ℂ a
-- Mathlib.Algebra.Group.Nat.Hom
AddMonoidHom.ext_nat_iff : ∀ {A : Type u_2} [inst : AddZeroClass A] {f g : ℕ →+ A}, f = g ↔ f 1 = g 1
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.sub : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMinOn f s a → IsLocalMaxOn g s a → IsLocalMinOn (fun x => f x - g x) s a
-- Std.Do.SPred.SVal
/-- A value indexed by a curried tuple of states.

Example:
```
example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl
```
 -/
Std.Do.SVal : List (Type u) → Type u → Type u
-- Batteries.Data.MLList.Basic
/-- Given a lazy list in a state monad, run it on some initial state, recording the states.  -/
MLList.runState : {m : Type u → Type u} → {σ α : Type u} → [Monad m] → MLList (StateT σ m) α → σ → MLList m (α × σ)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (a : PrimeSpectrum S),
  ↑(↑((IsLocalization.AtPrime.primeSpectrumOrderIso S I) a)).asIdeal = ⇑(algebraMap R S) ⁻¹' ↑a.asIdeal
-- Lean.SubExpr
/-- The subexpression.  -/
Lean.SubExpr.expr : Lean.SubExpr → Lean.Expr