mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₂_obj_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (E : Type u_7) [inst_4 : CategoryTheory.Category.{v_7, u_7} E]
  (F₁ : CategoryTheory.Functor C₁ D₁) {X Y : CategoryTheory.Functor C₂ D₂} (φ : X ⟶ Y)
  (X_1 : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) (X_2 : C₁) (c : C₂),
  (((((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₁).map φ).app X_1).app X_2).app c =
    (X_1.obj (F₁.obj X_2)).map (φ.app c)
-- Mathlib.RingTheory.Ideal.Height
/-- In a nontrivial commutative ring `R`, the supremum of heights of all maximal ideals is
equal to the Krull dimension of `R`.  -/
Ideal.sup_isMaximal_height_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R], ↑(⨆ I, ⨆ (_ : I.IsMaximal), I.height) = ringKrullDim R
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_bmod_self : ∀ (a : ℤ) (b : ℕ), (a + -↑b).bmod b = a.bmod b
-- Mathlib.Order.Minimal
maximal_mem_Icc : ∀ {α : Type u_2} {x : α} [inst : PartialOrder α] {a b : α}, b ≤ a → (Maximal (fun x => x ∈ Set.Icc b a) x ↔ x = a)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instConcreteCategoryAddHomCarrier : CategoryTheory.ConcreteCategory AddSemigrp fun x1 x2 => ↑x1 →ₙ+ ↑x2
-- Mathlib.Topology.Order.IntermediateValue
ordered_connected_space : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α], PreconnectedSpace α
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- A measure `μ` has temperate growth if there is an `n : ℕ` such that `(1 + ‖x‖) ^ (- n)` is
`μ`-integrable.  -/
MeasureTheory.Measure.HasTemperateGrowth : {E : Type u_5} → [NormedAddCommGroup E] → [inst : MeasurableSpace E] → MeasureTheory.Measure E → Prop
-- Mathlib.Topology.Category.TopCat.ULift
/-- The `ULift` functor on categories of topological spaces is fully faithful.  -/
TopCat.uliftFunctorFullyFaithful : TopCat.uliftFunctor.FullyFaithful
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.algebraMonoidAlgebra.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : CommMonoid M] [inst_1 : CommSemiring R] [inst_2 : CommSemiring S]
  [inst_3 : Algebra R S], MonoidAlgebra.algebraMonoidAlgebra = (MonoidAlgebra.mapRingHom M (algebraMap R S)).toAlgebra
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.toExtendScalars_toRingHom_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (x : P.Ring), P.toExtendScalars.toRingHom x = x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.head?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Min α] [inst_1 : LE α]
  [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqCmp cmp],
  t.toList.head? = t.min?
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.bounds_nonempty : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F),
  ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_left : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F}, P 2 = 0 → WeierstrassCurve.Jacobian.addU P Q = 0
-- Mathlib.GroupTheory.ArchimedeanDensely
instUniqueOrderAddMonoidIsoInt : Unique (ℤ ≃+o ℤ)
-- Mathlib.Data.Finset.Lattice.Fold
List.foldr_sup_eq_sup_toFinset : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (l : List α),
  List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ l = l.toFinset.sup id
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `f : A ⟶ B` is a ring homomorphism, the corresponding arrow is isomorphic
to the arrow of the morphism induced on global sections by the map on prime spectra.  -/
AlgebraicGeometry.arrowIsoΓSpecOfIsAffine : {A B : CommRingCat} →
  (f : A ⟶ B) →
    CategoryTheory.Arrow.mk f ≅
      CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f))
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.mem_inv_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : AddMonoid A] [inst_1 : GroupWithZero G₀] [inst_2 : DistribMulAction G₀ A]
  {a : G₀}, a ≠ 0 → ∀ (S : AddSubmonoid A) (x : A), x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.Algebra.Algebra.Unitization
/-- **Alias** of the reverse direction of `Unitization.isIdempotentElem_inr_iff`. -/
Unitization.IsIdempotentElem.inr : ∀ (R : Type u_1) {A : Type u_2} [inst : MulZeroClass R] [inst_1 : AddZeroClass A] [inst_2 : Mul A]
  [inst_3 : SMulWithZero R A] {a : A}, IsIdempotentElem a → IsIdempotentElem ↑a
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The essential image of a property of objects by a functor.  -/
CategoryTheory.ObjectProperty.map : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.ObjectProperty C → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D
-- Std.Data.DTreeMap.Internal.Balancing
/-- Slower version of `balance` which can be used in the complete absence of balancing information
but still assumes that the preconditions of `balance` are satisfied
(otherwise panics).
 -/
Std.DTreeMap.Internal.Impl.balance! : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_iff : ∀ {α : Type u_1} [inst : LT α] {a : α}, ¬Order.IsSuccPrelimit a ↔ ∃ b, b ⋖ a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT?_eq_getEntryGT?_reverse : ∀ {α : Type u} {β : α → Type v} [o : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getEntryLT? k t = Std.DTreeMap.Internal.Impl.getEntryGT? k t.reverse
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.startsWith_prop_eq_false_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String},
  s.startsWith P = false ↔ ∀ (h : s.startPos ≠ s.endPos), ¬P (s.startPos.get h)
-- Lean.Environment
/-- `.olean` + `.olean.server` (optional) + `.olean.private` (optional).  -/
_private.Lean.Environment.0.Lean.ImportedModule.parts : Lean.ImportedModule✝ → Array (Lean.ModuleData × Lean.CompactedRegion)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGT?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getEntryGT? k t₁ = Std.DTreeMap.Internal.Impl.getEntryGT? k t₂
-- Mathlib.Algebra.Category.Grp.Adjunctions
instIsRightAdjointCommGrpCatCommMonCatUnits : CommMonCat.units.IsRightAdjoint
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Fold a function on the values from left to right (in increasing order).  -/
RBTree.RBSet.foldl : {σ : Sort u_1} → {α : Type u_2} → {cmp : α → α → Ordering} → (σ → α → σ) → σ → RBTree.RBSet α cmp → σ
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuous : ∀ {𝕜 : 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), Continuous ↑I
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.homCongr_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Iso.refl X).homCongr (CategoryTheory.Iso.refl Y)) f = f
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ordHom_of_isUnit : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {U : X.Opens} [inst_2 : Nonempty ↥↑U]
  {f : ↑(X.presheaf.obj (Opposite.op U))},
  IsUnit f →
    ∀ {x : ↥X} (hx : Order.coheight x = 1),
      x ∈ U →
        (AlgebraicGeometry.Scheme.ordHom x hx) ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f) = 1
-- Mathlib.Logic.Godel.GodelBetaFunction
_private.Mathlib.Logic.Godel.GodelBetaFunction.0.Nat.supOfSeq : {m : ℕ} → (Fin m → ℕ) → ℕ
-- Mathlib.Computability.TuringMachine.Computable
/-- A Turing machine + a proof it outputs `f`.  -/
Turing.TM2Computable : {α β αΓ βΓ : Type} → (α → List αΓ) → (β → List βΓ) → (α → β) → Type 1
-- Mathlib.RingTheory.WittVector.StructurePolynomial
/-- `wittStructureInt Φ` is a family of polynomials `ℕ → MvPolynomial (idx × ℕ) ℤ`
that are uniquely characterised by the property that
```
bind₁ (wittStructureInt p Φ) (wittPolynomial p ℤ n) =
bind₁ (fun i ↦ (rename (prod.mk i) (wittPolynomial p ℤ n))) Φ
```
In other words: evaluating the `n`-th Witt polynomial on the family `wittStructureInt Φ`
is the same as evaluating `Φ` on the (appropriately renamed) `n`-th Witt polynomials.

See `wittStructureInt_prop` for this property,
and `wittStructureInt_existsUnique` for the fact that `wittStructureInt`
gives the unique family of polynomials with this property.  -/
wittStructureInt : (p : ℕ) → {idx : Type u_2} → [hp : Fact (Nat.Prime p)] → MvPolynomial idx ℤ → ℕ → MvPolynomial (idx × ℕ) ℤ
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mk.congr_simp : ∀ {R : Type u_3} [inst : CommSemiring R] {A : Type u_4} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_5} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (toAlgHom toAlgHom_1 : A →ₐ[R] B) (e_toAlgHom : toAlgHom = toAlgHom_1)
  (cont : Continuous (↑↑toAlgHom.toRingHom).toFun),
  { toAlgHom := toAlgHom, cont := cont } = { toAlgHom := toAlgHom_1, cont := ⋯ }
-- Mathlib.Algebra.Ring.Defs
/-- A `NonUnitalSemiring` which `IsMulCommutative` is a `NonUnitalCommSemiring`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instNonUnitalCommSemiring : {R : Type v} → [inst : NonUnitalSemiring R] → [IsMulCommutative R] → NonUnitalCommSemiring R
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocSemiring β] → [IsTopologicalSemiring β] → NonUnitalNonAssocSemiring C(α, β)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.turanGraph.eq_1 : ∀ (n r : ℕ), SimpleGraph.turanGraph n r = { Adj := fun v w => ↑v % r ≠ ↑w % r, symm := ⋯, loopless := ⋯ }
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformRight_snd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformRight e x).2 = x.2 ∩ (-e +ᵥ x.2)
-- Mathlib.Computability.Partrec
Computable.nat_rec : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → ℕ} {g : α → σ}
  {h : α → ℕ × σ → σ},
  Computable f → Computable g → Computable₂ h → Computable fun a => Nat.rec (g a) (fun y IH => h a (y, IH)) (f a)
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.mul_def : ∀ (x x_1 : ℝ),
  Real.mul✝ x x_1 =
    match x, x_1 with
    | { cauchy := a }, { cauchy := b } => { cauchy := a * b }
-- Mathlib.AlgebraicTopology.CechNerve
/-- The morphism between augmented Čech nerve associated to a morphism of arrows.  -/
CategoryTheory.Arrow.mapAugmentedCechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] →
          (f ⟶ g) → (f.augmentedCechNerve ⟶ g.augmentedCechNerve)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If an additive group satisfies the universal property of an additive free group with respect to
a given type, then it is free. Here, the universal property is expressed as in `IsFreeAddGroup.lift`
and its properties.  -/
IsFreeAddGroup.ofLift : ∀ {G : Type u} [inst : AddGroup G] (X : Type u) (of : X → G)
  (lift : {H : Type u} → [inst_1 : AddGroup H] → (X → H) ≃ (G →+ H)),
  (∀ {H : Type u} [inst_1 : AddGroup H] (f : X → H) (a : X), (lift f) (of a) = f a) → IsFreeAddGroup G
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The target open subscheme of a partial isomorphism.  -/
AlgebraicGeometry.Scheme.PartialIso.target : {X Y : AlgebraicGeometry.Scheme} → X.PartialIso Y → Y.Opens
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l → (Std.DHashMap.Const.ofList l).size = l.length
-- Mathlib.Topology.Basic
TopologicalSpace.ext_iff : ∀ {X : Type u} {t t' : TopologicalSpace X}, t = t' ↔ ∀ (s : Set X), IsOpen s ↔ IsOpen s
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_le_one : ∀ {c : Cardinal.{u}}, Cardinal.toENat c ≤ 1 ↔ c ≤ 1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.nonempty : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [Nonempty m] [Nonempty n] [Nontrivial α], Nontrivial (Matrix m n α)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Let `C(G, A)` denote the complex of inhomogeneous cochains of `A : Rep k G`. This lemma
says `d₂₃` gives a simpler expression for the 2nd differential: that is, the following
square commutes:
```
      C²(G, A) ----d 2 3----> C³(G, A)
        |                         |
        |                         |
        |                         |
        v                         v
  Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)
```
where the vertical arrows are `cochainsIso₂` and `cochainsIso₃` respectively.
 -/
groupCohomology.comp_d₂₃_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).hom (groupCohomology.d₂₃ A) =
    CategoryTheory.CategoryStruct.comp ((groupCohomology.inhomogeneousCochains A).d 2 3)
      (groupCohomology.cochainsIso₃ A).hom
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  (φ' : S' ⟶ R) {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
  (ModuleCat.Hom.hom ((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f))
      (CommRingCat.KaehlerDifferential.d x) =
    CommRingCat.KaehlerDifferential.d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ : Std.DTreeMap α β cmp} {l : List ((a : α) × β a)},
  (t₁.insertMany l).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) t₁ l)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanModuleHierarchyImportsParams.toJson : Lean.Lsp.LeanModuleHierarchyImportsParams → Lean.Json
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.balance' : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, l.Sized → r.Sized → (l.balance' x r).Sized
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_zero_equiv_symm_apply : ∀ (p : Fin 0 → Type u) (τ : Type u) (a : Function.FromTypes p τ), (Function.fromTypes_zero_equiv p τ).symm a = a
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The point of a cone is a lower bound.  -/
Preorder.conePt_mem_lowerBounds : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F), c.pt ∈ lowerBounds (Set.range F.obj)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing `UniformSpace` instance on `E`).  -/
AddGroupSeminorm.toSeminormedAddCommGroup : {E : Type u_5} → [inst : AddCommGroup E] → AddGroupSeminorm E → SeminormedAddCommGroup E
-- Mathlib.Analysis.Calculus.FDeriv.Comp
fderiv_comp : ∀ {𝕜 : 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} (x : E) {g : F → G},
  DifferentiableAt 𝕜 g (f x) → DifferentiableAt 𝕜 f x → fderiv 𝕜 (g ∘ f) x = fderiv 𝕜 g (f x) ∘SL fderiv 𝕜 f x
-- Lean.Data.KVMap
Lean.KVMap.instValueString : Lean.KVMap.Value String
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` iff the function `swap 𝓕 : X → ι → α` is
continuous at `x₀` *when `ι → α` is equipped with the topology of uniform convergence*. This is
very useful for developing the equicontinuity API, but it should not be used directly for other
purposes.  -/
equicontinuousAt_iff_continuousAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X},
  EquicontinuousAt F x₀ ↔ ContinuousAt (⇑UniformFun.ofFun ∘ Function.swap F) x₀
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instZero : {𝕜 : Type u_1} → [inst : Zero 𝕜] → [inst_1 : PseudoMetricSpace 𝕜] → Zero ↑(Metric.ball 0 1)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Local notation for the positive elements of a type `α`.  -/
_private.Mathlib.Algebra.Order.GroupWithZero.Basic.0.«termα>0» : Lean.ParserDescr
-- Mathlib.Order.Filter.Pointwise
Filter.vaddCommClass_filter'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass (Filter α) β (Filter γ)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr : Inhabited Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.evaluation K C).obj k)) j)
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k).inv =
    (CategoryTheory.Limits.colimit.ι F j).app k
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- Assume that `f` is differentiable inside a convex set `s`, and that its derivative `f'` is
differentiable at a point `x`. Then, given two vectors `v` and `w` pointing inside `s`, one can
Taylor-expand to order two the function `f` on the segment `[x + h v, x + h (v + w)]`, giving a
bilinear estimate for `f (x + hv + hw) - f (x + hv)` in terms of `f' w` and of `f'' ⬝ w`, up to
`o(h^2)`.

This is a technical statement used to show that the second derivative is symmetric.  -/
Convex.taylor_approx_two_segment : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F},
      (∀ x ∈ interior s, HasFDerivAt f (f' x) x) →
        ∀ {x : E},
          x ∈ s →
            HasFDerivWithinAt f' f'' (interior s) x →
              ∀ {v w : E},
                x + v ∈ interior s →
                  x + v + w ∈ interior s →
                    (fun h =>
                        f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w -
                          (h ^ 2 / 2) • (f'' w) w) =o[nhdsWithin 0 (Set.Ioi 0)]
                      fun h => h ^ 2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.all_eq_true : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {p : (a : α) → β a → Bool},
  (↑m).WF → ((↑m).all p = true ↔ ∀ (a : α) (h : m.contains a = true), p a (m.get a h) = true)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_add_one : ∀ {f : Ordinal.{u} → Ordinal.{u}},
  Order.IsNormal f → ∀ (o : Ordinal.{u}), Ordinal.veblenWith f (o + 1) = Ordinal.deriv (Ordinal.veblenWith f o)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_filter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.DTreeMap.filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = false
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `P` is a submersive presentation of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural submersive presentation of `T ⊗[R] S` over `T`.  -/
Algebra.SubmersivePresentation.baseChange : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (T : Type u_1) →
                  [inst_4 : CommRing T] →
                    [inst_5 : Algebra R T] →
                      Algebra.SubmersivePresentation R S ι σ →
                        Algebra.SubmersivePresentation T (TensorProduct R T S) ι σ
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The localization map of a quotient module.  -/
Submodule.toLocalizedQuotient : {R : Type u_5} →
  {M : Type u_7} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (p : Submonoid R) → (M' : Submodule R M) → M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ Submodule.localized p M'
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- For a family of functions between (pseudo) metric spaces, a convenient way to prove
uniform equicontinuity is to show that all of the functions share a common *global* continuity
modulus.  -/
Metric.uniformEquicontinuous_of_continuity_modulus : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β] (b : ℝ → ℝ),
  Filter.Tendsto b (nhds 0) (nhds 0) →
    ∀ (F : ι → β → α), (∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)) → UniformEquicontinuous F
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.le_sup_of_le_right : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {l : Filter α} {f g h : α → β}, h ≤ᶠ[l] g → h ≤ᶠ[l] f ⊔ g
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State : Type
-- Aesop.Rule.Name
Aesop.BuilderName.noConfusionType : Sort v✝ → Aesop.BuilderName → Aesop.BuilderName → Sort v✝
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAt_iff : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat