mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.IsSolvable.mk : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {k : ℕ},
  LieAlgebra.derivedSeries R L k = ⊥ → LieAlgebra.IsSolvable L
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to negative infinity along a nontrivial filter `l`, then
`fun x ↦ f x / r` tends to negative infinity if and only if `0 < r`.  -/
Filter.tendsto_div_const_atBot_iff_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atBot → (Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ 0 < r)
-- Std.Data.DTreeMap.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.DTreeMap.Equiv : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → Prop
-- Mathlib.RingTheory.PowerBasis
/-- `pb.liftEquiv` states that roots of the minimal polynomial of `pb.gen` correspond to
maps sending `pb.gen` to that root.

This is the bundled equiv version of `PowerBasis.lift`.
If the codomain of the `AlgHom`s is an integral domain, then the roots form a multiset,
see `liftEquiv'` for the corresponding statement.
 -/
PowerBasis.liftEquiv : {S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra A S] →
          {S' : Type u_7} →
            [inst_3 : Ring S'] →
              [inst_4 : Algebra A S'] →
                (pb : PowerBasis A S) → (S →ₐ[A] S') ≃ { y // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsGT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ico c a → Set.Icc c a ∈ nhdsWithin b (Set.Ioi b)
-- Lean.Util.Sorry
Lean.Declaration.hasNonSyntheticSorry : Lean.Declaration → Bool
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.node.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (cs : Array (Lean.PersistentArrayNode α)),
  sizeOf (Lean.PersistentArrayNode.node cs) = 1 + sizeOf cs
-- Mathlib.Order.Filter.Extr
IsExtrFilter.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter f l a → ∀ {g : β → γ}, Monotone g → IsExtrFilter (g ∘ f) l a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeHomEquiv_comp_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} {I : Type u}
  (f : SheafOfModules.free I ⟶ M) (p : M ⟶ N) (i : I),
  N.freeHomEquiv (CategoryTheory.CategoryStruct.comp f p) i = SheafOfModules.sectionsMap p (M.freeHomEquiv f i)
-- Init.Data.SInt.Lemmas
UInt8.toInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt8 = OfNat.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_iInf : ∀ {ι : Sort u_1} {V : Type u} [Nonempty ι] {s : ι → SimpleGraph V} (v : V),
  (⨅ i, s i).neighborSet v = ⋂ i, (s i).neighborSet v
-- Init.Data.Float.Float32
instLEFloat32 : LE Float32
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
eq_zero_of_ne_zero_of_mul_right_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x y : M₀} [NoZeroDivisors M₀], x ≠ 0 → y * x = 0 → y = 0
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult : Type
-- Lean.Elab.DefView
Lean.Elab.DefView.mk.inj : ∀ {kind : Lean.Elab.DefKind} {ref headerRef : Lean.Syntax} {modifiers : Lean.Elab.Modifiers}
  {declId binders : Lean.Syntax} {type? : Option Lean.Syntax} {value : Lean.Syntax}
  {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)}
  {headerSnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot))}
  {deriving? : Option (Array Lean.Syntax)} {kind_1 : Lean.Elab.DefKind} {ref_1 headerRef_1 : Lean.Syntax}
  {modifiers_1 : Lean.Elab.Modifiers} {declId_1 binders_1 : Lean.Syntax} {type?_1 : Option Lean.Syntax}
  {value_1 : Lean.Syntax} {docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)}
  {headerSnap?_1 : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot))}
  {deriving?_1 : Option (Array Lean.Syntax)},
  { kind := kind, ref := ref, headerRef := headerRef, modifiers := modifiers, declId := declId, binders := binders,
        type? := type?, value := value, docString? := docString?, headerSnap? := headerSnap?, deriving? := deriving? } =
      { kind := kind_1, ref := ref_1, headerRef := headerRef_1, modifiers := modifiers_1, declId := declId_1,
        binders := binders_1, type? := type?_1, value := value_1, docString? := docString?_1,
        headerSnap? := headerSnap?_1, deriving? := deriving?_1 } →
    kind = kind_1 ∧
      ref = ref_1 ∧
        headerRef = headerRef_1 ∧
          modifiers = modifiers_1 ∧
            declId = declId_1 ∧
              binders = binders_1 ∧
                type? = type?_1 ∧
                  value = value_1 ∧ docString? = docString?_1 ∧ headerSnap? = headerSnap?_1 ∧ deriving? = deriving?_1
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.isometry_comap_mkMetric : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (m : ENNReal → ENNReal) {f : X → Y},
  Isometry f →
    Monotone m ∨ Function.Surjective f →
      (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.mkMetric m) =
        MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.Order.WithBot
WithTop.coe_max : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), ↑(max a b) = max ↑a ↑b
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- The star-subalgebra of polynomials.  -/
BoundedContinuousFunction.charPoly : {V : Type u_1} →
  {W : Type u_2} →
    [inst : AddCommGroup V] →
      [inst_1 : Module ℝ V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : AddCommGroup W] →
            [inst_4 : Module ℝ W] →
              [inst_5 : TopologicalSpace W] →
                {e : AddChar ℝ Circle} →
                  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} →
                    Continuous ⇑e → (Continuous fun p => (L p.1) p.2) → StarSubalgebra ℂ (BoundedContinuousFunction V ℂ)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Ioc_iff : ∀ {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ b₁ → (Finset.Icc a₁ b₁ ⊆ Finset.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂)
-- Mathlib.Algebra.Group.End
AddAut.zero_apply : ∀ (M : Type u_2) [inst : Add M] (m : M), 0 m = m
-- Mathlib.Topology.Algebra.Module.LocallyConvex
/-- Convex subsets of locally convex spaces are locally path-connected.  -/
Convex.locallyPathConnectedSpace : ∀ (E : Type u_2) [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {S : Set E}, Convex ℝ S → LocallyPathConnectedSpace ↑S
-- Init.Data.List.Lemmas
List.foldr_map : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {l : List α₁} {init : β},
  List.foldr g init (List.map f l) = List.foldr (fun x y => g (f x) y) init l
-- Lean.Compiler.IR.Basic
Lean.IR.instReprJoinPointId.repr : Lean.IR.JoinPointId → ℕ → Std.Format
-- Mathlib.Data.ENNReal.Basic
ENNReal.range_coe : Set.range ENNReal.ofNNReal = {⊤}ᶜ
-- Init.Prelude
/-- Lifts a proposition or type to a higher universe level.

`PLift α` wraps a proof or value of type `α`. The resulting type is in the next largest universe
after that of `α`. In particular, propositions become data.

The related type `ULift` can be used to lift a non-proposition type by any number of levels.

Examples:
 * `(False : Prop)`
 * `(PLift False : Type)`
 * `([.up (by trivial), .up (by simp), .up (by decide)] : List (PLift True))`
 * `(Nat : Type 0)`
 * `(PLift Nat : Type 1)`
 -/
PLift : Sort u → Type u
-- Batteries.Data.String.Lemmas
String.posOf_eq : ∀ (s : String) (c : Char), String.Legacy.posOf s c = String.Legacy.find s fun x => x == c
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) (x : F),
  (p.comp f) x = p (f x)
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure.eq_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C) (x : ℕ),
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f x =
    match x with
    | 0 => ⟨ULift.{v, w} α, f ∘ ULift.down⟩
    | n.succ =>
      ⟨CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep✝ (n + 1) fun m x =>
          CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f m,
        CategoryTheory.IsCofiltered.CofilteredClosureSmall.inductiveStepRealization✝ (n + 1) fun m x =>
          CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f m⟩
-- Mathlib.Order.Filter.Basic
/-- Weaker version of `Filter.biInter_mem` that assumes `Subsingleton β` rather than `Finite β`.  -/
Filter.biInter_mem' : ∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β},
  is.Subsingleton → (⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Given a homology map data for a morphism `φ`, this is the induced homology
map data for `-φ`.  -/
CategoryTheory.ShortComplex.HomologyMapData.neg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.HomologyMapData (-φ) h₁ h₂
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.chunkedBody.sizeOf_spec : ∀ (ext : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)) (remaining : ℕ),
  sizeOf (Std.Http.Protocol.H1.Reader.BodyState.chunkedBody ext remaining) = 1 + sizeOf ext + sizeOf remaining
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∩ t₂)[k]? = none
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.liesOver_span_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [NoZeroDivisors R]
  [Ring.KrullDimLE 1 R] [inst_4 : Algebra R S] {P : Ideal S} {p : R},
  P ≠ ⊤ → Prime p → (P.LiesOver (Ideal.span {p}) ↔ (algebraMap R S) p ∈ P)
-- Std.Sync.CancellationToken
Std.CancellationReason.cancel.sizeOf_spec : sizeOf Std.CancellationReason.cancel = 1
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- We enrich the existing function `toAlgHom` with the structure of a `MonoidHom`, to produce a
bundled function that we now call `toEnd`.  -/
GradedAlgHom.toEnd : {R : Type u_1} →
  {A : Type u_6} →
    {ι : Type u_10} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] → {𝒜 : ι → Submodule R A} → [inst_5 : GradedAlgebra 𝒜] → (𝒜 →ₐᵍ[R] 𝒜) →* A →ₐ[R] A
-- Mathlib.Data.Fintype.Sets
Set.toFinset_subset_toFinset : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s.toFinset ⊆ t.toFinset ↔ s ⊆ t
-- Mathlib.Algebra.Order.Star.Basic
star_right_conjugate_le_conjugate : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a b : R}, a ≤ b → ∀ (c : R), c * a * star c ≤ c * b * star c
-- Init.Data.String.Iterator
/-- Returns an iterator into the underlying string, at the substring's starting position. The ending
position is discarded, so the iterator alone cannot be used to determine whether its current
position is within the original substring.
 -/
Substring.Raw.toLegacyIterator : Substring.Raw → String.Legacy.Iterator
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_nsmul_const : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddMonoid G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ), f (n • a) = f 0 + n • b
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.comp_image : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : X.Opens) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor (CategoryTheory.CategoryStruct.comp f g)).obj U =
    (AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)
-- Mathlib.Algebra.Ring.Hom.Defs
AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero : ∀ {α : Type u_2} {β : Type u_3} [inst : CommRing α] [inst_1 : IsDomain α] [inst_2 : CommRing β] (f : β →+ α)
  (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 ≠ 0) (h_one : f 1 = 1),
  ⇑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = ⇑f
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.isZeroAt_iff_exists_SL2Z : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ},
  IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range →
    (c.IsZeroAt f k ↔
      ∃ γ,
        (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c ∧
          UpperHalfPlane.IsZeroAtImInfty (SlashAction.map k γ f))
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.WithTerminal J → Sort u_2) (a : J)
  (h_1 : (a : J) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of a with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_1 a
-- Mathlib.Data.Fintype.Defs
Fintype.decidableBijectiveFintype : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [Fintype α] → [Fintype β] → DecidablePred Function.Bijective
-- Mathlib.SetTheory.ZFC.PSet
PSet.mk.inj : ∀ {α : Type u} {A : α → PSet.{u}} {α_1 : Type u} {A_1 : α_1 → PSet.{u}},
  PSet.mk α A = PSet.mk α_1 A_1 → α = α_1 ∧ A ≍ A_1
-- Init.Meta.Defs
/-- Syntax that represents a quoted name literal that begins with a back-tick.
 -/
Lean.Syntax.NameLit : Type
-- Mathlib.Data.Real.ConjExponents
/-- **Alias** of the reverse direction of `ENNReal.holderTriple_coe_iff`. -/
NNReal.HolderTriple.coe_ennreal : ∀ {p q r : NNReal}, r ≠ 0 → p.HolderTriple q r → (↑p).HolderTriple ↑q ↑r
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.MonicDegreeEq.map_coe : ∀ {R : Type u} {S : Type v} {n : ℕ} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial.MonicDegreeEq R n)
  (f : R →+* S), ↑(p.map f) = Polynomial.map f ↑p
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.succ_mul_binomial : ∀ {α : Type u_1} {f : α → ℕ} {a b : α} [inst : DecidableEq α],
  a ≠ b →
    (f a + f b).succ * Nat.multinomial {a, b} f = (f a).succ * Nat.multinomial {a, b} (Function.update f a (f a).succ)
-- Mathlib.Data.ENat.Basic
ENat.lt_add_left : ∀ {n k : ℕ∞}, n ≠ ⊤ → 0 < k → n < k + n
-- Mathlib.RingTheory.IntegralDomain
card_nthRoots_subgroup_units : ∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G] [inst_3 : Fintype G]
  [inst_4 : DecidableEq G] (f : G →* R),
  Function.Injective ⇑f → ∀ {n : ℕ}, 0 < n → ∀ (g₀ : G), {g | g ^ n = g₀}.card ≤ (Polynomial.nthRoots n (f g₀)).card
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {km : α}, t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α}, (Std.ExtHashMap.map f m).getKey? k = m.getKey? k
-- Mathlib.Data.Int.Init
Int.inductionOn'.neg.eq_def : ∀ {motive : ℤ → Sort u_1} (b : ℤ) (zero : motive b) (pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)) (n : ℕ),
  Int.inductionOn'.neg b zero pred n =
    match n with
    | 0 => pred b ⋯ zero
    | n.succ => cast ⋯ (pred (b + Int.negSucc n) ⋯ (Int.inductionOn'.neg b zero pred n))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.instInhabitedΛ' : {Γ : Type u_1} → {Λ : Type u_2} → [Inhabited Λ] → Inhabited (Turing.TM0to1.Λ' Γ Λ)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.divMaxPow_base_mul : ∀ {p : ℕ}, p ≠ 0 → ∀ (n : ℕ), (p * n).divMaxPow p = n.divMaxPow p
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Given a diagram `{ Dᵢ }` of schemes and an open `U ⊆ Dᵢ`,
the preimage of `U ⊆ Dᵢ` under the map `lim Dᵢ ⟶ Dᵢ` is the limit of `{ Dⱼᵢ⁻¹ U }_{j ≤ i}`.
This is the underlying cone, and it is limiting as witnessed by `isLimitOpensCone` below.  -/
AlgebraicGeometry.opensCone : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) →
      CategoryTheory.Limits.Cone D →
        (i : I) → (U : (D.obj i).Opens) → CategoryTheory.Limits.Cone (AlgebraicGeometry.opensDiagram D i U)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Each function of an equicontinuous family is continuous.  -/
Equicontinuous.continuous : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
  Equicontinuous F → ∀ (i : ι), Continuous (F i)
-- Mathlib.Analysis.Convex.Segment
openSegment_translate_preimage : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a b c : E), (fun x => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumAssoc_apply : ∀ {U : Type u_1} {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
  (a : (V ⊕ W) ⊕ U), SimpleGraph.Iso.sumAssoc a = Sum.elim (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl)) (Sum.inr ∘ Sum.inr) a
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcomp₁_obj_left_obj : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F))
  (X_1 : D), ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).left.obj X_1 = X.left.obj (G.obj X_1)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
expUnitary_argSelfAdjoint : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : ↥(unitary A)},
  ‖↑u - 1‖ < 2 → selfAdjoint.expUnitary (Unitary.argSelfAdjoint u) = u
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.compLeft.eq_1 : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul α] [inst_1 : Mul β] (f : α →ₙ* β) (I : Type u_7),
  f.compLeft I = { toFun := fun h => ⇑f ∘ h, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.subtype_injective : ∀ {M : Type u_1} {A : Type u_3} [inst : AddZeroClass M] [inst_1 : SetLike A M] [hA : AddSubmonoidClass A M] (S' : A),
  Function.Injective ⇑(AddSubmonoidClass.subtype S')
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.inv_hom_id_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X) ((e.hom.hom n).app X) =
    CategoryTheory.CategoryStruct.id ((G.functor n).obj X)
-- Mathlib.Data.Finset.Max
Finset.lt_min'_iff : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α}, x < s.min' H ↔ ∀ y ∈ s, x < y
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.homLinearEquiv_apply : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {S : Type u_1} [inst_1 : Semiring S] [inst_2 : Module S ↑N]
  [inst_3 : SMulCommClass R S ↑N] (a : M ⟶ N), ModuleCat.homLinearEquiv a = ModuleCat.homAddEquiv.toFun a
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_zsmul : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ), f (x + n • a) = f x + n • b
-- Mathlib.Data.Vector.Snoc
/-- Define `C v` by *reverse* case analysis, i.e. by handling the cases `nil` and `xs.snoc x`
separately  -/
List.Vector.revCasesOn : {α : Type u_1} →
  {C : {n : ℕ} → List.Vector α n → Sort u_5} →
    {n : ℕ} →
      (v : List.Vector α n) → C List.Vector.nil → ({n : ℕ} → (xs : List.Vector α n) → (x : α) → C (xs.snoc x)) → C v
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (X : C),
  (CategoryTheory.Functor.CommShift.isoZero F A).hom.app X =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
      ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X))
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.exists_isAtom : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {S : Finset G},
  K < 1 → S.Nonempty → ∃ A, Finset.IsAtom✝ K S A
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- Transport a `HasLimitsOfShape` instance across an equivalence.  -/
CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (E : CategoryTheory.Functor D C) [E.IsEquivalence]
  [CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J D
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_ofLp : ∀ (p : ENNReal) {V : Type u_4} (x : WithLp p V), WithLp.toLp p x.ofLp = x
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.const_smul : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'} {f' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt% f z f' → ∀ (s : 𝕜), HasMFDerivAt% (s • f) z (s • f')
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubsetResult.exact.sizeOf_spec : sizeOf Lean.Grind.AC.SubsetResult.exact = 1
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_symm_id : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (p : ENNReal),
  (Matrix.toLpLin p p).symm LinearMap.id = 1