mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.toPlusNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  (J.toPlusNatTrans D).app P = J.toPlus P
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_inj : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.coeff = q.coeff ↔ p = q
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, s ∩ {a} = if a ∈ s then {a} else ∅
-- Mathlib.Analysis.Calculus.FDeriv.Prod
Differentiable.snd : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₂ : E → F × G},
  Differentiable 𝕜 f₂ → Differentiable 𝕜 fun x => (f₂ x).2
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend'.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)],
  Bundle.Pretrivialization.codExtend' hs e =
    { toFun := fun z => (↑(↑e z).1, (↑e z).2),
      invFun := fun x => if h : x.1 ∈ s then e.invFun (⟨x.1, h⟩, x.2) else Classical.arbitrary (B → F → Z) x.1 x.2,
      source := e.source, target := Prod.map Subtype.val id '' e.target, map_source' := ⋯, map_target' := ⋯,
      left_inv' := ⋯, right_inv' := ⋯, open_target := ⋯, baseSet := Subtype.val '' e.baseSet, open_baseSet := ⋯,
      source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.CategoryTheory.Groupoid
/-- A category where every morphism `IsIso` is a groupoid.  -/
CategoryTheory.Groupoid.ofIsIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f) → CategoryTheory.Groupoid C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k a : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).getKey! a = if compare k a = Ordering.eq then default else t.getKey! a
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Symm.map`. -/
Relation.map_symmetric : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Symm r] (f : α → β), Std.Symm (Relation.Map r f f)
-- Mathlib.Data.Rat.Cast.Order
NNRat.castOrderEmbedding_apply : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K] (a : ℚ≥0),
  NNRat.castOrderEmbedding a = ↑a
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
/-- Predicate saying that a connection `∇` on a Riemannian bundle `(V, g)` is compatible with the
ambient metric, i.e. for all differentiable vector fields `X` on `M` and sections `σ` and `τ` of
`V`, we have `X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩`.  -/
CovariantDerivative.IsMetricCompatible : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type u_3} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  {F : Type u_4} →
                    [inst_5 : NormedAddCommGroup F] →
                      [inst_6 : NormedSpace ℝ F] →
                        {V : M → Type u_5} →
                          [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] →
                            [inst_8 : (x : M) → NormedAddCommGroup (V x)] →
                              [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] →
                                [inst_10 : FiberBundle F V] →
                                  CovariantDerivative I F V →
                                    [inst_11 : VectorBundle ℝ F V] →
                                      [IsContMDiffRiemannianBundle I 1 F V] →
                                        [ContMDiffVectorBundle 1 F V I] → [FiniteDimensional ℝ F] → Prop
-- Mathlib.Analysis.Convex.GaugeRescale
/-- `gaugeRescale` bundled as a `Homeomorph`.  -/
gaugeRescaleHomeomorph : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : Module ℝ E] →
      [inst_2 : TopologicalSpace E] →
        [IsTopologicalAddGroup E] →
          [ContinuousSMul ℝ E] →
            [T1Space E] →
              (s t : Set E) →
                Convex ℝ s →
                  s ∈ nhds 0 →
                    Bornology.IsVonNBounded ℝ s → Convex ℝ t → t ∈ nhds 0 → Bornology.IsVonNBounded ℝ t → E ≃ₜ E
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.removeZero_coeff_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), p.removeZero 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- A cofork is a colimit cocone if and only if the corresponding fork in the opposite category is
a limit cone.  -/
CategoryTheory.Limits.Cofork.isColimitEquivIsLimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        (c : CategoryTheory.Limits.Cofork f g) → CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsLimit c.op
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.clm_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5} [inst_7 : NormedAddCommGroup X]
  [inst_8 : NormedSpace 𝕜 X] {n : WithTop ℕ∞} {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {x : X},
  ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => g x ∘SL f x) x
-- Mathlib.Data.Finset.Interval
/-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (cons a s ha)` for
all `s` and `a ∉ s`.  -/
Finset.strictMono_iff_forall_lt_cons : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f : Finset α → β},
  StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (Finset.cons a s ha)
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.lt_rearrange : ∀ {α : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α}, a - b < 0 → a < b
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_le_artanh : ∀ {x y : ℝ}, -1 < x → y < 1 → x ≤ y → Real.artanh x ≤ Real.artanh y
-- Mathlib.Tactic.Widget.CongrM
/-- The congrm widget.  -/
CongrMSelectionPanel : ProofWidgets.Component SelectInsertParams
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.of_eq : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → t₁ = t₃ → t₂ = t₄ → p.Splits t₃ t₄
-- Mathlib.Topology.Category.Profinite.Product
/-- The object part of the functor `indexFunctor : (Finset ι)ᵒᵖ ⥤ Profinite`.  -/
Profinite.IndexFunctor.obj : {ι : Type u} →
  {X : ι → Type} →
    [(i : ι) → TopologicalSpace (X i)] → Set ((i : ι) → X i) → (J : ι → Prop) → Set ((i : { i // J i }) → X ↑i)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for 2-morphisms.  -/
Mathlib.Tactic.BicategoryLike.Mor₂ : Type
-- Mathlib.Data.List.Lemmas
List.mapAccumr.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ → γ × β) (x : γ) (y : α) (yr : List α),
  List.mapAccumr f (y :: yr) x =
    ((f y (List.mapAccumr f yr x).1).1, (f y (List.mapAccumr f yr x).1).2 :: (List.mapAccumr f yr x).2)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_eq_zero_iff_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → (x ^ y = 0 ↔ x = 0 ∧ y ≠ 0)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonLeanClientCapabilities : Lean.ToJson Lean.Lsp.LeanClientCapabilities
-- Mathlib.Data.ZMod.QuotientGroup
MulAction.minimalPeriod_pos : ∀ {α : Type u_3} {β : Type u_4} [inst : Group α] (a : α) [inst_1 : MulAction α β] (b : β)
  [Finite ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)], NeZero (Function.minimalPeriod (fun x => a • x) b)
-- Mathlib.Topology.MetricSpace.Bounded
/-- If a function is continuous on a set `s` containing a compact set `k`, then it is bounded on
some open neighborhood of `k` in `s`.  -/
Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
  IsCompact k → k ⊆ s → ContinuousOn f s → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_mem_of_mem_closure_of_mem : ∀ {G : Type u_2} [inst : Group G] {X : Type u_5} [inst_1 : MulAction G X] {s : Set G} {t : Set X},
  (∀ g ∈ s, g⁻¹ ∈ s) → (∀ g ∈ s, ∀ x ∈ t, g • x ∈ t) → ∀ {g : G}, g ∈ Subgroup.closure s → ∀ {x : X}, x ∈ t → g • x ∈ t
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.State.mk.injEq : ∀ (structs : Array Lean.Meta.Grind.Arith.Linear.Struct) (typeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (exprToStructIdEntries : Lean.PArray (Lean.Expr × ℕ))
  (forbiddenNatModules : Lean.PHashSet Lean.Meta.Sym.ExprPtr)
  (natStructs : Array Lean.Meta.Grind.Arith.Linear.NatStruct)
  (natTypeIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToNatStructId : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (structs_1 : Array Lean.Meta.Grind.Arith.Linear.Struct)
  (typeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToStructId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ) (exprToStructIdEntries_1 : Lean.PArray (Lean.Expr × ℕ))
  (forbiddenNatModules_1 : Lean.PHashSet Lean.Meta.Sym.ExprPtr)
  (natStructs_1 : Array Lean.Meta.Grind.Arith.Linear.NatStruct)
  (natTypeIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToNatStructId_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ),
  ({ structs := structs, typeIdOf := typeIdOf, exprToStructId := exprToStructId,
        exprToStructIdEntries := exprToStructIdEntries, forbiddenNatModules := forbiddenNatModules,
        natStructs := natStructs, natTypeIdOf := natTypeIdOf, exprToNatStructId := exprToNatStructId } =
      { structs := structs_1, typeIdOf := typeIdOf_1, exprToStructId := exprToStructId_1,
        exprToStructIdEntries := exprToStructIdEntries_1, forbiddenNatModules := forbiddenNatModules_1,
        natStructs := natStructs_1, natTypeIdOf := natTypeIdOf_1, exprToNatStructId := exprToNatStructId_1 }) =
    (structs = structs_1 ∧
      typeIdOf = typeIdOf_1 ∧
        exprToStructId = exprToStructId_1 ∧
          exprToStructIdEntries = exprToStructIdEntries_1 ∧
            forbiddenNatModules = forbiddenNatModules_1 ∧
              natStructs = natStructs_1 ∧ natTypeIdOf = natTypeIdOf_1 ∧ exprToNatStructId = exprToNatStructId_1)
-- Mathlib.CategoryTheory.Action.Basic
Action.hom_inv_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f : M ≅ N), CategoryTheory.CategoryStruct.comp f.hom.hom f.inv.hom = CategoryTheory.CategoryStruct.id M.V
-- Init.Data.List.Basic
/-- True if the first list is a potentially non-contiguous sub-sequence of the second list, comparing
elements with the `==` operator.

The relation `List.Sublist` is a logical characterization of this property.

Examples:
* `[1, 3].isSublist [0, 1, 2, 3, 4] = true`
* `[1, 3].isSublist [0, 1, 2, 4] = false`
 -/
List.isSublist : {α : Type u} → [BEq α] → List α → List α → Bool
-- Mathlib.Order.Monotone.Basic
antitone_nat_of_succ_le : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f (n + 1) ≤ f n) → Antitone f
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instCompactSpaceOfDiscreteTopology : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A] [DiscreteTopology A], CompactSpace (PontryaginDual A)
-- Lean.Util.ShareCommon
Lean.ShareCommon.ShareCommonT.run : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → Lean.ShareCommon.ShareCommonT m α → m α
-- Mathlib.Analysis.Normed.Group.Basic
vadd_ball'' : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, a +ᵥ Metric.ball b r = Metric.ball (a +ᵥ b) r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.distinct_keys_toList : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop.instNormal : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup Gᵐᵒᵖ} [H.Normal], H.unop.Normal
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A Dirichlet character is even if its value at -1 is 1.  -/
DirichletCharacter.Even : {S : Type u_2} → [inst : CommRing S] → {m : ℕ} → DirichletCharacter S m → Prop
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_comap_eq_self_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Surjective ⇑f → ∀ (H : Subgroup N), Subgroup.map f (Subgroup.comap f H) = H
-- Init.Data.Bool
Bool.false_xor : ∀ (x : Bool), (false ^^ x) = x
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Turn an element of a type `F` satisfying `MulEquivClass F α β` into an actual
`MulEquiv`. This is declared as the default coercion from `F` to `α ≃* β`.  -/
MulEquivClass.toMulEquiv : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : EquivLike F α β] → [inst_1 : Mul α] → [inst_2 : Mul β] → [MulEquivClass F α β] → F → α ≃* β
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.AsSmall.hasFiniteLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.AsSmall C)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  Std.DHashMap.Const.get (m.insertIfNew k v) a h₁ =
    if h₂ : (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Const.get m a ⋯
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_rec : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} {g : α → ℕ × β → β},
  Primrec f → Primrec₂ g → Primrec₂ fun a n => Nat.rec (f a) (fun n IH => g a (n, IH)) n
-- Mathlib.Data.Vector3
/-- Recursion principle with the vector as first argument.  -/
Vector3.recOn : {α : Type u_1} →
  {C : {n : ℕ} → Vector3 α n → Sort u} →
    {n : ℕ} → (v : Vector3 α n) → C [] → ({n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)) → C v
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContDiff.comp_contMDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_7} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {g : F → F'} {f : M → F} {s : Set M} {x : M},
  ContDiff 𝕜 n g →
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F) n f s x →
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n (g ∘ f) s x
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderiv_pow_ring' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {x : 𝔸} (n : ℕ),
  fderiv 𝕜 (fun x => x ^ n) x =
    ∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieModule.IsIrreducible.mk : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [Nontrivial M],
  (∀ (N : LieSubmodule R L M), N ≠ ⊥ → N = ⊤) → LieModule.IsIrreducible R L M
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_subtype_le : ∀ {κ : Type u_4} {γ : Type u_5} [inst : AddCommGroup γ] [inst_1 : PartialOrder γ] [IsOrderedAddMonoid γ]
  [inst_3 : UniformSpace γ] [IsUniformAddGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ),
  (∀ (a : κ), 0 ≤ f a) → Summable f → ∑' (b : ↑β), f ↑b ≤ ∑' (a : κ), f a
-- Lean.Elab.InfoTree.Types
Lean.Elab.instReprDocElabKind : Repr Lean.Elab.DocElabKind
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.coconeMorphism_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.colimit.coconeMorphism c).hom = CategoryTheory.Limits.colimit.desc F c
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.eq_def : ∀ {α : Type u_1} {β : Type u_2} (node : Lean.PersistentHashMap.Node α β),
  node.measure =
    match node with
    | Lean.PersistentHashMap.Node.entries es => Lean.PersistentHashMap.Node.measure.measureEntries✝ es 0
    | Lean.PersistentHashMap.Node.collision ks vals h => vals.size
-- Mathlib.RingTheory.RingHom.Finite
RingHom.finite_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange @RingHom.Finite
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- **Alias** of `HasFDerivAt.finsetProd`. -/
HasFDerivAt.finset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasFDerivAt (g i) (g' i) x) →
    HasFDerivAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
-- Mathlib.Data.List.Rotate
List.rotate'_eq_drop_append_take : ∀ {α : Type u} {l : List α} {n : ℕ}, n ≤ l.length → l.rotate' n = List.drop n l ++ List.take n l
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff''ₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_injOn_Icc : ∀ {a b : ℝ}, b - a < 2 * Real.pi → Set.InjOn (⇑Circle.exp) (Set.Icc a b)
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- The special adjoint functor theorem: if `F : C ⥤ D` preserves colimits and `C` is cocomplete,
well-copowered and has a small separating set, then `F` has a right adjoint.
 -/
CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [CategoryTheory.Limits.HasColimits C] [CategoryTheory.WellPowered.{v, v, u} Cᵒᵖ] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{v, v, u} P],
  P.IsSeparating → ∀ (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F], F.IsLeftAdjoint
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.go.eq_def : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (i : ℕ) (a : i ≤ n),
  Array.ofFn.go✝ f acc i a =
    match i, a with
    | i.succ, h =>
      have w := ⋯;
      Array.ofFn.go✝ f (acc.push (f ⟨n - i - 1, w⟩)) i ⋯
    | 0, x => acc
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.span_gramSchmidt_Iic : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (c : ι), Submodule.span 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f '' Set.Iic c) = Submodule.span 𝕜 (f '' Set.Iic c)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inr_desc_whiskerRight_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) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Q ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hP.desc h k w) Q) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight k Q) h_1
-- Lean.Language.Lean.Types
/-- First command task (there is always at least a terminal command).  -/
Lean.Language.Lean.HeaderProcessedState.firstCmdSnap : Lean.Language.Lean.HeaderProcessedState → Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.homEquiv_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C}
  (f : W ⟶ t.pt), h.homEquiv f = (t.extend f).π
-- Mathlib.Order.Interval.Basic
Interval.coe_coe : ∀ {α : Type u_1} [inst : PartialOrder α] (s : NonemptyInterval α), ↑↑s = ↑s
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.ne_univ : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [NonLindelofSpace X], IsLindelof s → s ≠ Set.univ
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Sheaf.extend_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {ι : Type u_1} {B : ι → TopologicalSpace.Opens ↑X}
  (F : TopCat.Presheaf C X) (F' : TopCat.Sheaf C X) (h : TopologicalSpace.Opens.IsBasis (Set.range B))
  (α : (CategoryTheory.inducedFunctor B).op.comp F ⟶ (CategoryTheory.inducedFunctor B).op.comp F'.obj) (i : ι),
  ((TopCat.Sheaf.restrictHomEquivHom F F' h) α).app (Opposite.op (B i)) = α.app (Opposite.op i)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- A structure extending open partial homeomorphisms, defining a local trivialization of a
projection `proj : Z → B` with fiber `F`, as an open partial homeomorphism between `Z` and `B × F`
defined between two sets of the form `proj ⁻¹' baseSet` and `baseSet × F`, acting trivially on the
first coordinate.
 -/
Bundle.Trivialization : {B : Type u_1} →
  (F : Type u_2) →
    {Z : Type u_4} →
      [TopologicalSpace B] → [TopologicalSpace F] → [TopologicalSpace Z] → (Z → B) → Type (max (max u_1 u_2) u_4)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_eq_singleton_of_irreducible : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  Irreducible a → ∃ b, Associated a b ∧ UniqueFactorizationMonoid.factors a = {b}
-- Lean.Util.Trace
Lean.ExceptToTraceResult.mk : {ε α : Type} → (Except ε α → Lean.TraceResult) → Lean.ExceptToTraceResult ε α