mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
/-- If `f` has formal power series `∑ n, pₙ` within a set, on a ball of radius `r`, then for `y, z`
in any smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above
by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`.  -/
HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r r' : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    r' < r →
      ∃ C,
        ∀ y ∈ insert x s ∩ Metric.eball x r',
          ∀ z ∈ insert x s ∩ Metric.eball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Assuming that `(C, J)` is a dense subsite of `(D, K)` (via a functor `G : C ⥤ D`)
and `sheafPushforwardContinuous G A J₀ J` is an equivalence of categories
this is a sheafification functor `(Dᵒᵖ ⥤ A) ⥤ Sheaf K A`
when `HasWeakSheafify J A` holds.  -/
CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              (A : Type u_4) →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                    [(G.sheafPushforwardContinuous A J K).IsEquivalence] →
                      [CategoryTheory.HasWeakSheafify J A] →
                        CategoryTheory.Functor (CategoryTheory.Functor Dᵒᵖ A) (CategoryTheory.Sheaf K A)
-- Mathlib.Order.Basic
Ne.instIsEquiv_compl : ∀ {α : Type u_2}, IsEquiv α (fun x1 x2 => x1 ≠ x2)ᶜ
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetInstance.mk.sizeOf_spec : ∀ (toWidgetInstance : Lean.Widget.WidgetInstance) (range? : Option Lean.Lsp.Range) (name? : Option String),
  sizeOf { toWidgetInstance := toWidgetInstance, range? := range?, name? := name? } =
    1 + sizeOf toWidgetInstance + sizeOf range? + sizeOf name?
-- Mathlib.Order.Comparable
/-- **Alias** of `incompRel_of_incompRel_of_antisymmRel`. -/
IncompRel.trans_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  IncompRel (fun x1 x2 => x1 ≤ x2) a b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → IncompRel (fun x1 x2 => x1 ≤ x2) a c
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
-- Mathlib.Data.Set.Prod
Set.prod_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {b : β}, s ×ˢ {b} = (fun a => (a, b)) '' s
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.sSup_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] (s : Set (Lex ((i : ι) → (fun i => α i) i))) (i : ι), sSup s i = ⨆ e, ↑e i
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.reverse : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.reverse.IsCycle
-- Lean.Compiler.LCNF.Basic
/-- The code we are acting on is to be considered generally impure, doing reorderings is potentially
no longer legal.
 -/
Lean.Compiler.LCNF.Purity.impure : Lean.Compiler.LCNF.Purity
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDTreeMap.filter f t).get? k = Option.filter (f k) (t.get? k)
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.quotientKerEquivOfRightInverse.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P) (g : P → M)
  (hf : Function.RightInverse g ⇑f),
  AddCon.quotientKerEquivOfRightInverse f g hf =
    { toFun := ⇑(AddCon.kerLift f), invFun := AddCon.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.Pos.find?_char_eq_some_iff : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  pos.find? c = some pos' ↔
    pos ≤ pos' ∧
      (∃ (h : pos' ≠ s.endPos), pos'.get h = c) ∧
        ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), pos''.get ⋯ ≠ c
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) {Z : Cᵒᵖ}
  (h : (CategoryTheory.shiftFunctor Cᵒᵖ n).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f) h)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- The function `f ↦ cfcₙ f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{quasispectrum R a}] R`) on those functions which are continuous on
the quasispectrum and map zero to itself.  -/
lipschitzOnWith_cfcₙ_fun : ∀ (R : Type u_2) {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : MetricSpace A] [inst_9 : Module R A] [inst_10 : SMulCommClass R A A]
  [inst_11 : IsScalarTower R A A] [inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A),
  LipschitzOnWith 1 (fun f => cfcₙ ((UniformOnFun.toFun {quasispectrum R a}) f) a)
    {f | ContinuousOn ((UniformOnFun.toFun {quasispectrum R a}) f) (quasispectrum R a) ∧ f 0 = 0}
-- Mathlib.Order.Irreducible
infPrime_iff_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α}, InfPrime a ↔ ¬IsMax a
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.zero_le_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N) (x : M), 0 ≤ (P.RootForm x) x
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- The module isomorphism to the exterior algebra.

Note that this holds more generally when `Q` is divisible by two, rather than only when `1` is
divisible by two; but that would be more awkward to use.  -/
CliffordAlgebra.equivExterior : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → [Invertible 2] → CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
-- Mathlib.SetTheory.Lists
Lists.sizeof_pos : ∀ {α : Type u_1} {b : Bool} (l : Lists' α b), 0 < sizeOf l
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
/-- If `ω` is a closed `1`-form on a convex set `s`, then it admits a primitive,
a version stated in terms of `HasFDerivWithinAt`.  -/
Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    (∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) →
      (∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) →
        ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.ball_subset_trichotomy : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r s : ℝ),
  Metric.ball x r ⊆ Metric.ball y s ∨ Metric.ball y s ⊆ Metric.ball x r ∨ Disjoint (Metric.ball x r) (Metric.ball y s)
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f : EsakiaHom α β}, f.toFun = ⇑f
-- Init.Data.Slice.Array.Lemmas
Std.IterStep.mapIterator.eq_1 : ∀ {α : Type u} {β : Type w} {α' : Type u'} (f : α → α') (it : α) (out : β),
  Std.IterStep.mapIterator f (Std.IterStep.yield it out) = Std.IterStep.yield (f it) out
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_ind_discrete : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {ι : Type u_1}
  [Small.{w, u_1} ι] [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete ι)]
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape ι C] [CategoryTheory.Limits.IsIPCOfShape.{w, u_1, v, u} ι C],
  P.ind.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete ι)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.ext_iff : ∀ {𝕜 : 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} {x y : ModelWithCorners 𝕜 E H},
  x = y ↔ ↑x.toPartialEquiv = ↑y.toPartialEquiv ∧ x.invFun = y.invFun ∧ x.source = y.source ∧ x.target = y.target
-- Mathlib.NumberTheory.LSeries.SumCoeff
LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l) →
    (∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s) →
      Filter.Tendsto (fun s => (↑s - 1) * LSeries f ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds l)
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_zero_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a.tdiv b = 0
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.res_apply : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V ⟶ U)
  (s : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)) (x : ↥V),
  ↑((CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.structureSheafInType R M).obj.map i.op)) s) x = ↑s (i x)
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- **Alias** of `ContinuousLinearMap.le_opENorm`. -/
ContinuousLinearMap.le_opNorm_enorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) (x : E), ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ
-- Mathlib.SetTheory.Lists
Lists'.of_toList : ∀ {α : Type u_1} (l : Lists' α true), Lists'.ofList l.toList = l
-- Init.Data.Array.Lemmas
Array.anyM_toList : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool} {as : Array α},
  List.anyM p as.toList = Array.anyM p as
-- Init.Data.Vector.Int
Vector.sum_append_int : ∀ {n m : ℕ} {as₁ : Vector ℤ n} {as₂ : Vector ℤ m}, (as₁ ++ as₂).sum = as₁.sum + as₂.sum
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.getAltNumFields : Lean.Meta.ElimInfo → Lean.Name → Lean.Elab.TermElabM ℕ
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_mul_top : ∀ (a : ENNReal), (a * ⊤).toReal = 0
-- Mathlib.Data.Nat.Factorial.BigOperators
Nat.prod_factorial_pos : ∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), 0 < ∏ i ∈ s, (f i).factorial
-- Mathlib.Data.Vector.Defs
/-- The tail of a vector obtained by prepending is the vector prepended. to  -/
List.Vector.tail_cons : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), (a ::ᵥ v).tail = v
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.MonoidalCategory.tensor C) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff : Int.Internal.Linear.Poly → Int.Internal.Linear.Var → ℤ
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- This is Exercise 1.2.1 from [tao2010]. It allows you to express integration of a measurable
function with respect to `(μ.withDensity f)` as an integral with respect to `μ`, called the base
measure. `μ` is often the Lebesgue measure, and in this circumstance `f` is the probability density
function, and `(μ.withDensity f)` represents any continuous random variable as a
probability measure, such as the uniform distribution between 0 and 1, the Gaussian distribution,
the exponential distribution, the Beta distribution, or the Cauchy distribution (see Section 2.4
of [wasserman2004]). Thus, this method shows how to one can calculate expectations, variances,
and other moments as a function of the probability density function.
 -/
MeasureTheory.lintegral_withDensity_eq_lintegral_mul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  Measurable f → ∀ {g : α → ENNReal}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
-- Mathlib.CategoryTheory.Limits.Creates
/-- The lifted cone is a limit.  -/
CategoryTheory.liftedLimitIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [inst_3 : CategoryTheory.CreatesLimit K F] →
                  {c : CategoryTheory.Limits.Cone (K.comp F)} →
                    (t : CategoryTheory.Limits.IsLimit c) → CategoryTheory.Limits.IsLimit (CategoryTheory.liftLimit t)
-- Init.SimpLemmas
beq_eq_false_iff_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, (a == b) = false ↔ a ≠ b
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.of_ulift : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.IsStablyFree R (ULift.{w, v} M)], Module.IsStablyFree R M
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction.congr_simp : ∀ {N : ℕ} [inst : NeZero N] (Φ Φ_1 : ZMod N → ℂ),
  Φ = Φ_1 → ∀ (s s_1 : ℂ), s = s_1 → ZMod.completedLFunction Φ s = ZMod.completedLFunction Φ_1 s_1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?.eq_1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (t : RBTree.RBSet α cmp) (x : α), t.find? x = RBTree.RBNode.find? (cmp x) ↑t
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.himp_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α}, a ∈ L → b ∈ L → a ⇨ b ∈ L
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.smul_infty_def : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {g : GL (Fin 2) K},
  g • OnePoint.infty = (OnePoint.equivProjectivization K).symm (Projectivization.mk K ![↑g 0 0, ↑g 1 0] ⋯)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.congr_eq_3 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : x = Ordering.lt → motive Ordering.lt)
  (h_2 : x = Ordering.eq → motive Ordering.eq) (h_3 : x = Ordering.gt → motive Ordering.gt) (heq_1 : x = Ordering.gt),
  (match h : x with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) ≍
    h_3 heq_1
-- Mathlib.Algebra.Group.Conj
ConjClasses.instInhabited : {α : Type u} → [inst : Monoid α] → Inhabited (ConjClasses α)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (u : H ≃ₗᵢ[𝕜] H),
  (Unitary.conjStarAlgAut 𝕜 (H →L[𝕜] H)) (Unitary.linearIsometryEquiv.symm u) = u.conjStarAlgEquiv
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a translation-invariant pseudodistance.  -/
NormedAddCommGroup.ofAddDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddCommGroup E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)) → NormedAddCommGroup E
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportsParams.mk.inj : ∀ {module module_1 : Lean.Lsp.LeanModule}, { module := module } = { module := module_1 } → module = module_1
-- Mathlib.Data.Fin.Fin2
Fin2.rev_rev : ∀ {n : ℕ} (i : Fin2 n), i.rev.rev = i
-- Mathlib.Order.SetNotation
Set.instInfSet : {α : Type u} → InfSet (Set α)
-- Mathlib.Data.Stream.Init
Stream'.map_eq_apply : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' α), Stream'.map f s = Stream'.pure f ⊛ s
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.matchedRuleSetNames : Aesop.RuleSetNameFilter → Option (Array Aesop.RuleSetName)
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
/-- Given an outer measure `μ`, the Carathéodory-measurable space is
defined such that `s` is measurable if `∀ t, μ t = μ (t ∩ s) + μ (t \ s)`.  -/
MeasureTheory.OuterMeasure.caratheodory : {α : Type u} → MeasureTheory.OuterMeasure α → MeasurableSpace α
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- A constant function is a Stieltjes function.  -/
StieltjesFunction.const : (R : Type u_1) → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → ℝ → StieltjesFunction R
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.qr₃ : ∀ (a b : ℕ) (r : ℤ),
  a % 4 = 3 → b % 4 = 3 → Mathlib.Meta.NormNum.jacobiSymNat b a = r → Mathlib.Meta.NormNum.jacobiSymNat a b = -r
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {I : X.IdealSheafData}, I.support = ⊤ ↔ I = ⊥
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.linear_ne_zero : ∀ {cd : Fin 2 → ℝ} (τ : UpperHalfPlane), cd ≠ 0 → ↑(cd 0) * ↑τ + ↑(cd 1) ≠ 0
-- Mathlib.Data.Finset.Option
/-- Given a finset on `α`, lift it to being a finset on `Option α`
using `Option.some` and then insert `Option.none`.  -/
Finset.insertNone : {α : Type u_1} → Finset α ↪o Finset (Option α)
-- Init.Data.List.Nat.Basic
List.getElem?_intersperse_two_mul_add_one : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ}, i + 1 < l.length → (List.intersperse sep l)[2 * i + 1]? = some sep
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wPathDestLeft_wPathCasesOn : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {a : P.A} {f : P.last.B a → P.last.W}
  (g' : (P.drop.B a).Arrow α) (g : (j : P.last.B a) → TypeVec.Arrow (P.WPath (f j)) α),
  P.wPathDestLeft (P.wPathCasesOn g' g) = g'
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.dropn_add : ∀ {α : Type u} (s : Stream'.WSeq α) (m n : ℕ), s.drop (m + n) = (s.drop m).drop n
-- Mathlib.Control.Bifunctor
Bifunctor.snd_id : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁},
  Bifunctor.snd id = id
-- Mathlib.Algebra.Ring.Periodic
/-- For an antiperiodic function `f` with antiperiod `c`, summing `f` over a `Finset` shifted by
`c` (via `addRightEmbedding c`) negates the sum over the original `Finset`.  -/
Function.Antiperiodic.sum_map_addRightEmbedding : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Add α] [inst_1 : IsRightCancelAdd α]
  [inst_2 : SubtractionCommMonoid β],
  Function.Antiperiodic f c → ∀ (s : Finset α), ∑ k ∈ Finset.map (addRightEmbedding c) s, f k = -∑ k ∈ s, f k
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w},
  p.IsPath → u ∉ p.support → ∀ {h : G.Adj u v}, (SimpleGraph.Walk.cons h p).IsPath
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.vecMul_updateCol : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (v : m → α) (B : Matrix m n α) (j : n) (r : m → α),
  Matrix.vecMul v (B.updateCol j r) = Function.update (Matrix.vecMul v B) j (v ⬝ᵥ r)
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.partition_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, (Std.TreeMap.Raw.partition f t).2.WF
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Real.toNNReal_rpow_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → (x ^ y).toNNReal = x.toNNReal ^ y
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.pi : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {s : Set δ} {t : (i : δ) → Set (X i)},
  s.Countable → (∀ i ∈ s, MeasurableSet (t i)) → MeasurableSet (s.pi t)
-- Batteries.CodeAction.Attr
/-- A tactic code action extension.  -/
Batteries.CodeAction.TacticSeqCodeAction : Type
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Monotone.pow_const : ∀ {β : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : Preorder β] [MulLeftMono M]
  [MulRightMono M] {f : β → M}, Monotone f → ∀ (n : ℕ), Monotone fun a => f a ^ n
-- Init.Core
/-- The transitive closure is transitive.  -/
Relation.TransGen.trans : ∀ {α : Sort u} {r : α → α → Prop} {a b c : α},
  Relation.TransGen r a b → Relation.TransGen r b c → Relation.TransGen r a c
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
_private.Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter.0.modularCyclotomicCharacter.termχ₀ : Lean.ParserDescr
-- Mathlib.Logic.Equiv.Sum
/-- A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with
`Equiv.sigmaSumDistrib` which has the sums as the output type.  -/
Equiv.sumSigmaDistrib : {α : Type u_10} →
  {β : Type u_11} → (t : α ⊕ β → Type u_9) → (i : α ⊕ β) × t i ≃ (i : α) × t (Sum.inl i) ⊕ (i : β) × t (Sum.inr i)
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.«term_≼_» : Lean.TrailingParserDescr
-- Init.Data.BitVec.Bitblast
BitVec.toInt_sub_neg_umod : ∀ {w : ℕ} {x y : BitVec w}, x.msb = true → y.msb = false → ¬y.toInt ∣ x.toInt → (y - -x % y).toInt = x.toInt % y.toInt
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.PreIndSpreads.exists_isPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.PreIndSpreads] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J]
  {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D} (x : CategoryTheory.Limits.IsColimit c) {T : C}
  (f : c.pt ⟶ T), P f → ∃ j T' f' g, CategoryTheory.IsPushout (c.ι.app j) f' f g ∧ P f'
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If `f` is locally integrable with respect to `μ.restrict s`, it is locally integrable on `s`.
(See `locallyIntegrableOn_iff_locallyIntegrable_restrict` for an iff statement when `s` is
closed.)  -/
MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} [OpensMeasurableSpace X],
  MeasureTheory.LocallyIntegrable f (μ.restrict s) → MeasureTheory.LocallyIntegrableOn f s μ