mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_find?_of_gt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.gt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.find? (fun x => k x.fst == Ordering.eq) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        List.find? (fun x => k x.fst == Ordering.eq) r.toListModel
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.inr_comp_pushoutSymmetry_hom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushoutSymmetry f g).hom Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inl g f) Q
-- Mathlib.Dynamics.OmegaLimit
Flow.omegaLimit_omegaLimit : ∀ {τ : Type u_1} [inst : TopologicalSpace τ] [inst_1 : AddCommGroup τ] {α : Type u_2} [inst_2 : TopologicalSpace α]
  (f : Filter τ) (ϕ : Flow τ α) (s : Set α),
  (∀ (t : τ), Filter.Tendsto (fun x => t + x) f f) →
    omegaLimit f ϕ.toFun (omegaLimit f ϕ.toFun s) ⊆ omegaLimit f ϕ.toFun s
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqCtorInfo : BEq Lean.IR.CtorInfo
-- Init.Core
HasSubset.mk : {α : Type u} → (α → α → Prop) → HasSubset α
-- Mathlib.CategoryTheory.Preadditive.Projective.Internal
/-- An object `P : C` is *internally projective* if the functor `P ⟶[C] -` taking internal homs
out of `P` preserves epimorphisms.
 -/
CategoryTheory.isInternallyProjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.MonoidalClosed C] → CategoryTheory.ObjectProperty C
-- Mathlib.Data.Nat.Digits.Div
Nat.modEq_three_digits_sum : ∀ (n : ℕ), n ≡ (Nat.digits 10 n).sum [MOD 3]
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.instNontrivial : ∀ {α : Type u} [Nontrivial α], Nontrivial (Multiplicative α)
-- Mathlib.Algebra.Tropical.Basic
Tropical.instNontrivialWithTopOfZero : ∀ {R : Type u} [Zero R], Nontrivial (Tropical (WithTop R))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rcc_eq_none : ∀ {m n : ℤ} {i : ℕ}, (n + 1 - m).toNat ≤ i → (m...=n).toArray[i]? = none
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr_mul_r : ∀ {n : ℕ} (i j : ZMod n), DihedralGroup.sr i * DihedralGroup.r j = DihedralGroup.sr (i + j)
-- Mathlib.Algebra.Order.Star.Basic
/-- Every self-adjoint element is the difference of nonnegative elements.  -/
SelfAdjointDecompose.exists_nonneg_sub_nonneg : ∀ {R : Type u_3} {inst : AddGroup R} {inst_1 : Star R} {inst_2 : PartialOrder R} [self : SelfAdjointDecompose R]
  {a : R}, IsSelfAdjoint a → ∃ b c, 0 ≤ b ∧ 0 ≤ c ∧ a = b - c
-- Std.Data.ByteSlice
/-- The ending index of the region of interest (exclusive).
 -/
ByteSlice.stop : ByteSlice → ℕ
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.exists_coe_eq_v : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  (x : UniformSpace.Completion K), ∃ r, Valued.extensionValuation x = Valued.v r
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_comp_mul_left_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ) {b : ℝ},
  0 < b → ∫ (x : ℝ) in Set.Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Set.Ioi (b * a), g x
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The pullback along an epi that's preserved under pullbacks is faithful.

This "preserved under pullbacks" condition is automatically satisfied in abelian categories:
```
example [Abelian C] [Epi f] : (pullback f).Faithful := inferInstance
```
 -/
CategoryTheory.Over.faithful_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f]
  [∀ (Z : C) (g : Z ⟶ Y), CategoryTheory.Epi (CategoryTheory.Limits.pullback.fst g f)],
  (CategoryTheory.Over.pullback f).Faithful
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.IsStrictSegal.ext : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} [X.IsStrictSegal] {d : ℕ} {hd : { len := d + 1 }.len ≤ n + 1}
  {x y : X.obj (Opposite.op { obj := { len := d + 1 }, property := hd })},
  (∀ (i : Fin (d + 1)),
      (CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ hd).op))
          x =
        (CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ hd).op))
          y) →
    x = y
-- Mathlib.Algebra.Order.Field.Basic
div_neg_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_compl_eq_zero_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → (μ sᶜ = 0 ↔ μ s = 1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The right object of a structured arrow.  -/
CategoryTheory.StructuredArrow.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} → {T : CategoryTheory.Functor C D} → CategoryTheory.StructuredArrow S T → C
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instAlternativeGrindTacticM : Alternative Lean.Elab.Tactic.Grind.GrindTacticM
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKeyD_modify_eq_maxKeyD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {fallback : α},
  (Std.DTreeMap.Const.modify t k f).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of `f i` over `i ∈ {a}` equals `f a`.  -/
finprod_mem_singleton : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α}, ∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- When `[HasPullbacks C]`, `MonoOver A` has "intersections", functorial in both arguments.

As `MonoOver A` is only a preorder, this doesn't satisfy the axioms of `SemilatticeInf`,
but we reuse all the names from `SemilatticeInf` because they will be used to construct
`SemilatticeInf (Subobject A)` shortly.
 -/
CategoryTheory.MonoOver.inf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasPullbacks C] →
      {A : C} →
        CategoryTheory.Functor (CategoryTheory.MonoOver A)
          (CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.MonoOver A))
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Equivalence between Dyck words of semilength `n` and rooted binary trees with
`n` internal nodes.  -/
DyckWord.equivTreesOfNumNodesEq : (n : ℕ) → { p // p.semilength = n } ≃ ↥(BinaryTree.treesOfNumNodesEq n)
-- Init.Data.Repr
/-- Converts a natural number to a string that contains the its decimal representation as Unicode
superscript digit characters.

Examples:
 * `Nat.toSuperscriptString 0 = "⁰"`
 * `Nat.toSuperscriptString 35 = "³⁵"`
 -/
Nat.toSuperscriptString : ℕ → String
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  m.insertMany [] = m
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for Wikidata identifiers: it accepts `Q` followed by one or more digits.  -/
Mathlib.CrossRef.wikidataIdNoAntiquot : Lean.Parser.Parser
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.getAppNumArgsAux : Lean.Expr → ℕ → ℕ
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_of_equiv_fin : ∀ {α : Type u_3} {n : ℕ} (f : α ≃ Fin n), Nat.card α = n
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `smul_le_smul_of_nonneg_left` instead.  -/
PosSMulMono.smul_le_smul_of_nonneg_left : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  [self : PosSMulMono α β] ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, b₁ ≤ b₂ → a • b₁ ≤ a • b₂
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.facePairComplIso.congr_simp : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j),
  SSet.stdSimplex.facePairComplIso i j h = SSet.stdSimplex.facePairComplIso i j h
-- Mathlib.Algebra.Group.Action.Defs
AddDistribAddAction.mk : {M : Type u_9} →
  {N : Type u_10} →
    [inst : AddMonoid M] →
      [inst_1 : AddMonoid N] →
        [toAddAction : AddAction M N] →
          (∀ (r : M), r +ᵥ 0 = 0) → (∀ (r : M) (x y : N), r +ᵥ x + y = (r +ᵥ x) + (r +ᵥ y)) → AddDistribAddAction M N
-- Mathlib.CategoryTheory.EssentialImage
/-- Pre-composing by an essentially surjective functor doesn't change the essential image.  -/
CategoryTheory.Functor.essImage_comp_apply_of_essSurj : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.EssSurj] {X : E},
  (F.comp G).essImage X ↔ G.essImage X
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Swapping the first and second points in an oriented angle negates the sign of that angle.  -/
EuclideanGeometry.oangle_swap₁₂_sign : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), -(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₂ p₁ p₃).sign
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- Two simplices with the same points have the same centroid.  -/
Affine.Simplex.centroid_eq_of_range_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} {s₁ s₂ : Affine.Simplex k P n},
  Set.range s₁.points = Set.range s₂.points →
    Finset.centroid k Finset.univ s₁.points = Finset.centroid k Finset.univ s₂.points
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.LinExpr : Type
-- Mathlib.Data.Complex.Basic
Complex.re_surjective : Function.Surjective Complex.re
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.getKeyD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a fallback : α) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getKeyD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback =
    Std.DHashMap.Internal.AssocList.getKeyD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.Order.CompactlyGenerated.Basic
/-- See [Theorem 6.6][calugareanu].  -/
complementedLattice_of_sSup_atoms_eq_top : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α],
  sSup {a | IsAtom a} = ⊤ → ComplementedLattice α
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.match_1.eq_1 : ∀ (motive : Lean.Name → Lean.Name → Sort u_1) (h_1 : Unit → motive Lean.Name.anonymous Lean.Name.anonymous)
  (h_2 : (p₁ : Lean.Name) → (s₁ : String) → (p₂ : Lean.Name) → (s₂ : String) → motive (p₁.str s₁) (p₂.str s₂))
  (h_3 : (p₁ : Lean.Name) → (n₁ : ℕ) → (p₂ : Lean.Name) → (n₂ : ℕ) → motive (p₁.num n₁) (p₂.num n₂))
  (h_4 : (x x_1 : Lean.Name) → motive x x_1),
  (match Lean.Name.anonymous, Lean.Name.anonymous with
    | Lean.Name.anonymous, Lean.Name.anonymous => h_1 ()
    | p₁.str s₁, p₂.str s₂ => h_2 p₁ s₁ p₂ s₂
    | p₁.num n₁, p₂.num n₂ => h_3 p₁ n₁ p₂ n₂
    | x, x_1 => h_4 x x_1) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.eq_iSup_nat : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal),
  MeasureTheory.OuterMeasure.mkMetric' m = ⨆ n, MeasureTheory.OuterMeasure.mkMetric'.pre m (↑n)⁻¹
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true →
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter m₂ ⋯) k fallback =
          Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : CategoryTheory.LocallyDiscrete Cᵒᵖ} (f : X ⟶ Y)
  {X_1 Y_1 : CategoryTheory.Sheaf (J.over (Opposite.unop X.as)) A} (f_1 : X_1 ⟶ Y_1)
  (X_2 : (CategoryTheory.Over (Opposite.unop Y.as))ᵒᵖ),
  (((J.pseudofunctorOver A).map f).toFunctor.map f_1).hom.app X_2 =
    f_1.hom.app (Opposite.op ((CategoryTheory.Over.map f.as.unop).obj (Opposite.unop X_2)))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
CFC.rpow_le_rpow : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : ℝ},
  p ∈ Set.Icc 0 1 → ∀ {a b : A}, a ≤ b → a ^ p ≤ b ^ p
-- Mathlib.Topology.UniformSpace.Completion
/-- The pairs of Cauchy filters generated by a set.  -/
CauchyFilter.gen : {α : Type u} → [inst : UniformSpace α] → SetRel α α → SetRel (CauchyFilter α) (CauchyFilter α)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.one_le_norm_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]}, 1 ≤ ‖x‖ ↔ ‖x‖ = 1
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsSchemeTheoreticallyDominant g]
  [AlgebraicGeometry.QuasiCompact g] [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.IsSchemeTheoreticallyDominant (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.map_sConvexComb : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N]
  {f : M → N},
  Convexity.IsAffineMap R f →
    ∀ (s : Convexity.StdSimplex R M), f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map f s)
-- Init.CbvSimproc
Lean.Parser.«command__Builtin_cbv_simproc____(_):=_» : Lean.ParserDescr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α], ∅.size = 0
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_δ_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.OplaxMonoidal] [inst_9 : G.OplaxMonoidal] (X Y : C × E),
  (CategoryTheory.Functor.OplaxMonoidal.δ (F.prod G) X Y).2 = CategoryTheory.Functor.OplaxMonoidal.δ G X.2 Y.2
-- Mathlib.CategoryTheory.Limits.Cones
/-- A morphism between the two vertex objects of the cones  -/
CategoryTheory.Limits.ConeMorphism.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} →
          {A B : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.ConeMorphism A B → (A.pt ⟶ B.pt)
-- Init.Data.Dyadic.Basic
Rat.toDyadic_eq_ofIntWithPrec : ∀ (x : ℚ) (prec : ℤ), x.toDyadic prec = Dyadic.ofIntWithPrec (x.num <<< prec.toNat / ↑(x.den <<< (-prec).toNat)) prec
-- Lean.Setup
Lean.ImportArtifacts.irSig? : Lean.ImportArtifacts → Option System.FilePath
-- Mathlib.Order.Bounded
Set.unbounded_lt_of_forall_exists_le : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b ∈ s, a ≤ b) → Set.Unbounded (fun x1 x2 => x1 < x2) s
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forget.Faithful : CategoryTheory.ReflQuiv.forget.Faithful
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.Adj.Bicategory.rightUnitor α).hom.τl = (CategoryTheory.Bicategory.rightUnitor α.l).hom
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, 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] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] {K : Type s} [inst_8 : CategoryTheory.SmallCategory K]
  [inst_9 : CategoryTheory.FinCategory K] [inst_10 : CategoryTheory.Limits.HasLimitsOfShape K D]
  [inst_11 : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)]
  [inst_12 : CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (X : C)
  (S :
    CategoryTheory.Limits.Cone
      (F.comp ((J.plusFunctor D).comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X)))))
  (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj F X S)
      ((J.plusMap (CategoryTheory.Limits.limit.π F k)).app (Opposite.op X)) =
    S.π.app k
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_pos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, 0 < a - b ↔ b < a
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
ball_add_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 ≤ δ → ∀ (a b : E), Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.coe_zsmul : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (z : ℤ) (f : M →ₗ⁅R,L⁆ N), ⇑(z • f) = z • ⇑f
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_zero : ∀ {α : Type u_2} [inst : Zero α], Set.Finite 0
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop : ∀ (n : SimplexCategory), PathConnectedSpace ↑(SimplexCategory.toTop.{u}.obj n)
-- Init.Data.String.Termination
String.Slice.Pos.Down.mk : {s : String.Slice} → s.Pos → String.Slice.Pos.Down s
-- Mathlib.Topology.Homotopy.Path
Path.symm.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y),
  γ.symm = { toFun := ⇑γ ∘ unitInterval.symm, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Real.exp` is real analytic.  -/
analyticWithinAt_rexp : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.exp s x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly_k : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The derivative of a differentiable open partial homeomorphism, as a continuous linear
equivalence between the tangent spaces at `x` and `e x`.  -/
OpenPartialHomeomorph.MDifferentiable.mfderiv : {𝕜 : 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'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                {I' : ModelWithCorners 𝕜 E' H'} →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {e : OpenPartialHomeomorph M M'} →
                                          OpenPartialHomeomorph.MDifferentiable I I' e →
                                            {x : M} → x ∈ e.source → TangentSpace I x ≃L[𝕜] TangentSpace I' (↑e x)
-- Init.Data.String.Lemmas.Modify
String.toList_mapAux : ∀ {t₁ t₂ : String} {f : Char → Char} {s : String} {p : s.Pos},
  p.Splits t₁ t₂ → (String.mapAux f s p).toList = t₁.toList ++ List.map f t₂.toList
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv : ∀ {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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F],
  (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv =
    CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Linear map version of the map `toMultilinearMap` associating to a continuous multilinear map
the corresponding multilinear map.  -/
ContinuousMultilinearMap.toMultilinearMapLinear : {ι : Type v} →
  {M₁ : ι → Type w₁} →
    {M₂ : Type w₂} →
      {R' : Type u_1} →
        {A : Type u_2} →
          [inst : Semiring R'] →
            [inst_1 : Semiring A] →
              [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : ContinuousAdd M₂] →
                        [inst_7 : (i : ι) → Module A (M₁ i)] →
                          [inst_8 : Module A M₂] →
                            [inst_9 : Module R' M₂] →
                              [inst_10 : ContinuousConstSMul R' M₂] →
                                [inst_11 : SMulCommClass A R' M₂] →
                                  ContinuousMultilinearMap A M₁ M₂ →ₗ[R'] MultilinearMap A M₁ M₂