mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Quiver.Path.Weight
_private.Mathlib.Combinatorics.Quiver.Path.Weight.0.Quiver.Path.weight.match_1.splitter : {V : Type u_2} →
  [inst : Quiver V] →
    (motive : (x x_1 : V) → Quiver.Path x x_1 → Sort u_3) →
      (x x_1 : V) →
        (x_2 : Quiver.Path x x_1) →
          ((a : V) → motive a a Quiver.Path.nil) →
            ((a x b : V) → (p : Quiver.Path a b) → (e : b ⟶ x) → motive a x (p.cons e)) → motive x x_1 x_2
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- Convergence in distribution of random variables.
This is the weak convergence of the laws of the random variables: `Tendsto` in the
`ProbabilityMeasure` type.  -/
MeasureTheory.TendstoInDistribution : {ι : Type u_1} →
  {E : Type u_2} →
    {Ω' : Type u_3} →
      {Ω : ι → Type u_5} →
        {m : (i : ι) → MeasurableSpace (Ω i)} →
          {m' : MeasurableSpace Ω'} →
            {mE : MeasurableSpace E} →
              [inst : TopologicalSpace E] →
                [OpensMeasurableSpace E] →
                  ((i : ι) → Ω i → E) →
                    Filter ι →
                      (Ω' → E) →
                        (μ : (i : ι) → MeasureTheory.Measure (Ω i)) →
                          [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] →
                            (μ' : autoParam (MeasureTheory.Measure Ω') MeasureTheory.TendstoInDistribution._auto_1) →
                              [MeasureTheory.IsProbabilityMeasure μ'] → Prop
-- Mathlib.Order.LiminfLimsup
Filter.eventually_lt_of_lt_liminf : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} [inst : ConditionallyCompleteLinearOrder β] {u : α → β} {b : β},
  b < Filter.liminf u f →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.eventually_lt_of_lt_liminf._auto_1 →
      ∀ᶠ (a : α) in f, b < u a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₁ → (m₁ ∩ m₂)[k]! = default
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- The operator norm of the projection is `1` if there is an element whose norm is different from
`0`.  -/
SeparationQuotient.norm_normedMk_eq_one : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] [NontrivialTopology M], ‖SeparationQuotient.normedMk‖ = 1
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.iterateInduction.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.CategoryTheory.Sites.Limits
/-- An auxiliary definition to be used below.

Whenever `E` is a cone of shape `K` of sheaves, and `S` is the multifork associated to a
covering `W` of an object `X`, with respect to the cone point `E.X`, this provides a cone of
shape `K` of objects in `D`, with cone point `S.X`.

See `isLimitMultiforkOfIsLimit` for more on how this definition is used.
 -/
CategoryTheory.Sheaf.multiforkEvaluationCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {K : Type z} →
            [inst_2 : CategoryTheory.Category.{z', z} K] →
              (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) →
                (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))) →
                  (X : C) →
                    (W : J.Cover X) →
                      CategoryTheory.Limits.Multifork (W.index E.pt) →
                        CategoryTheory.Limits.Cone
                          (F.comp
                            ((CategoryTheory.sheafToPresheaf J D).comp
                              ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))
-- Mathlib.Data.List.Sym
List.sym.eq_def : ∀ {α : Type u_1} (x : ℕ) (x_1 : List α),
  List.sym x x_1 =
    match x, x_1 with
    | 0, x => [Sym.nil]
    | x, [] => []
    | n.succ, x :: xs => List.map (fun p => x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs
-- Mathlib.Algebra.Order.Kleene
/-- The Kleene star operator on a Kleene algebra  -/
Computability.«term_∗» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} (self : L.Hom L') {Z : C₂} (h : X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) (CategoryTheory.CategoryStruct.comp L'.w h) =
    CategoryTheory.CategoryStruct.comp L.w h
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.generatedNormal_isNormal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X : (c d : C) → Set (c ⟶ d)),
  (CategoryTheory.Subgroupoid.generatedNormal X).IsNormal
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- `limit.π (F ⋙ forget (ModuleCat.{w} R)) j` as an `R`-linear map.  -/
ModuleCat.limitπLinearMap : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] →
            (j : J) →
              (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt →ₗ[R]
                (F.comp (CategoryTheory.forget (ModuleCat R))).obj j
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra)
  [inst_2 : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))],
  (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).ι =
    F.map (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
-- Mathlib.Algebra.Group.TypeTags.Basic
isRightRegular_ofAdd : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, IsRightRegular (Multiplicative.ofAdd a) ↔ IsAddRightRegular a
-- Init.Data.UInt.Lemmas
UInt64.one_def : 1 = { toBitVec := 1 }
-- Mathlib.Topology.Algebra.Monoid
Topology.IsInducing.continuousMul : ∀ {M : Type u_6} {N : Type u_7} {F : Type u_8} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] [inst_4 : TopologicalSpace M] [inst_5 : TopologicalSpace N] [ContinuousMul N] (f : F),
  Topology.IsInducing ⇑f → ContinuousMul M
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.smul_eq_iff_of_mem : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (r : R) (hr : r ∈ S) (x y : LocalizedModule S M), r • x = y ↔ x = Localization.mk 1 ⟨r, hr⟩ • y
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C)
  (S : CategoryTheory.Sieve X), J.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), J.Saturate Y (CategoryTheory.Sieve.pullback f S)
-- Mathlib.Geometry.Diffeology.Basic
_private.Mathlib.Geometry.Diffeology.Basic.0.term𝔼__ : Lean.ParserDescr
-- Init.Data.SInt.Basic
/-- Bitwise exclusive or for 8-bit signed integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.xor : Int8 → Int8 → Int8
-- Mathlib.GroupTheory.Complement
Subgroup.exists_isComplement_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : G), ∃ S, Subgroup.IsComplement S ↑H ∧ g ∈ S
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.liesOver : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] [p.IsMaximal]
  (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset), (↑P).LiesOver p
-- Lean.Meta.Basic
/-- Return the local declaration for the given free variable.
Throw an exception if local declaration is not in the current local context.
 -/
Lean.FVarId.getDecl : Lean.FVarId → Lean.MetaM Lean.LocalDecl
-- Mathlib.Order.LiminfLimsup
/-- The `limsInf` of a filter `f` is the supremum of the `a` such that the inequality
`x ≥ a` eventually holds for `f`.  -/
Filter.limsInf : {α : Type u_1} → [ConditionallyCompleteLattice α] → Filter α → α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' → (Std.ExtTreeMap.filterMap f t).getD k fallback = (t[k]?.bind (f k')).getD fallback
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_insert_div : ∀ {ι : Type u_1} {G : Type u_3} {s : Finset ι} {a : ι} [inst : CommGroup G] [inst_1 : DecidableEq ι],
  a ∉ s → ∀ (f : ι → G), (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.cokernelSequence_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.ShortComplex.cokernelSequence f).g = CategoryTheory.Limits.cokernel.π f
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The co-Kleisli adjunction which gives rise to the comonad `(U, ε_ U, δ_ U)`.  -/
CategoryTheory.Cokleisli.Adjunction.adj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Comonad C) →
      CategoryTheory.Cokleisli.Adjunction.fromCokleisli U ⊣ CategoryTheory.Cokleisli.Adjunction.toCokleisli U
-- Mathlib.Data.Set.Basic
Set.sep_and : ∀ {α : Type u} {s : Set α} {p q : α → Prop}, {x | x ∈ s ∧ p x ∧ q x} = {x | x ∈ s ∧ p x} ∩ {x | x ∈ s ∧ q x}
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.hom_ext_iff : ∀ {R : Type u} [inst : Ring R] {V W : FGModuleCat R} {f g : V ⟶ W},
  f = g ↔ ModuleCat.Hom.hom f.hom = ModuleCat.Hom.hom g.hom
-- Init.Data.List.MinMax
List.isSome_min?_of_mem : ∀ {α : Type u_1} {l : List α} [inst : Min α] {a : α}, a ∈ l → l.min?.isSome = true
-- Mathlib.Data.List.Sigma
List.nodup_zipIdx_map_snd : ∀ {α : Type u} (l : List α), (List.map Prod.snd l.zipIdx).Nodup
-- Mathlib.Algebra.Star.StarRingHom
/-- `StarRingEquivClass F A B` asserts `F` is a type of bundled ⋆-ring equivalences between `A` and
`B`.
You should also extend this typeclass when you extend `StarRingEquiv`.  -/
StarRingEquivClass : (F : Type u_1) →
  (A : outParam (Type u_2)) →
    (B : outParam (Type u_3)) → [Add A] → [Mul A] → [Star A] → [Add B] → [Mul B] → [Star B] → [EquivLike F A B] → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.contains a = false
-- Mathlib.Data.Matrix.Mul
instIsStablyFiniteRingSubtypeMem : ∀ {R : Type u_10} {F : Type u_12} [inst : NonAssocSemiring R] [inst_1 : SetLike F R] [inst_2 : SubsemiringClass F R]
  (S : F) [IsStablyFiniteRing R], IsStablyFiniteRing ↥S
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.finite_setOfPred_matroid'`.

---

For finite `E`, finitely many matroids have ground set `E`.  -/
Matroid.finite_setOf_matroid' : ∀ {α : Type u_1} {E : Set α}, E.Finite → {M | M.E = E}.Finite
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci.inj : ∀ {lo lo_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound},
  Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo = Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.ci lo_1 →
    lo = lo_1
-- Lean.Server.RequestCancellation
Lean.Server.CancellableT : (Type → Type u_1) → Type → Type u_1
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-closed right-unbounded range as an array in ascending order.
 -/
Std.Rci.toArray : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxi.IsAlwaysFinite α] → Std.Rci α → Array α
-- Mathlib.Algebra.Order.Hom.Basic
le_map_div_add_map_div : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : Add β]
  [inst_3 : LE β] [MulLEAddHomClass F α β] (f : F) (a b c : α), f (a / c) ≤ f (a / b) + f (b / c)
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.isNode : {α : Type u_1} → Lean.PersistentArrayNode α → Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_zsmul : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (r : ℤ)
  (f : BoundedContinuousFunction α β), ⇑(r • f) = r • ⇑f
-- Lean.Expr
/-- Return `true` if `e` contains expression metavariables.
This is a constant time operation.
 -/
Lean.Expr.hasExprMVar : Lean.Expr → Bool
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Graphs on a set of vertices embed in their `spanningCoe`.  -/
SimpleGraph.Embedding.spanningCoe : {V : Type u_1} → {s : Set V} → (G : SimpleGraph ↑s) → G ↪g G.spanningCoe
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn_3.go : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1} →
        {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
          {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
            {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1} →
              (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                ((t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t) →
                  ((t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                      Lean.PrefixTreeNode.below_1 t → motive_2 t) →
                    ((t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) →
                        Lean.PrefixTreeNode.below_2 t → motive_3 t) →
                      ((t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                          Lean.PrefixTreeNode.below_3 t → motive_4 t) →
                        motive_4 t ×' Lean.PrefixTreeNode.below_3 t
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.mk.inj : ∀ {config : Lean.Grind.Config} {extensions : Lean.Meta.Grind.ExtensionStateArray}
  {extra : Lean.PArray Lean.Meta.Grind.EMatchTheorem} {extraInj : Lean.PArray Lean.Meta.Grind.InjectiveTheorem}
  {extraFacts : Lean.PArray Lean.Expr} {symPrios : Lean.Meta.Grind.SymbolPriorities} {norm : Lean.Meta.Simp.Context}
  {normProcs : Array Lean.Meta.Simprocs} {anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)}
  {config_1 : Lean.Grind.Config} {extensions_1 : Lean.Meta.Grind.ExtensionStateArray}
  {extra_1 : Lean.PArray Lean.Meta.Grind.EMatchTheorem} {extraInj_1 : Lean.PArray Lean.Meta.Grind.InjectiveTheorem}
  {extraFacts_1 : Lean.PArray Lean.Expr} {symPrios_1 : Lean.Meta.Grind.SymbolPriorities}
  {norm_1 : Lean.Meta.Simp.Context} {normProcs_1 : Array Lean.Meta.Simprocs}
  {anchorRefs?_1 : Option (Array Lean.Meta.Grind.AnchorRef)},
  { config := config, extensions := extensions, extra := extra, extraInj := extraInj, extraFacts := extraFacts,
        symPrios := symPrios, norm := norm, normProcs := normProcs, anchorRefs? := anchorRefs? } =
      { config := config_1, extensions := extensions_1, extra := extra_1, extraInj := extraInj_1,
        extraFacts := extraFacts_1, symPrios := symPrios_1, norm := norm_1, normProcs := normProcs_1,
        anchorRefs? := anchorRefs?_1 } →
    config = config_1 ∧
      extensions = extensions_1 ∧
        extra = extra_1 ∧
          extraInj = extraInj_1 ∧
            extraFacts = extraFacts_1 ∧
              symPrios = symPrios_1 ∧ norm = norm_1 ∧ normProcs = normProcs_1 ∧ anchorRefs? = anchorRefs?_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.type : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negY_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.negY P = -P 1
-- Mathlib.Combinatorics.Hall.Basic
/-- This is a version of **Hall's Marriage Theorem** in terms of a relation
between types `α` and `β` such that `α` is finite and the image of
each `x : α` is finite (it suffices for `β` to be finite; see
`Fintype.all_card_le_filter_rel_iff_exists_injective`).  There is
a transversal of the relation (an injective function `α → β` whose graph is
a subrelation of the relation) iff every subset of
`k` terms of `α` is related to at least `k` terms of `β`.

Note: if `[Fintype β]`, then there exist instances for `[∀ (a : α), Fintype (R.image {a})]`.
 -/
Fintype.all_card_le_rel_image_card_iff_exists_injective : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (R : SetRel α β) [inst_1 : (a : α) → Fintype ↑(R.image {a})],
  (∀ (A : Finset α), A.card ≤ Fintype.card ↑(R.image ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), (x, f x) ∈ R
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the set of expressions `e` is a child of, or an expression in
`e`s equivalence class is a child of.
The information is only up to date if `e` is the root (aka canonical representative) of the equivalence class.
 -/
Lean.Meta.Grind.getParents : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.ParentSet
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ico.mk_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] [inst_3 : Nontrivial R]
  (h : 0 ∈ Set.Ico 0 1), ⟨0, h⟩ = 0
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.lowerCentralSeries_succ : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ),
  LieModule.lowerCentralSeries R L M (k + 1) = ⁅⊤, LieModule.lowerCentralSeries R L M k⁆
-- Lean.Environment
Lean.PersistentEnvExtensionState : Type → Type → Type
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_right_strictMono₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 1 < a → StrictMono fun n => a ^ n
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.dist_triangle_max : ∀ {X : Type u_2} {inst : Dist X} [self : IsUltrametricDist X] (x y z : X), dist x z ≤ max (dist x y) (dist y z)
-- Lean.Parser.Extra
Lean.Parser.sepBy.formatter : Lean.PrettyPrinter.Formatter →
  String → Lean.PrettyPrinter.Formatter → optParam Bool false → Lean.PrettyPrinter.Formatter
-- Init.Data.Nat.Lemmas
Nat.add_eq_min_iff : ∀ {m n : ℕ}, m + n = min m n ↔ m = 0 ∧ n = 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
EuclideanGeometry.angle_self_orthogonalProjection : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p : P) {p' : P} {s : AffineSubspace ℝ P}
  [inst_4 : s.direction.HasOrthogonalProjection] (h : p' ∈ s),
  EuclideanGeometry.angle p (↑((EuclideanGeometry.orthogonalProjection s) p)) p' = Real.pi / 2
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow_nc.induct_unfolding : ∀ (p : Lean.Grind.CommRing.Poly) (motive : ℕ → Lean.Grind.CommRing.Poly → Prop),
  motive 0 (Lean.Grind.CommRing.Poly.num 1) →
    motive 1 p →
      (∀ (k : ℕ), (k = 0 → False) → motive k (p.pow_nc k) → motive k.succ ((p.pow_nc k).mul_nc p)) →
        ∀ (k : ℕ), motive k (p.pow_nc k)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G],
  ContMDiff (I.prod I) I n fun p => p.1 * p.2
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.tendsto_comp_exp_atBot : ∀ {α : Type u_1} {l : Filter α} {f : ℝ → α},
  Filter.Tendsto (fun x => f (Real.exp x)) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin 0 (Set.Ioi 0)) l
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiffWithinAt_piLp' : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E} {t : Set H} {y : H},
  (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => (f x).ofLp i) t y) → ContDiffWithinAt 𝕜 n f t y
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.le_lexOrder_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ : MvPowerSeries σ R} {w : WithTop (Lex (σ →₀ ℕ))},
  w ≤ φ.lexOrder ↔ ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (MvPowerSeries.coeff d) φ = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc) {Z : C} (h : X.obj { len := n + 1 + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ (i.castLT ⋯)) (CategoryTheory.CategoryStruct.comp (X.δ j.succ) h) =
    CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h)
-- Std.Http.Protocol.H1.Writer
/-- Body chunks supplied by the user, accumulated before being flushed to output.
 -/
Std.Http.Protocol.H1.Writer.userData : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Array Std.Http.Chunk
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- A family of friendly operations on sequences indexed by a type `γ`.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass : {α : Type u_1} → {γ : Type u_3} → (γ → Stream'.Seq α → Stream'.Seq α) → Prop
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.IsNontrivial.exists_abv_gt_one : ∀ {R : Type u_3} {S : Type u_4} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  [ExistsAddOfLE S] {v : AbsoluteValue R S}, v.IsNontrivial → ∃ x, 1 < v x
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q (CategoryTheory.Limits.pushout f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g)) h