mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- An open neighborhood of the identity in the Cartesian square of a nonarchimedean group
contains the Cartesian square of an open neighborhood in the group.  -/
NonarchimedeanGroup.prod_self_subset : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [NonarchimedeanGroup G] {U : Set (G × G)},
  U ∈ nhds 1 → ∃ V, ↑V ×ˢ ↑V ⊆ U
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.isAffineMap_map : ∀ (R : Type u_1) {I : Type u_6} {J : Type u_7} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] (f : I → J), Convexity.IsAffineMap R (Convexity.StdSimplex.map f)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- **Alias** of `HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIso`.

---

The isomorphism `toHoCat ⋙ toLocalization L ≅ ι ⋙ L` which expresses that
if `L : C ⥤ D` is a localization functor, then its restriction on the
full subcategory of cofibrant objects factors through the homotopy category
of cofibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.toπCompToLocalizationIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              HomotopicalAlgebra.CofibrantObject.toHoCat.comp
                  (HomotopicalAlgebra.CofibrantObject.HoCat.toLocalization L) ≅
                HomotopicalAlgebra.CofibrantObject.ι.comp L
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algebraMap_left_injective : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (v : AbsoluteValue R S),
  Function.Injective ⇑(algebraMap R T) → Function.Injective ⇑(algebraMap (WithAbs v) T)
-- Mathlib.ModelTheory.PartialEquiv
/-- The limit of a directed system of PartialEquivs.  -/
FirstOrder.Language.DirectLimit.partialEquivLimit : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          {ι : Type u_1} →
            [inst_2 : Preorder ι] → [Nonempty ι] → [IsDirectedOrder ι] → (ι →o L.PartialEquiv M N) → L.PartialEquiv M N
-- Mathlib.Algebra.Algebra.Equiv
/-- Interpret an algebra equivalence as a linear map.  -/
AlgEquiv.toLinearMap : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ →ₗ[R] A₂
-- Std.Data.HashSet.Raw
/-- Removes all elements from the hash set for which the given function returns `false`.  -/
Std.HashSet.Raw.filter : {α : Type u} → [BEq α] → [Hashable α] → (α → Bool) → Std.HashSet.Raw α → Std.HashSet.Raw α
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofErrorNameInfo.sizeOf_spec : ∀ (i : Lean.Elab.ErrorNameInfo), sizeOf (Lean.Elab.Info.ofErrorNameInfo i) = 1 + sizeOf i
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- A special case of `Summable.map_iff_of_leftInverse` for convenience  -/
Summable.map_iff_of_equiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_4}
  [inst_4 : EquivLike G α γ] [AddEquivClass G α γ] (g : G),
  Continuous ⇑g → Continuous (EquivLike.inv g) → (Summable (⇑g ∘ f) L ↔ Summable f L)
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectOutput.below.indirect : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive : (a : Std.IterM m β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} {it it' : Std.IterM m β} {out : β}
  (a : it'.IsPlausibleSuccessorOf it) (a_1 : it'.IsPlausibleIndirectOutput out),
  Std.IterM.IsPlausibleIndirectOutput.below a_1 → motive it' out a_1 → Std.IterM.IsPlausibleIndirectOutput.below ⋯
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.instIsAddTorsionFree : ∀ {ι : Type u_1} {M : ι → Type u_3} [inst : (i : ι) → AddMonoid (M i)] [∀ (i : ι), IsAddTorsionFree (M i)],
  IsAddTorsionFree ((i : ι) → M i)
-- Lean.Data.Name
Lean.Name.quickLt : Lean.Name → Lean.Name → Bool
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_addMonoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β],
  Function.Injective fun f => ↑f
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] [h : IsManifold I 2 M],
  ContMDiffVectorBundle 1 E (TangentSpace I) I
-- Mathlib.Algebra.Group.Units.Defs
/-- Addition of a `u : AddUnits M` on the right doesn't affect `IsAddUnit`.  -/
AddUnits.isAddUnit_add_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (a : M) (u : AddUnits M), IsAddUnit (a + ↑u) ↔ IsAddUnit a
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The functor `G` has a colimit if `C` has `K`-shaped colimits and `(curry.obj G ⋙ colim)` has a
colimit.  -/
CategoryTheory.Limits.instHasColimitProd : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)],
  CategoryTheory.Limits.HasColimit G
-- Init.Prelude
LE.mk : {α : Type u} → (α → α → Prop) → LE α
-- Aesop.Script.ScriptM
Aesop.recordScriptSteps : {m : Type → Type u_1} → [MonadStateOf (Array Aesop.Script.LazyStep) m] → Array Aesop.Script.LazyStep → m Unit
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- In a flatten of sublists, taking the slice between the indices `A` and `B - 1` gives back the
original sublist of index `i` if `A` is the sum of the lengths of sublists of index `< i`, and
`B` is the sum of the lengths of sublists of index `≤ i`.  -/
List.drop_take_succ_flatten_eq_getElem : ∀ {α : Type u_2} (L : List (List α)) (i : ℕ) (h : i < L.length),
  List.drop (List.take i (List.map List.length L)).sum
      (List.take (List.take (i + 1) (List.map List.length L)).sum L.flatten) =
    L[i]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- A notation for the categorical pullback.  -/
CategoryTheory.Limits.CategoricalPullback.«term_⊡_» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.diag_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Zero α] [inst_2 : One α],
  (SimpleGraph.adjMatrix α G).diag = 0
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The quotient map `(R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span {a})` is surjective.
 -/
Ideal.quotOfMul_surjective : ∀ {R : Type u_1} [inst : CommRing R] {a : R} (I : Ideal R), Function.Surjective ⇑(Ideal.quotOfMul a I)
-- Mathlib.Data.Finset.Prod
Finset.mem_product : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {p : α × β}, p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Mathlib.Data.PNat.Defs
PNat.eq : ∀ {m n : ℕ+}, ↑m = ↑n → m = n
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
GenContFract.squashGCF.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] (g : GenContFract K),
  g.squashGCF 0 =
    match g.s.get? 0 with
    | none => g
    | some gp => { h := g.h + gp.a / gp.b, s := g.s }
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_add_right : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddRightCancelMonoid (N a)] (f g h : Π₀ (a : α), N a), (f + h).neLocus (g + h) = f.neLocus g
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination
of twists of the von Mangoldt function by Dirichlet characters.  -/
ArithmeticFunction.vonMangoldt.residueClass_eq : ∀ {q : ℕ} {a : ZMod q} [NeZero q],
  IsUnit a →
    (fun n => ↑(ArithmeticFunction.vonMangoldt.residueClass a n)) =
      (↑q.totient)⁻¹ • ∑ χ, χ a⁻¹ • fun n => χ ↑n * ↑(ArithmeticFunction.vonMangoldt n)
-- Mathlib.Topology.WithTopology
WithTopology.toTopology_bijective : ∀ {X : Type u_1} (t : TopologicalSpace X), Function.Bijective (WithTopology.toTopology t)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.annotationId? : Lean.Lsp.DeleteFile → Option String
-- Lean.Server.Rpc.Basic
Lean.Lsp.instInhabitedRpcRef.default : Lean.Lsp.RpcRef
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.partDens.eq_1 : ∀ {α : Type u_1} (g : GenContFract α), g.partDens = Stream'.Seq.map GenContFract.Pair.b g.s
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.liftHom_algEquiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial R}
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f)
  {U : Type u_2} [inst_5 : CommRing U] [inst_6 : Algebra R U] (x : U) (hx : (Polynomial.aeval x) f = 0) (z : S),
  (h'.liftHom x hx) ((h.algEquiv h') z) = (h.liftHom x hx) z
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_lt_eq_Ioi : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a : α} [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun x => a < x], {x | a < x} = Finset.Ioi a
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ext : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} {x y : Metric.Snowflaking X α hα₀ hα₁}, x.val = y.val → x = y
-- Lean.Meta.CollectFVars
/-- For each variable in `s.fvarSet`, include its dependencies.  -/
Lean.CollectFVars.State.addDependencies : Lean.CollectFVars.State → Lean.MetaM Lean.CollectFVars.State
-- Mathlib.Data.Finsupp.BigOperators
Multiset.mem_sup_map_support_iff : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : Zero M] {s : Multiset (ι →₀ M)} {x : ι},
  x ∈ (Multiset.map Finsupp.support s).sup ↔ ∃ f ∈ s, x ∈ f.support
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.signExtend_elim : ∀ {v : ℕ} {x : BitVec v} {w : ℕ} (h : v ≤ w),
  BitVec.signExtend w x = BitVec.cast ⋯ ((bif x.msb then -1#(w - v) else 0#(w - v)) ++ x)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_eq_top_of_summable_norm : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), (∀ (r : NNReal), Summable fun n => ‖p n‖ * ↑r ^ n) → p.radius = ⊤
-- Mathlib.Data.Set.Sups
Set.infs_subset : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesIsoSc'_inv_iCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv
      (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) =
    CategoryTheory.CategoryStruct.comp (K.sc' i j k).iCycles h
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- `M × N` is diffeomorphic to `N × M`.  -/
Diffeomorph.prodComm : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_4} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_7} →
                      [inst_6 : TopologicalSpace G] →
                        (I : ModelWithCorners 𝕜 E H) →
                          (J : ModelWithCorners 𝕜 F G) →
                            (M : Type u_9) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  (N : Type u_11) →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        (n : WithTop ℕ∞) → Diffeomorph (I.prod J) (J.prod I) (M × N) (N × M) n
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_appTop_map_eq_zero_of_isAffine_of_isLimit : ∀ {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 : I), AlgebraicGeometry.IsAffine (D.obj i)] (i : I) (s : ↑((D.obj i).presheaf.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (c.π.app i))) s = 0 →
    ∃ j f, (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (D.map f))) s = 0
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Continuity of interval integral with respect to a parameter.
Given `F : X → ℝ → E`, assume each `F x` is ae-measurable on `[a, b]`,
and assume it is bounded by a function integrable on `[a, b]` independent of `x`.
If `(fun x ↦ F x t)` is continuous for almost every `t` in `[a, b]`
then the same holds for `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`.  -/
intervalIntegral.continuous_of_dominated_interval : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3}
  [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {bound : ℝ → ℝ} {a b : ℝ},
  (∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
    (∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → Continuous fun x => F x t) → Continuous fun x => ∫ (t : ℝ) in a..b, F x t ∂μ
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.MonadGetStruct.getStruct : {m : Type → Type} → [self : Lean.Meta.Grind.Arith.Linear.MonadGetStruct m] → m Lean.Meta.Grind.Arith.Linear.Struct
-- Mathlib.Order.Category.LinOrd
LinOrd.hom_inv_apply : ∀ {X Y : LinOrd} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- Choice of a closed complement of `range f`  -/
ContinuousLinearMap.HasLeftInverse.complement : {R : Type u_7} →
  {E : Type u_8} →
    {F : Type u_10} →
      [inst : Ring R] →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : AddCommGroup E] →
            [inst_3 : Module R E] →
              [inst_4 : TopologicalSpace F] →
                [inst_5 : AddCommGroup F] → [inst_6 : Module R F] → {f : E →L[R] F} → f.HasLeftInverse → Submodule R F
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.map₂Left'.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α)
  (h_1 : (bs : List β) → motive [] bs) (h_2 : (a : α) → (as : List α) → motive (a :: as) [])
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)),
  (match a :: as, [] with
    | [], bs => h_1 bs
    | a :: as, [] => h_2 a as
    | a :: as, b :: bs => h_3 a as b bs) =
    h_2 a as
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.hasBasis_nhds_zero : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F],
  (nhds 0).HasBasis (fun SV => Bornology.IsVonNBounded 𝕜₁ SV.1 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.subset_ordConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α} {t : Set α} [h : s.OrdConnected],
  x ∈ s → s ⊆ t → s ⊆ t.ordConnectedComponent x
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.stuck.sizeOf_spec : ∀ (val : Lean.Expr), sizeOf (Lean.Meta.ReduceMatcherResult.stuck val) = 1 + sizeOf val
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.subsingleton : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α},
  s.Subsingleton → eVariationOn f s = 0
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanHalfSpace.pathConnectedSpace : ∀ {n : ℕ} [inst : NeZero n], PathConnectedSpace (EuclideanHalfSpace n)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_eq_zero_ae_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
-- Mathlib.RingTheory.Unramified.Field
/-- If `A = K[X]/⟨p⟩` is unramified at some prime `Q`, then the minpoly of `X` in `κ(Q)`
only divides `p` once.  -/
Algebra.IsUnramifiedAt.not_minpoly_sq_dvd : ∀ {K : Type u_1} {A : Type u_2} [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] (Q : Ideal A)
  [inst_3 : Q.IsPrime] [Algebra.IsUnramifiedAt K Q] (x : A) (p : Polynomial K),
  Ideal.span {p} = RingHom.ker (Polynomial.aeval x).toRingHom →
    Function.Surjective ⇑(Polynomial.aeval x) → ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ p
-- Mathlib.Algebra.Order.Ring.Abs
sq_le_sq' : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  -b ≤ a → a ≤ b → a ^ 2 ≤ b ^ 2
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonLeanClientCapabilities.toJson : Lean.Lsp.LeanClientCapabilities → Lean.Json
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.toPartialResultParams : Lean.Lsp.DocumentColorParams → Lean.Lsp.PartialResultParams
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- **Alias** of `Function.Injective.map_atTop_finsetSum_eq`. -/
Function.Injective.map_atTop_finset_sum_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {g : α → β},
  Function.Injective g →
    ∀ {f : β → M},
      (∀ x ∉ Set.range g, f x = 0) →
        Filter.map (fun s => ∑ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun s => ∑ i ∈ s, f i) Filter.atTop
-- Init.System.IOError
/-- An argument was the wrong type (e.g. a directory when a file was required).

This corresponds to the POSIX errors `EISDIR`, `EBADMSG`, and `ENOTDIR`.
 -/
IO.Error.inappropriateType : Option String → UInt32 → String → IO.Error
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Adjunction.map_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [G.PreservesEpimorphisms] (P : C),
  CategoryTheory.Projective P → CategoryTheory.Projective (F.obj P)
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.oreMin.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r : R) (s : ↥S),
  AddOreLocalization.oreMin r s = AddOreLocalization.AddOreSet.oreMin r s
-- Lean.InternalExceptionId
Lean.instBEqInternalExceptionId.beq : Lean.InternalExceptionId → Lean.InternalExceptionId → Bool
-- Mathlib.GroupTheory.Focal
AddSubgroup.addCommutator_le_focalAddSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), addCommutator ↥H ≤ H.focalAddSubgroupOf
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (φK : h₁.K ⟶ h₂.K) (φH : h₁.H ⟶ h₂.H)
  (commi :
    autoParam (CategoryTheory.CategoryStruct.comp φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commi._autoParam)
  (commf' :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.f' φK = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f')
      CategoryTheory.ShortComplex.LeftHomologyMapData.commf'._autoParam)
  (commπ :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.π φH = CategoryTheory.CategoryStruct.comp φK h₂.π)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commπ._autoParam)
  (φK_1 : h₁.K ⟶ h₂.K) (φH_1 : h₁.H ⟶ h₂.H)
  (commi_1 :
    autoParam (CategoryTheory.CategoryStruct.comp φK_1 h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commi._autoParam)
  (commf'_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.f' φK_1 = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f')
      CategoryTheory.ShortComplex.LeftHomologyMapData.commf'._autoParam)
  (commπ_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.π φH_1 = CategoryTheory.CategoryStruct.comp φK_1 h₂.π)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commπ._autoParam),
  ({ φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ } =
      { φK := φK_1, φH := φH_1, commi := commi_1, commf' := commf'_1, commπ := commπ_1 }) =
    (φK = φK_1 ∧ φH = φH_1)
-- Mathlib.LinearAlgebra.Matrix.MvPolynomial
/-- Evaluating the generic determinant polynomial `det (mvPolynomialX m m R)` at a point `s`
gives the determinant of the matrix obtained by substituting `s`.  -/
Matrix.eval_det_mvPolynomialX : ∀ (m : Type u_1) (R : Type u_3) [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : CommRing R] (s : m × m → R),
  (MvPolynomial.eval s) (Matrix.mvPolynomialX m m R).det = (Matrix.of fun i j => s (i, j)).det
-- Mathlib.Order.Hom.Bounded
TopHomClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : Top α] [inst_1 : Top β]
  [inst_2 : FunLike F α β], (∀ (f : F), f ⊤ = ⊤) → TopHomClass F α β
-- Mathlib.Data.Sum.Order
Sum.lt_def : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α ⊕ β},
  a < b ↔ Sum.LiftRel (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) a b
-- Std.Internal.Do.ExceptPost
/-- The trivial complete lattice on `EPost.Nil`.  -/
Std.Internal.Do.instCompleteLatticeNil : Lean.Order.CompleteLattice EPost⟨⟩
-- Mathlib.Data.PFun
PFun.preimage_union : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : Set β), f.preimage (s ∪ t) = f.preimage s ∪ f.preimage t
-- Mathlib.Data.Finsupp.Interval
Finsupp.Icc_eq : ∀ {ι : Type u_1} {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] [inst_4 : DecidableEq α] (f g : ι →₀ α),
  Finset.Icc f g = (f.support ∪ g.support).finsupp ⇑(f.rangeIcc g)
-- Mathlib.Algebra.Algebra.Spectrum.Pi
/-- The equivalence between pre-quasiregular elements of an indexed product and the indexed product
of pre-quasiregular elements.  -/
PreQuasiregular.toPi : {ι : Type u_1} →
  (κ : ι → Type u_5) →
    [inst : (i : ι) → NonUnitalSemiring (κ i)] → PreQuasiregular ((i : ι) → κ i) ≃* ((i : ι) → PreQuasiregular (κ i))