mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPtInd_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (N : ℕ) (x : α), (MeasureTheory.SimpleFunc.nearestPtInd e N) x ≤ N
-- Mathlib.RingTheory.FractionalIdeal.Basic
Nat.unaryCast.eq_def : ∀ {R : Type u_1} [inst : One R] [inst_1 : Zero R] [inst_2 : Add R] (x : ℕ),
  x.unaryCast =
    match x with
    | 0 => 0
    | n.succ => n.unaryCast + 1
-- Init.Data.SInt.Lemmas
Int64.neg_add : ∀ {a b : Int64}, -(a + b) = -a - b
-- Init.Data.Ord.Basic
Ordering.eq_eq_iff_isLE_and_isGE : ∀ {o : Ordering}, o = Ordering.eq ↔ o.isLE = true ∧ o.isGE = true
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Summable.hasSum : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α}, Summable f L → HasSum f (∑'[L] (b : β), f b) L
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_order_map : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {S : Type u_3} [inst_1 : Semiring S] (f : R →+* S)
  {φ : MvPowerSeries σ R}, φ.order ≤ ((MvPowerSeries.map f) φ).order
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- A more general version of `summable_congr`, allowing the functions to
disagree on a finite set.  -/
summable_congr_cofinite : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f g : β → α}, f =ᶠ[Filter.cofinite] g → (Summable f ↔ Summable g)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_nil : ∀ {α : Type u}, Stream'.Seq.nil.length ⋯ = 0
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Lagrange's **Mean Value Theorem**, applied to convex domains.  -/
domain_mvt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x y : E}
  {f' : E → StrongDual ℝ E},
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    Convex ℝ s → x ∈ s → y ∈ s → ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  s.toKaroubiNondegComplexIsoN₁.inv.f.f n =
    s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))
-- Mathlib.Algebra.Algebra.Defs
algebraMap.smul : ∀ {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [inst : SMul A B] [inst_1 : CommSemiring B]
  [inst_2 : Semiring C] [inst_3 : Algebra B C] [inst_4 : SMul A C] [IsScalarTower A B C],
  (algebraMap B C) (a • b) = a • (algebraMap B C) b
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.comp_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] (g : ZeroHom N P)
  (f : ZeroHom M N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i j k : ℕ)
  (hij : i ≤ j) (hjk : j ≤ k),
  CategoryTheory.Functor.OfSequence.map f i k ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i j hij)
      (CategoryTheory.Functor.OfSequence.map f j k hjk)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measure_eq_trim : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α), μ s = μ.trim s
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Two linear equivs are equal if they are equal on basis vectors.  -/
Module.Basis.ext' : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {R₁ : Type u_13} [inst_3 : Semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R}
  [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ] {M₁ : Type u_14} [inst_6 : AddCommMonoid M₁]
  [inst_7 : Module R₁ M₁] {f₁ f₂ : M ≃ₛₗ[σ] M₁}, (∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_mul_right_of_le : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atTop → (∀ (x : α), C ≤ g x) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_eq_ite : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α}, a⁺ᵐ = if 1 ≤ a then a else 1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_of_isEmpty : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} [IsEmpty ι] {Y : ι → C}
  (f : (i : ι) → Y i ⟶ X), CategoryTheory.Presieve.ofArrows Y f = ⊥
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- A letter only reduces to itself.  -/
FreeAddGroup.Red.singleton_iff : ∀ {α : Type u} {L₁ : List (α × Bool)} {x : α × Bool}, FreeAddGroup.Red [x] L₁ ↔ L₁ = [x]
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_source_of_mem_source : ∀ {𝕜 : 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'] {f : M → M'} {s : Set M} {x x' : M}
  {n : WithTop ℕ∞} [IsManifold I n M],
  x' ∈ (chartAt H x).source →
    (ContMDiffWithinAt I I' n f s x' ↔
      ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x'))
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_Iic : ∀ {f : ℝ → ℝ} {y : ℝ}, ConvexOn ℝ (Set.Iic y) f → ContinuousWithinAt f (Set.Iic y) y → ContinuousOn f (Set.Iic y)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {k a : α} {v : β}, (t.insert k v)[a]! = if cmp k a = Ordering.eq then v else t[a]!
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_id_of_isIso : ∀ {x : SimplexCategory} (f : x ⟶ x) [CategoryTheory.IsIso f], f = CategoryTheory.CategoryStruct.id x
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given `F : C ⥤ D` and `X : C`, `yoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type _` is the
left Kan extension of `yoneda.obj X : Cᵒᵖ ⥤ Type _` along `F.op`.  -/
CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.yoneda.obj (F.obj X)).IsLeftKanExtension (CategoryTheory.yonedaMap F X)
-- Mathlib.Analysis.Convex.Strict
StrictConvex.linear_image : ∀ {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : TopologicalSpace E] [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid E] [inst_5 : AddCommMonoid F]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] {s : Set E} [inst_8 : Semiring 𝕝] [inst_9 : Module 𝕝 E]
  [inst_10 : Module 𝕝 F] [LinearMap.CompatibleSMul E F 𝕜 𝕝],
  StrictConvex 𝕜 s → ∀ (f : E →ₗ[𝕝] F), IsOpenMap ⇑f → StrictConvex 𝕜 (⇑f '' s)
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.of_comm_of_nhds_one : ∀ {G : Type u} [inst : CommGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1) →
    Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) → IsTopologicalGroup G
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSymbolInformation.toJson : Lean.Lsp.SymbolInformation → Lean.Json
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.mk : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {X : Ω → ℝ} {c : NNReal}
  {κ : ProbabilityTheory.Kernel Ω' Ω}
  {ν : autoParam (MeasureTheory.Measure Ω') ProbabilityTheory.Kernel.HasSubgaussianMGF._auto_1},
  (∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) (ν.bind ⇑κ)) →
    (∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), ProbabilityTheory.mgf X (κ ω') t ≤ Real.exp (↑c * t ^ 2 / 2)) →
      ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instBEqKey : BEq Lean.Meta.DiscrTree.Key
-- Mathlib.Algebra.Module.Torsion.Basic
AddSubgroup.torsionBy.mod_self_nsmul' : ∀ {A : Type u_3} [inst : AddCommGroup A] {n : ℕ} (s : ℕ) {x : A}, x ∈ AddSubgroup.torsionBy A ↑n → s • x = (s % n) • x
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The identity function as an element of `C(s, R)₀` when `0 ∈ (s : Set R)`.  -/
ContinuousMapZero.id : {R : Type u_3} →
  [inst : Zero R] → [inst_1 : TopologicalSpace R] → (s : Set R) → [inst_2 : Fact (0 ∈ s)] → ContinuousMapZero (↑s) R
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.Hom.equivContinuousMap_apply : ∀ (X Y : TopCat) (f : X ⟶ Y), (TopCat.Hom.equivContinuousMap X Y) f = TopCat.Hom.hom f
-- Init.Data.Vector.Lemmas
Vector.idRun_foldlM : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {f : β → α → Id β} {b : β} {xs : Vector α n},
  (Vector.foldlM f b xs).run = Vector.foldl (fun x1 x2 => (f x1 x2).run) b xs
-- Init.Data.List.Lex
List.not_lt : ∀ {α : Type u_1} [inst : LT α] {l₁ l₂ : List α}, ¬l₁ < l₂ ↔ l₂ ≤ l₁
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} {s : Set E} [inst_7 : IntCast F] (z : ℤ), DifferentiableWithinAt 𝕜 (↑z) s x
-- Init.Data.UInt.Lemmas
USize.succ_mul : ∀ {a b : USize}, (a + 1) * b = a * b + b
-- Mathlib.Data.PFun
PFun.mem_core_res : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (x : α), x ∈ (PFun.res f s).core t ↔ x ∈ s → f x ∈ t
-- Init.Data.BitVec.Lemmas
BitVec.getElem_append : ∀ {n m i : ℕ} {x : BitVec n} {y : BitVec m} (h : i < n + m), (x ++ y)[i] = if h : i < m then y[i] else x[i - m]
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.cons' : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  {rs : List R},
  IsSMulRegular M r →
    RingTheory.Sequence.IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) →
      RingTheory.Sequence.IsRegular M (r :: rs)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedHurwitzZetaEven₀_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedHurwitzZetaEven₀ (-a) s = HurwitzZeta.completedHurwitzZetaEven₀ a s
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.AtomIso.mk.inj : ∀ {e : Lean.Expr} {src tgt : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr}
  {src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  { e := e, src := src, tgt := tgt } = { e := e_1, src := src_1, tgt := tgt_1 } → e = e_1 ∧ src = src_1 ∧ tgt = tgt_1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Given a theorem with proof `proof` and `numParams` parameters, returns a message
containing the parameters at positions `paramPos`.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.ppParamsAt : Lean.Expr → ℕ → List ℕ → Lean.MetaM Lean.MessageData
-- Lean.Meta.CongrTheorems
/-- Returns `true` if `s` is of the form `hcongr_<idx>`  -/
Lean.Meta.isHCongrReservedNameSuffix : String → Bool
-- Std.Time.Format
/-- Parses a string representing an offset into an `Offset` object. The input string must follow the `"xxx"` format.
 -/
Std.Time.TimeZone.Offset.fromOffset : String → Except String Std.Time.TimeZone.Offset
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.normalizerCondition_of_isNilpotent`. -/
normalizerCondition_of_isNilpotent : ∀ {G : Type u_1} [inst : Group G] [h : Group.IsNilpotent G], NormalizerCondition G
-- Mathlib.Data.W.Constructions
WType.Listα.nil : {γ : Type u} → WType.Listα γ
-- Mathlib.Geometry.Manifold.VectorField.Pullback
MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [inst_11 : IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E],
  MDiffAt[t] (T% V) y₀ →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            2 ≤ n → y₀ = f x₀ → (MDiffAt[s ∩ f ⁻¹' t] fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) x₀
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → ‖r‖ = r
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The isomorphism between special linear groups of isomorphic modules.  -/
SpecialLinearGroup.congr_linearEquiv : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          {W : Type u_3} →
            [inst_3 : AddCommGroup W] →
              [inst_4 : Module R W] → (V ≃ₗ[R] W) → SpecialLinearGroup R V ≃* SpecialLinearGroup R W
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q} ↔ q = p ∧ dist p s.center = s.radius
-- Batteries.Recycling.RBTree.WF
/-- The balancing properties of the `balLeft` function.  -/
RBTree.RBNode.Balanced.balLeft : ∀ {α : Type u_1} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α} {cr : RBTree.RBColor} {n : ℕ},
  RBTree.RBNode.RedRed True l n →
    r.Balanced cr (n + 1) → RBTree.RBNode.RedRed (cr = RBTree.RBColor.red) (l.balLeft v r) (n + 1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (hl : l.Balanced) →
          ((hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hl) →
            ((sz : ℕ) →
                (ky : α) →
                  (y : β ky) →
                    (l r : Std.DTreeMap.Internal.Impl α β) →
                      (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) →
                        motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl) →
              motive l hl
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A function is `FinStronglyMeasurable` with respect to a measure if it is the limit of simple
functions with support with finite measure.  -/
MeasureTheory.FinStronglyMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    [TopologicalSpace β] →
      [Zero β] →
        {x : MeasurableSpace α} →
          (α → β) → autoParam (MeasureTheory.Measure α) MeasureTheory.FinStronglyMeasurable._auto_1 → Prop
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_ceil_div_atTop : ∀ {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : Field R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  [OrderTopology R] [inst_5 : FloorRing R], Filter.Tendsto (fun x => ↑⌈x⌉₊ / x) Filter.atTop (nhds 1)
-- Mathlib.Algebra.Order.AddGroupWithTop
/-- If `G` has subtraction, we can extend the subtraction to `WithTop G`, by setting `x - ⊤ = ⊤` and
`⊤ - x = ⊤`. This definition is only registered as an instance on additive commutative groups, to
avoid conflicting with the instance `WithTop.instSub` on types with a bottom element.  -/
WithTop.LinearOrderedAddCommGroup.instSub : {G : Type u_1} → [AddCommGroup G] → Sub (WithTop G)
-- Lean.Parser.Command
Lean.Parser.Command.assertNotExists.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.SetSemiring
_private.Mathlib.MeasureTheory.SetSemiring.0.MeasureTheory.IsSetSemiring.disjointOfUnion.eq_1 : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C) (j : Set α),
  hC.disjointOfUnion hJ j = if hj : j ∈ J then ⋯.choose.parts else ∅
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.map_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.NonemptyCompacts α),
  TopologicalSpace.NonemptyCompacts.map id ⋯ K = K
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toInt16 = Int16.ofInt n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.toArray_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : BEq α] [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp]
  {k : α}, (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_zero_vadd : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] (r : R) (x : AddOreLocalization S X),
  (r +ᵥ 0) +ᵥ x = r +ᵥ x
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition] [inst_3 : Q.IsStableUnderBaseChange]
  (f : X ⟶ Y) [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.IsStableUnderBaseChangeAlong f]
  [inst_6 : Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) (A : P.Over Q Y),
  (CategoryTheory.MorphismProperty.Over.mapPullbackAdj P Q f hPf hQf).counit.app A =
    CategoryTheory.MorphismProperty.Over.homMk (CategoryTheory.Limits.pullback.fst A.hom f) ⋯ ⋯
-- Mathlib.Data.Set.Lattice
Set.iInter_congr_of_surjective : ∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂),
  Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⋂ x, f x = ⋂ y, g y
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- An iff variation on `ordinaryHypergeometricSeries_eq_zero_of_nonpos_int` for `[RCLike 𝕂]`.  -/
ordinaryHypergeometricSeries_eq_zero_iff : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  (a b c : 𝕂) (n : ℕ), ordinaryHypergeometricSeries 𝔸 a b c n = 0 ↔ ∃ k < n, ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- An equivalence of categories induces an equivalence on under categories.  -/
CategoryTheory.Under.postEquiv : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (X : T) → (F : T ≌ D) → CategoryTheory.Under X ≌ CategoryTheory.Under (F.functor.obj X)
-- Mathlib.Analysis.Normed.Group.Uniform
NormedGroup.to_isIsometricSMul_right : ∀ {E : Type u_2} [inst : SeminormedCommGroup E], IsIsometricSMul Eᵐᵒᵖ E
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
/-- The degree of an irreducible monic factor of the `n`-th cyclotomic polynomial over a finite
field. This is a special case of `natDegree_of_dvd_cyclotomic_of_irreducible` below.  -/
_private.Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization.0.Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible_of_monic : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ} {P : Polynomial K},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)],
      P ∣ Polynomial.cyclotomic n K → Irreducible P → P.Monic → P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)
-- Lean.Parser.Types
Lean.Parser.InputContext.mk'.inj : ∀ {inputString fileName : String} {fileMap : Lean.FileMap} {endPos : String.Pos.Raw}
  {endPos_valid : autoParam (endPos ≤ inputString.rawEndPos) Lean.Parser.InputContext.endPos_valid._autoParam}
  {inputString_1 fileName_1 : String} {fileMap_1 : Lean.FileMap} {endPos_1 : String.Pos.Raw}
  {endPos_valid_1 : autoParam (endPos_1 ≤ inputString_1.rawEndPos) Lean.Parser.InputContext.endPos_valid._autoParam},
  { inputString := inputString, fileName := fileName, fileMap := fileMap, endPos := endPos,
        endPos_valid := endPos_valid } =
      { inputString := inputString_1, fileName := fileName_1, fileMap := fileMap_1, endPos := endPos_1,
        endPos_valid := endPos_valid_1 } →
    inputString = inputString_1 ∧ fileName = fileName_1 ∧ fileMap = fileMap_1 ∧ endPos = endPos_1
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_parts_le_card : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), P.parts.card ≤ s.card
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_const' : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  (c : ε), p ≠ 0 → p ≠ ⊤ → MeasureTheory.eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingHom_coe : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  {f : α →+* β} (hf : Continuous ⇑f) (a : α), (UniformSpace.Completion.mapRingHom f hf) ↑a = ↑(f a)
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderivWithin_clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {s : Set E} {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      DifferentiableWithinAt 𝕜 u s x →
        fderivWithin 𝕜 (fun y => (c y) (u y)) s x = c x ∘SL fderivWithin 𝕜 u s x + (fderivWithin 𝕜 c s x).flip (u x)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_iff_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {k : α}, k ∈ t ↔ t.contains k = true
-- Mathlib.Algebra.Order.Group.End
RelIso.one_apply : ∀ {α : Type u_1} {r : α → α → Prop} (x : α), 1 x = x
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.stabilizer.surjective_toPerm : ∀ {α : Type u_2} (s : Set α), Function.Surjective MulAction.toPerm
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toNonUnitalStarSubalgebra_injective : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A],
  Function.Injective StarSubalgebra.toNonUnitalStarSubalgebra
-- Init.Data.List.Perm
_private.Init.Data.List.Perm.0.List.reverseAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) → ((r : List α) → motive [] r) → ((a : α) → (l r : List α) → motive (a :: l) r) → motive x x_1