mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Lemmas
USize.toUInt32_mod : ∀ (a b : USize), a < 4294967296 → b < 4294967296 → (a % b).toUInt32 = a.toUInt32 % b.toUInt32
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_snoc : ∀ {m n : ℕ} {α : Sort u_2} (as : Fin n → α) (bs : Fin m → α) (b : α),
  Fin.append as (Fin.snoc bs b) = Fin.snoc (Fin.append as bs) b
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.below.zero : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop}
  {motive : (a : Multiset α) → (a_1 : Multiset β) → Multiset.Rel r a a_1 → Prop}, Multiset.Rel.below ⋯
-- Mathlib.CategoryTheory.Limits.Presentation
/-- Change the index category of a limit presentation.  -/
CategoryTheory.Limits.LimitPresentation.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          CategoryTheory.Limits.LimitPresentation J X →
            {J' : Type u_1} →
              [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] →
                (F : CategoryTheory.Functor J' J) → [F.Initial] → CategoryTheory.Limits.LimitPresentation J' X
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `f □ (∅ ⟶ L)` lifts against `X ⟶ ⋆` if and only if `f` lifts against `(L ⟹ X) ⟶ ⋆`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} (i : CategoryTheory.Limits.IsInitial K)
  (t : CategoryTheory.Limits.IsTerminal Y),
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk (i.to L)).hom (t.from X) ↔
    CategoryTheory.HasLiftingProperty f (t.from (L ⟹ X))
-- Init.Data.Int.Order
Int.toNat?.eq_1 : ∀ (n : ℕ), (Int.ofNat n).toNat? = some n
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_bounded_set_le : ∀ (α : Type u) (c : Cardinal.{u}), Cardinal.mk { t // Cardinal.mk ↑t ≤ c } ≤ max (Cardinal.mk α) Cardinal.aleph0 ^ c
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.Set : ShareCommon.StateFactoryBuilder → (α : Type) → [BEq α] → [Hashable α] → Type
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_1 : Turing.ToPartrec.Code.zero'.eval = fun v => pure (0 :: v)
-- Init.Data.Int.Gcd
Int.gcd_neg : ∀ {a b : ℤ}, a.gcd (-b) = a.gcd b
-- Init.Control.Lawful.MonadLift.Basic
/-- The `MonadLiftT` typeclass only contains the transitive lifting operation.
  `LawfulMonadLiftT` further asserts that lifting commutes with `pure` and `bind`:
```
monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
```
 -/
LawfulMonadLiftT : (m : Type u → Type v) → (n : Type u → Type w) → [Monad m] → [Monad n] → [inst : MonadLiftT m n] → Prop
-- Mathlib.GroupTheory.Exponent
AddMonoid.addOrder_dvd_exponent : ∀ {G : Type u} [inst : AddMonoid G] (g : G), addOrderOf g ∣ AddMonoid.exponent G
-- Batteries.Data.AssocList
/-- The number of entries in an `AssocList`.  -/
Batteries.AssocList.length : {α : Type u_1} → {β : Type u_2} → Batteries.AssocList α β → ℕ
-- Mathlib.Order.SetNotation
/-- Class for the `sInf` operator  -/
InfSet : Type u_1 → Type u_1
-- Mathlib.Algebra.Group.Defs
IsRightRegular.mul_eq_one_symm : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, IsRightRegular a → b * a = 1 → a * b = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor_mapId : ∀ {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)
  (x : CategoryTheory.LocallyDiscrete C), F.toPseudofunctor.mapId x = CategoryTheory.eqToIso ⋯
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsNormal.conjugation_bij : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C),
  S.IsNormal →
    ∀ {c d : C} (p : c ⟶ d),
      Set.BijOn
        (fun γ =>
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv p) (CategoryTheory.CategoryStruct.comp γ p))
        (S.arrows c c) (S.arrows d d)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addY_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W.addY P Q = WeierstrassCurve.Jacobian.addU P Q ^ 3
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The extension of `g` along `f`.  -/
CategoryTheory.Bicategory.RightExtension.extension : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : a ⟶ b} → {g : a ⟶ c} → CategoryTheory.Bicategory.RightExtension f g → (b ⟶ c)
-- Mathlib.Order.Partition.Basic
Partition.mem_copy_iff : ∀ {α : Type u_1} {s t x : α} [inst : CompleteLattice α] {P : Partition s} (hst : s = t), x ∈ P.copy hst ↔ x ∈ P
-- Mathlib.Analysis.Meromorphic.Order
/-- Helper lemma for `meromorphicOrderAt_add_of_ne`.
 -/
meromorphicOrderAt_add_eq_left_of_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f₂ x →
    meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x → meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x
-- Init.Data.UInt.Lemmas
UInt64.sub_right_inj : ∀ {a b : UInt64} (c : UInt64), c - a = c - b ↔ a = b
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forwardMatches.sizeOf_spec : ∀ (ms : Array Aesop.ForwardRuleMatch), sizeOf (Aesop.RuleTacDescr.forwardMatches ms) = 1 + sizeOf ms
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.zero_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0), MeasureTheory.Measure.trim 0 hm = 0
-- Mathlib.SetTheory.ZFC.Ordinal
/-- The membership operation within an ordinal is transitive.  -/
ZFSet.IsOrdinal.mem_trans' : ∀ {x : ZFSet.{u_1}}, x.IsOrdinal → ∀ {y z w : ZFSet.{u_1}}, y ∈ z → z ∈ w → w ∈ x → y ∈ w
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.nonempty_monotone_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, s.Nonempty → Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (G : CategoryTheory.ComposableArrows C n)
  (j : Fin (n + 1)),
  (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows G).incl.app j = G.map ((Fin.isTerminalLast n).from j)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.asIdeal : {R : Type u_1} → [inst : CommRing R] → IsDedekindDomain.HeightOneSpectrum R → Ideal R
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.contains_eq_contains_toSlice : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String}, s.contains pat = s.toSlice.contains pat
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the right as an `AddMonoidHom`. Similar to `AddMonoidHom.compHom'`.  -/
ContinuousMap.compAddMonoidHom' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {γ : Type u_3} →
          [inst_2 : TopologicalSpace γ] →
            [inst_3 : AddZeroClass γ] → [inst_4 : ContinuousAdd γ] → C(α, β) → C(β, γ) →+ C(α, γ)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.rotateRight.sizeOf_spec : ∀ (n : ℕ), sizeOf (Std.Tactic.BVDecide.BVUnOp.rotateRight n) = 1 + sizeOf n
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- **Alias** of the reverse direction of `SimpleGraph.cliqueSet_eq_empty_iff`. -/
SimpleGraph.CliqueFree.cliqueSet : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, G.CliqueFree n → G.cliqueSet n = ∅
-- Init.Data.Order.Lemmas
Std.instTrichotomousLtOfLawfulOrderLTOfTotalOfAntisymmLe : ∀ {α : Type u} {x : LT α} [inst : LE α] [Std.LawfulOrderLT α] [Std.Total fun x1 x2 => x1 ≤ x2]
  [Std.Antisymm fun x1 x2 => x1 ≤ x2], Std.Trichotomous fun x1 x2 => x1 < x2
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_eq_tsum_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G]
  {ν : MeasureTheory.Measure α},
  MeasureTheory.IsFundamentalDomain G s μ → ν.AbsolutelyContinuous μ → ∀ (t : Set α), ν t = ∑' (g : G), ν (t ∩ g • s)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X' : C} (f : X' ⟶ X) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasKernel g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIsoComp f g).hom
      (CategoryTheory.Limits.kernelSubobject g).arrow =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)).arrow f
-- Init.Data.Int.LemmasAux
Int.mul_le_mul_of_le_of_le_of_nonpos_of_nonneg : ∀ {a b c d : ℤ}, c ≤ a → b ≤ d → b ≤ 0 → 0 ≤ c → a * b ≤ c * d
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_neg_pi_div_two_mul_I : Complex.exp (-↑Real.pi / 2 * Complex.I) = -Complex.I
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.injective_mapNatBool : ∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α]
  [MeasurableSpace.SeparatesPoints α], Function.Injective (MeasurableSpace.mapNatBool α)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).getKey? k' =
    if (k == k') = true then if (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then some k else none
    else m.getKey? k'
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inclusion_faithful : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S T : CategoryTheory.Subgroupoid C} (h : S ≤ T) (s t : ↑S.objs),
  Function.Injective fun f => (CategoryTheory.Subgroupoid.inclusion h).map f
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instTop : {M : Type u_1} → [inst : MulOneClass M] → Top (SaturatedSubmonoid M)
-- Mathlib.Data.Multiset.AddSub
Multiset.singleton_add : ∀ {α : Type u_1} (a : α) (s : Multiset α), {a} + s = a ::ₘ s
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodePi.match_3.eq_1 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.prod f) → Sort u_1) (x : Fin 0 → ℕ) (x_1 : Fin (Fin.prod x))
  (h_1 : (x : Fin 0 → ℕ) → (x_2 : Fin (Fin.prod x)) → motive 0 x x_2)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : ℕ) → (hx : x < Fin.prod f) → motive n.succ f ⟨x, hx⟩),
  (match 0, x, x_1 with
    | 0, x, x_2 => h_1 x x_2
    | n.succ, f, ⟨x, hx⟩ => h_2 n f x hx) =
    h_1 x x_1
-- Init.Data.Bool
Bool.decide_and : ∀ (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q], decide (p ∧ q) = (decide p && decide q)
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.mapCoeffs_X : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (d : Derivation R A M),
  d.mapCoeffs Polynomial.X = 0
-- Mathlib.Analysis.Normed.Group.Continuity
Continuous.norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  Continuous f → Continuous fun x => ‖f x‖
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The `n`th function in this family is `Γ(s)` if `-n < s.re`, and junk otherwise.  -/
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux : ℕ → ℂ → ℂ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is strictly between the other two, the angle at that point
(reversed) is π.  -/
Sbtw.angle₃₂₁_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- [Stacks Tag 01Z4](https://stacks.math.columbia.edu/tag/01Z4) ((1)) -/
AlgebraicGeometry.exists_preimage_eq : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] (U : c.pt.Opens),
  IsCompact ↑U → ∃ i V, IsCompact ↑V ∧ (TopologicalSpace.Opens.map (c.π.app i).base).obj V = U
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.map_fun : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.Embedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_takeEndWhile_iff_dropEndWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  (s.takeEndWhile pat).isEmpty = true ↔ s.dropEndWhile pat = s
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- `x : tzre R M` is invertible when `x.fst : R` is.  -/
TrivSqZeroExt.invertibleOfInvertibleFst : {R : Type u} →
  {M : Type v} →
    [inst : AddCommGroup M] →
      [inst_1 : Semiring R] →
        [inst_2 : Module Rᵐᵒᵖ M] →
          [inst_3 : Module R M] → [SMulCommClass R Rᵐᵒᵖ M] → (x : TrivSqZeroExt R M) → [Invertible x.fst] → Invertible x
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A Cauchy filter in a discrete uniform space is contained in the principal filter
of a point.  -/
DiscreteUniformity.eq_pure_of_cauchy : ∀ {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α] {f : Filter α}, Cauchy f → ∃ x, f = pure x
-- Mathlib.Analysis.Convex.Topology
/-- In a topological vector space, the closure of a convex set is convex.  -/
Convex.closure : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → Convex 𝕜 (closure s)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcKeepAliveParams.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (sessionId : UInt64),
  sizeOf { uri := uri, sessionId := sessionId } = 1 + sizeOf uri + sizeOf sessionId
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.compContinuousLinearMapCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F] {E' : Type u_6}
  [inst_9 : AddCommGroup E'] [inst_10 : Module 𝕜 E'] [inst_11 : TopologicalSpace E'] (f : E →L[𝕜] E')
  (g : E' [⋀^ι]→L[𝕜] F), (ContinuousAlternatingMap.compContinuousLinearMapCLM f) g = g.compContinuousLinearMap f
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.inv_hom_apply : ∀ {M N : MonCat} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` is `C¹` on a convex compact set `s`, it is Lipschitz on `s`.  -/
ContDiffOn.exists_lipschitzOnWith : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {s : Set E} {f : E → F} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → n ≠ 0 → Convex ℝ s → IsCompact s → ∃ K, LipschitzOnWith K f s
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ},
  ↑i ≤ n →
    ∀ {f : ContDiffMapSupportedIn E F n K} {x : E},
      ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter m₂ ⋯).getD k fallback = m₁.getD k fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ_ne_zero_of_X_ne : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R},
  P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 → WeierstrassCurve.Jacobian.addZ P Q ≠ 0
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableVAdd_of_add : ∀ (M : Type u_2) [inst : Add M] [inst_1 : MeasurableSpace M] [MeasurableAdd M], MeasurableVAdd M M
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- (Implementation) Given the appropriate product and equalizer cones, build the cone for `F` which is
limiting if the given cones are also.
 -/
CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {F : CategoryTheory.Functor J C} →
          {c₁ : CategoryTheory.Limits.Fan F.obj} →
            {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} →
              (s t : c₁.pt ⟶ c₂.pt) →
                (∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                    CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) =
                      CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) →
                  (∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                      CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) →
                    CategoryTheory.Limits.Fork s t → CategoryTheory.Limits.Cone F
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)},
  (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃a' : α⦄, (a, b, c) ∈ t → (a', b, c) ∈ t → a = a') →
    (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃b' : β⦄, (a, b, c) ∈ t → (a, b', c) ∈ t → b = b') →
      (∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c c' : γ⦄, (a, b, c) ∈ t → (a, b, c') ∈ t → c = c') →
        SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R], ↑1 = 1
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalSemiring.mk : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocSemiring R] [toContinuousAdd : ContinuousAdd R]
  [toSeparatelyContinuousMul : SeparatelyContinuousMul R], IsSemitopologicalSemiring R
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_succ_succ : ∀ {m n : ℕ}, ((m + 1)<...=n + 1).toArray = Array.map (fun x => x + 1) (m<...=n).toArray
-- Mathlib.Topology.GDelta.Basic
/-- A set is called **meagre** iff its complement is a residual (or comeagre) set.  -/
IsMeagre : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- All points are in `⊤`.  -/
AffineSubspace.mem_top : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P), p ∈ ⊤
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State : Type
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.eigenvectorBasis_def : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  hT.eigenvectorBasis hn =
    (DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯).reindex
      (Equiv.symm (Tuple.sort (LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn) * Fin.revPerm))
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.constAlterKey : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.Const.alterKey a f l)
-- Lean.Elab.InfoTree.Types
/-- Context for a sub-`InfoTree`.

Within `InfoTree`, this must fulfill the invariant that every non-`commandCtx` `PartialContextInfo`
node is always contained within a `commandCtx` node.
 -/
Lean.Elab.PartialContextInfo : Type
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The closed subspace of vectors orthogonal to a given subspace, denoted `Kᗮ`.  -/
ClosedSubmodule.«term_ᗮ» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.rel_neg : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (p q r s : ℤ), IsEllipticNet.rel W (-p) (-q) (-r) (-s) = IsEllipticNet.rel W p q r s
-- Mathlib.Analysis.Seminorm
Seminorm.bddAbove_iff : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set (Seminorm 𝕜 E)}, BddAbove s ↔ BddAbove (DFunLike.coe '' s)
-- Mathlib.GroupTheory.Schreier
card_dvd_exponent_nsmul_rank : ∀ (G : Type u_1) [inst : AddCommGroup G] [inst_1 : AddGroup.FG G], Nat.card G ∣ AddMonoid.exponent G ^ AddGroup.rank G
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_ne_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → (MeasureTheory.Measure.map f μ ≠ 0 ↔ μ ≠ 0)
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductive.go.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (x : Option ℕ) (h_1 : (val : ℕ) → motive (some val)) (h_2 : (x : Option ℕ) → motive x),
  (∀ (val : ℕ), x = some val → False) →
    (match x with
      | some val => h_1 val
      | x => h_2 x) =
      h_2 x
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.lt_of_pos_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R},
  0 < ArchimedeanClass.mk x → ∀ {y : S}, 0 < y → x < f y
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_self_inter : ∀ {α : Type u_1} (s t : Set α), Subtype.val ⁻¹' (s ∩ t) = Subtype.val ⁻¹' t
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingFun` is a ring seminorm.  -/
smoothingSeminorm : {R : Type u_1} → [inst : CommRing R] → (μ : RingSeminorm R) → μ 1 ≤ 1 → IsNonarchimedean ⇑μ → RingSeminorm R
-- Mathlib.Data.Num.Basic
/-- Addition of two `PosNum`s.  -/
PosNum.add : PosNum → PosNum → PosNum
-- Init.Data.Fin.Lemmas
Fin.castSucc_castLT : ∀ {n : ℕ} (i : Fin (n + 1)) (h : ↑i < n), (i.castLT h).castSucc = i