mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instMonoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.Grp C)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β k} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Lean.Data.Name
Lean.Name.getNumParts : Lean.Name → ℕ
-- Mathlib.Topology.VectorBundle.Basic
/-- The zero section of a vector bundle is continuous.  -/
Bundle.Trivialization.continuous_zeroSection : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E] [VectorBundle R F E],
  Continuous (Bundle.zeroSection F E)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  Disjoint t (⋃₀ ↑(hC.disjointOfDiff hs ht))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α}, (cmp k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFractionRel.refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (z : W.RightFraction X Y), CategoryTheory.MorphismProperty.RightFractionRel z z
-- Mathlib.GroupTheory.Coset.Basic
eq_cosets_of_normal : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), s.Normal → ∀ (g : α), g • ↑s = MulOpposite.op g • ↑s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- A version of `exists_ne_zero_mem_ideal_lt` where the absolute value of the real part of `a` is
smaller than `1` at some fixed complex place. This is useful to ensure that `a` is not real.  -/
NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt' : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {f : NumberField.InfinitePlace K → NNReal}
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) (w₀ : { w // w.IsComplex }),
  NumberField.mixedEmbedding.minkowskiBound K I <
      MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀) →
    ∃ a ∈ ↑I,
      a ≠ 0 ∧
        (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧
          |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
-- Mathlib.Data.Nat.Digits.Div
Nat.dvd_iff_dvd_digits_sum : ∀ (b b' : ℕ), b' % b = 1 → ∀ (n : ℕ), b ∣ n ↔ b ∣ (b'.digits n).sum
-- Aesop.Tree.Data
Aesop.Iteration.instDecidableRelLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_le_mulIndicator : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f g : α → M} {a : α},
  f a ≤ g a → s.mulIndicator f a ≤ s.mulIndicator g a
-- Mathlib.Tactic.ProxyType
/-- Default configuration. Defines `proxyType` and `proxyTypeEquiv` in the namespace
of the inductive type. Uses `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`.  -/
Mathlib.ProxyType.ProxyEquivConfig.default : Lean.InductiveVal → Mathlib.ProxyType.ProxyEquivConfig
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLE : {n : ℕ} → LE (BitVec n)
-- Std.Http.Data.Status
Std.Http.Status.accepted.sizeOf_spec : sizeOf Std.Http.Status.accepted = 1
-- Mathlib.NumberTheory.Real.Irrational
Int.not_irrational : ∀ (m : ℤ), ¬Irrational ↑m
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
map_multiset_prod : ∀ {F : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) (s : Multiset M), f s.prod = (Multiset.map (⇑f) s).prod
-- Init.Data.SInt.Bitwise
Int8.or_neg_one : ∀ {a : Int8}, a ||| -1 = -1
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_eq_ofNat : ∀ n < UInt64.size, UInt64.ofNatClamp n = UInt64.ofNat n
-- Mathlib.GroupTheory.Perm.List
List.support_formPerm_of_nodup' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α),
  l.Nodup → (∀ (x : α), l ≠ [x]) → {x | l.formPerm x ≠ x} = ↑l.toFinset
-- Init.Data.List.Basic
List.prod_nil : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α], [].prod = 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceOr : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousOn_sub_left : ∀ (a : ENNReal), ContinuousOn (fun x => a - x) {x | x ≠ ⊤}
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.ShortComplex.SnakeInput.functorL₁'.obj S = S.L₁'
-- Lean.Meta.Check
Lean.Meta.checkApp : Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_sub : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] {x y : HahnSeries Γ R} {a : Γ},
  (x - y).coeff a = x.coeff a - y.coeff a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.id_snd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (x : CategoryTheory.Limits.CategoricalPullback F G),
  (CategoryTheory.CategoryStruct.id x).snd = CategoryTheory.CategoryStruct.id x.snd
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_const_eq_zero : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsKolmogorovProcess X P p q 0 → ∀ (s t : T), ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.linearMapEquiv_apply : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] (f : M →ₗ[A] N), h.linearMapEquiv f = solution.postcomp f
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Return the current comparison set.  -/
Mathlib.Tactic.Linarith.getPCompSet : Mathlib.Tactic.Linarith.LinarithM Mathlib.Tactic.Linarith.PCompSet
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.of_bound : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.MemLp f p μ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c_1 → c = c_1
-- Mathlib.Order.SymmDiff
symmDiff_isAssociative : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α], Std.Associative fun x1 x2 => symmDiff x1 x2
-- Mathlib.Order.Filter.Basic
/-- `mkOfClosure s hs` constructs a filter on `α` whose elements set is exactly
`s : Set (Set α)`, provided one gives the assumption `hs : (generate s).sets = s`.  -/
Filter.mkOfClosure : {α : Type u} → (s : Set (Set α)) → (Filter.generate s).sets = s → Filter α
-- Mathlib.CategoryTheory.Products.Basic
/-- The diagonal functor.  -/
CategoryTheory.Functor.diag : (C : Type u₃) → [inst : CategoryTheory.Category.{v₃, u₃} C] → CategoryTheory.Functor C (C × C)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a `M → α` function to `ArchimedeanClass M → α`.  -/
ArchimedeanClass.lift : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {α : Type u_2} →
          (f : M → α) →
            (∀ (a b : M), ArchimedeanClass.mk a = ArchimedeanClass.mk b → f a = f b) → ArchimedeanClass M → α
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- Given a pre-submersive presentation, this is the composition
`I ⧸ I ^ 2 → ⊕ S dxᵢ → ⊕ S dxᵢ` where the second direct sum runs over
all `i : σ` induced by the injection `P.map : σ → ι`.

If `P` is submersive, this is an isomorphism. See `SubmersivePresentation.cotangentEquiv`.
 -/
Algebra.PreSubmersivePresentation.cotangentComplexAux : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [Finite σ] → (P : Algebra.PreSubmersivePresentation R S ι σ) → P.toExtension.Cotangent →ₗ[S] σ → S
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.mul_apply_eq_iff : ∀ {α : Type u_1} {σ τ : Equiv.Perm α}, σ.Disjoint τ → ∀ {a : α}, (σ * τ) a = a ↔ σ a = a ∧ τ a = a
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel and collects results in the original order,
including the saved state after each task completes.

Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.

Results are wrapped in `Except Exception (α × Meta.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.

The final MetaM state is restored to the initial state (before tasks ran).
 -/
Lean.Meta.MetaM.par : {α : Type} → List (Lean.MetaM α) → Lean.MetaM (List (Except Lean.Exception (α × Lean.Meta.SavedState)))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities.mk.sizeOf_spec : ∀ (dynamicRegistration? : Option Bool) (resolveSupport? : Option Lean.Lsp.ResolveSupport),
  sizeOf { dynamicRegistration? := dynamicRegistration?, resolveSupport? := resolveSupport? } =
    1 + sizeOf dynamicRegistration? + sizeOf resolveSupport?
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.filterMapWithPostcondition : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : LawfulMonad n] [inst_4 : Std.Iterator α₁ m β] [inst_5 : Std.Iterator α₂ m β]
  [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.filterMapWithPostcondition f ita).Equiv (Std.IterM.filterMapWithPostcondition f itb)
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Given `R`-modules `A, B` with comultiplication maps `Δ_A, Δ_B` and counit maps
`ε_A, ε_B`, an `R`-coalgebra homomorphism `A →ₗc[R] B` is an `R`-linear map `f` such that
`ε_B ∘ f = ε_A` and `(f ⊗ f) ∘ Δ_A = Δ_B ∘ f`.  -/
«term_→ₗc[_]_» : Lean.TrailingParserDescr
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.monotone_preCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ],
  ∀ᵐ (a : α) ∂ρ.fst, Monotone fun r => ProbabilityTheory.preCDF ρ r a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.bot_lt_top_iff_nonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊥ < ⊤ ↔ Nonempty C
-- Mathlib.Topology.MetricSpace.Isometry
Fin.edist_append_eq_max_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (m n : ℕ) {x x2 : Fin m → α} {y y2 : Fin n → α},
  edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)
-- Mathlib.Data.Finite.Defs
/-- assertion that `α` is `¬Finite`  -/
Infinite.not_finite : ∀ {α : Sort u_3} [self : Infinite α], ¬Finite α
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₁ : ∀ (pq : ℤ × ℤ), CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological.i₁ pq = WithBotTop.coe pq.2
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformlyOn.smul₀_of_isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {s : Set X} {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (f y) 0) →
        (∀ x ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhdsWithin x s) fun y => dist (g y) 0) →
          TendstoLocallyUniformlyOn (F • G) (f • g) l s
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.measure_Ioi_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] {m : MeasurableSpace X}
  (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [NoMaxOrder X] (a : X), 0 < μ (Set.Ioi a)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.closure_pow_le : ∀ {M : Type u_3} [inst : Monoid M] {s : Set M} {n : ℕ}, Submonoid.closure (s ^ n) ≤ Submonoid.closure s
-- Mathlib.Data.List.ReduceOption
List.reduceOption_getElem?_iff : ∀ {α : Type u_1} {l : List (Option α)} {x : α}, (∃ i, l[i]? = some (some x)) ↔ ∃ i, l.reduceOption[i]? = some x
-- Aesop.Tree.Data
Aesop.instInhabitedGoalOrigin.default : Aesop.GoalOrigin
-- Lean.Server.Completion.CompletionCollectors
/-- Return `true` if `e` is a `declName`-application, or can be unfolded (delta-reduced) to one.  -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.isDefEqToAppOf : Lean.Expr → Lean.Name → Lean.MetaM Bool
-- Mathlib.Tactic.UnsetOption
/-- unset the option specified by id  -/
Lean.Elab.elabUnsetOption : {m : Type → Type} →
  [Monad m] → [Lean.MonadOptions m] → [Lean.MonadRef m] → [Lean.Elab.MonadInfoTree m] → Lean.Syntax → m Lean.Options
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.HasBasis.uniformity_of_nhds_zero_neg_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Sort u_3} {p : ι → Prop}
  {U : ι → Set α}, (nhds 0).HasBasis p U → (uniformity α).HasBasis p fun i => {x | -x.1 + x.2 ∈ U i}
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthSup_nonneg : ∀ {u : ℕ → ENNReal}, Monotone u → u ≠ 0 → 0 ≤ ExpGrowth.expGrowthSup u
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket commutes with taking pullbacks. One could also give a version avoiding
completeness but requiring that `f` is a local diffeomorphism.  -/
VectorField.pullback_lieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [CompleteSpace E],
  minSmoothness 𝕜 2 ≤ n →
    ∀ {f : E → F} {V W : F → F} {x : E},
      ContDiffAt 𝕜 n f x →
        DifferentiableAt 𝕜 V (f x) →
          DifferentiableAt 𝕜 W (f x) →
            VectorField.pullback 𝕜 f (VectorField.lieBracket 𝕜 V W) x =
              VectorField.lieBracket 𝕜 (VectorField.pullback 𝕜 f V) (VectorField.pullback 𝕜 f W) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) =
        (compare k a == Ordering.eq || Std.DTreeMap.Internal.Impl.contains a t)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_one : ∀ {K : Type u} [inst : CommRing K], { toFractionRing := 1 } = 1
-- Mathlib.Order.Grade
/-- An `𝕆`-graded order where minimal elements have minimal grades.  -/
GradeMinOrder : (𝕆 : Type u_5) → (α : Type u_6) → [Preorder 𝕆] → [Preorder α] → Type (max u_5 u_6)
-- Mathlib.Topology.Algebra.Star
instContinuousStarMulOpposite : ∀ {R : Type u_1} [inst : Star R] [inst_1 : TopologicalSpace R] [ContinuousStar R], ContinuousStar Rᵐᵒᵖ
-- Mathlib.Logic.Equiv.Fin.Rotate
coe_finRotate_symm_of_ne_zero : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, i ≠ 0 → ↑((Equiv.symm (finRotate n)) i) = ↑i - 1
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.instIsFilteredOfFactIsRegular : ∀ (X : Type u) (κ : Cardinal.{u}) [Fact κ.IsRegular], CategoryTheory.IsFiltered (HasCardinalLT.Set X κ)
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero : ∀ (a : ℂ),
  HasFPowerSeriesOnBall (fun x => 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun n => Ring.choose (a + ↑n - 1) n) 0 1
-- Mathlib.Data.List.AList
AList.mem_of_perm : ∀ {α : Type u} {β : α → Type v} {a : α} {s₁ s₂ : AList β}, s₁.entries.Perm s₂.entries → (a ∈ s₁ ↔ a ∈ s₂)
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.free_obj : ∀ (α : Type u), AddCommGrpCat.free.obj α = AddCommGrpCat.of (FreeAbelianGroup α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_contains_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool} {k : α}, (Std.HashMap.filter f m).contains k = true → m.contains k = true
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncMap_comp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M)
  (e : c.Embedding c') [inst_3 : e.IsRelIff],
  HomologicalComplex.stupidTruncMap (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.stupidTruncMap φ e) (HomologicalComplex.stupidTruncMap φ' e)
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.vars_neg : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R), (-p).vars = p.vars
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n a n' : ℤ) (hn' : n' + a = n) (γ : CochainComplex.HomComplex.Cocycle K L n),
  (CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv n a n' hn') γ = γ.rightShift a n' hn'
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.continuous_of_continuous_eval : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [inst_6 : TopologicalSpace α] {g : α → WeakBilin B},
  (∀ (y : F), Continuous fun a => (B (g a)) y) → Continuous g
-- Init.Data.UInt.Bitwise
UInt32.ofNatLT_shiftLeft : ∀ {a b : ℕ} (ha : a <<< b < UInt32.size) (hb : b < 32),
  UInt32.ofNatLT (a <<< b) ha = UInt32.ofNatLT a ⋯ <<< UInt32.ofNatLT b ⋯
-- Mathlib.Algebra.Quaternion
/-- Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$,
denoted as `ℍ[R,a,b]`.
Implemented as a structure with four fields: `re`, `imI`, `imJ`, and `imK`.  -/
Quaternion.«termℍ[_,_,_,_]» : Lean.ParserDescr
-- Mathlib.Topology.Spectral.Prespectral
/-- A space is prespectral if it has a basis consisting of compact opens.  -/
PrespectralSpace.of_isTopologicalBasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {B : Set (Set X)},
  TopologicalSpace.IsTopologicalBasis B → (∀ U ∈ B, IsCompact U) → PrespectralSpace X
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Coercion of a pretrivialization to a function. We don't use `e.toFun` in the `CoeFun` instance
because it is actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about
`toPartialEquiv`. While we may want to switch to this behavior later, doing it mid-port will break a
lot of proofs.  -/
Bundle.Pretrivialization.toFun' : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → {proj : Z → B} → Bundle.Pretrivialization F proj → Z → B × F
-- Mathlib.Computability.Partrec
Computable.option_some_iff : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
  (Computable fun a => some (f a)) ↔ Computable f
-- Mathlib.Topology.Convenient.Category
/-- The inclusion functor `GeneratedByTopCat X ⥤ TopCat`.  -/
GeneratedByTopCat.toTopCat : {ι : Type t} →
  {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.Functor (GeneratedByTopCat X) TopCat
-- Mathlib.Data.Sym.Sym2.Finsupp
Finsupp.coe_sym2Mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : CommMonoidWithZero M₀] (f : α →₀ M₀), ⇑f.sym2Mul = Sym2.mul ∘ Sym2.map ⇑f
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.hε : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C],
  AlgebraicTopology.DoldKan.Compatibility.υ CategoryTheory.Idempotents.DoldKan.isoN₁ = AlgebraicTopology.DoldKan.Γ₂N₁
-- Init.Data.String.Defs
String.instCoeSlice : Coe String String.Slice
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.union_right : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsCofinalFor s t → IsCofinalFor (t ∪ s) t
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.algebra.eq_1 : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M],
  MonoidAlgebra.algebra =
    { toSMul := MonoidAlgebra.smulZeroClass.toSMul, algebraMap := MonoidAlgebra.singleOneRingHom.comp (algebraMap R A),
      commutes' := ⋯, smul_def' := ⋯ }
-- Lean.Environment
/-- Information about the current branch of the environment representing asynchronous elaboration.

Use `Environment.enterAsync` instead of `mkRaw`.
 -/
_private.Lean.Environment.0.Lean.AsyncContext : Type
-- Mathlib.Logic.Equiv.Prod
/-- `PUnit` is a left identity for type product up to an equivalence.  -/
Equiv.punitProd : (α : Type u_9) → PUnit.{u_10 + 1} × α ≃ α
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasFDerivAt c c' x → ∀ (f : F), HasFDerivAt (fun y => c y • f) (c'.smulRight f) x