mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_3.splitter : (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) →
  (x x_1 : Lean.Grind.CommRing.Mon) →
    ((x : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit x) →
      ((x : Lean.Grind.CommRing.Mon) →
          (x = Lean.Grind.CommRing.Mon.unit → False) → motive x Lean.Grind.CommRing.Mon.unit) →
        ((pw₁ : Lean.Grind.CommRing.Power) →
            (m₁ : Lean.Grind.CommRing.Mon) →
              (pw₂ : Lean.Grind.CommRing.Power) →
                (m₂ : Lean.Grind.CommRing.Mon) →
                  motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
          motive x x_1
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
ContinuousLinearMap.apply.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_4} (Fₗ : Type u_7) [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ],
  ContinuousLinearMap.apply 𝕜 Fₗ = (ContinuousLinearMap.id 𝕜 (E →L[𝕜] Fₗ)).flip
-- Init.Data.BitVec.Lemmas
BitVec.replicate_one : ∀ {w : ℕ} {x : BitVec w}, BitVec.replicate 1 x = BitVec.cast ⋯ x
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g y` is invertible for all `y : S`, the homomorphism induced from
`N` to `P` sending `z : N` to `g x * (g y)⁻¹`, where `(x, y) : M × S` are such that
`z = f x * (f y)⁻¹`.  -/
Submonoid.LocalizationMap.lift : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} →
            [inst_2 : CommMonoid P] → S.LocalizationMap N → {g : M →* P} → (∀ (y : ↥S), IsUnit (g ↑y)) → N →* P
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofNat_lt_toENat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n < Cardinal.toENat c ↔ OfNat.ofNat n < c
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_self_iff : ∀ {x : ℝ}, √x ≤ x ↔ x = 0 ∨ 1 ≤ x
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsCofibrant X] [HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.LeftHomotopyRel f g ↔ HomotopicalAlgebra.RightHomotopyRel f g
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Icc_sub_one_right_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α),
  Set.Icc a (b - 1) = Set.Ico a b
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F` reflects isomorphisms (G6).  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.PreGaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  F.ReflectsIsomorphisms
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup_injective : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousAdd G],
  Function.Injective OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroup
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [inst : ENorm ε] {μ : MeasureTheory.Measure α},
  p ≠ 0 → p ≠ ⊤ → ∀ {f : α → ε}, MeasureTheory.eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
-- Mathlib.Algebra.Group.Prod
Prod.instAddLeftCancelMonoid : {M : Type u_3} → {N : Type u_4} → [AddLeftCancelMonoid M] → [AddLeftCancelMonoid N] → AddLeftCancelMonoid (M × N)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
FiberBundle.exists_contMDiffOn_extend : ∀ {𝕜 : 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] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  {V : M → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F] {k : WithTop ℕ∞}
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] [ContMDiffVectorBundle k F V I] {x₀ : M}
  (σ₀ : V x₀),
  ∃ s ∈ nhds x₀, ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x' => ⟨x', FiberBundle.extend F σ₀ x'⟩) s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g) (e : Y ⟶ Z) (he : CategoryTheory.CategoryStruct.comp g e = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelIsoOfEq h).hom
      (CategoryTheory.Limits.cokernel.desc g e he) =
    CategoryTheory.Limits.cokernel.desc f e ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.pairwise_fst_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → List.Pairwise (fun a b => (a.fst == b.fst) = false) l
-- Mathlib.Analysis.Calculus.VectorField
/-- Version of `lieBracketWithin_congr` in which one assumes that the point belongs to the
given set.  -/
VectorField.lieBracketWithin_congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  Set.EqOn V₁ V s →
    Set.EqOn W₁ W s → x ∈ s → VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_roi : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) = (Std.Slice.toArray xs).extract (lo + 1)
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), deriv Neg.neg x = -1
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_sub_eq_nnnorm_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E) {y : E}, ‖y‖₊ = 0 → ‖x - y‖₊ = ‖x‖₊
-- Mathlib.Data.Nat.GCD.Basic
Nat.div_dvd_div_left : ∀ {n m k : ℕ}, m ∣ k → n ∣ m → k / m ∣ k / n
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.mk_smul_toLp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : M) {f : α → E} (hf : MeasureTheory.MemLp f p μ),
  DomMulAct.mk c • MeasureTheory.MemLp.toLp f hf = MeasureTheory.MemLp.toLp (fun x => f (c • x)) ⋯
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.machine : Std.Internal.UV.System.UnameInfo → String
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_le_maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.maxKey? = some km →
    (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey?.get ⋯ = kmi → (compare km kmi).isLE = true
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- The selfadjoint element obtained by taking the argument (using the principal branch and the
continuous functional calculus) of a unitary whose spectrum does not contain `-1`. This returns
`0` if the principal branch of the logarithm is not continuous on the spectrum of the unitary
element.  -/
Unitary.argSelfAdjoint : {A : Type u_1} → [inst : CStarAlgebra A] → ↥(unitary A) → ↥(selfAdjoint A)
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.instRespectsRightOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C)
  [Q.IsClosedUnderIsomorphisms],
  (CategoryTheory.MorphismProperty.ofObjectProperty P Q).RespectsRight (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.homEquivOfIsLeftKanExtension_apply_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F' ⟶ G) (X : C),
  ((F'.homEquivOfIsLeftKanExtension α G) β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app (L.obj X))
-- Lean.Parser.Extra
Lean.Parser.withSetOptionValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mem_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} {x : M}, x ∈ MonoidHom.mker f ↔ f x = 1
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue : Type
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.eigenspace_zero : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M),
  f.eigenspace 0 = LinearMap.ker f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.filterMap_equiv_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, t.WF → (Std.TreeMap.Raw.filterMap (fun k v => some (f k v)) t).Equiv (Std.TreeMap.Raw.map f t)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_eq_rankOne_iff_comm : ∀ {𝕜 : Type u_4} [inst : RCLike 𝕜] {F : Type u_8} {H : Type u_9} [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace 𝕜 F] [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H] {a c : F} {b d : H},
  ((InnerProductSpace.rankOne 𝕜) a) b = ((InnerProductSpace.rankOne 𝕜) c) d ↔
    ((InnerProductSpace.rankOne 𝕜) b) a = ((InnerProductSpace.rankOne 𝕜) d) c
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
isInvertible_mfderivWithin_extChartAt_symm : ∀ {𝕜 : 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] [IsManifold I 1 M] {x : M} {y : E},
  y ∈ (extChartAt I x).target → (mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y).IsInvertible
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.mk.sizeOf_spec : ∀ (binders : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) (argNames targetNames : Array Lean.Name)
  (targetType : Lean.Term),
  sizeOf { binders := binders, argNames := argNames, targetNames := targetNames, targetType := targetType } =
    1 + sizeOf binders + sizeOf argNames + sizeOf targetNames + sizeOf targetType
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_inv_inr_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr.unop h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.nextCoeff_prod : ∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] (s : Finset ι) (f : ι → Polynomial R),
  (∀ i ∈ s, (f i).Monic) → (∏ i ∈ s, f i).nextCoeff = ∑ i ∈ s, (f i).nextCoeff
-- Lean.Parser.Extension
/-- Helper environment extension that gives us access to built-in aliases in pure parser functions.
 -/
Lean.Parser.aliasExtension : Lean.EnvExtension (Lean.NameMap Lean.Parser.ParserAliasValue)
-- Mathlib.Algebra.Group.Conj
conj_mul : ∀ {α : Type u} [inst : Group α] {a b c : α}, b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹
-- Mathlib.Algebra.Order.UpperLower
UpperSet.addCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  UpperSet.addCommSemigroup = Function.Injective.addCommSemigroup SetLike.coe ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- An orthonormal set is linearly independent.  -/
Orthonormal.linearIndependent : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → LinearIndependent 𝕜 v
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem_toArray_roo : ∀ {m n : ℤ} {i : ℕ} (_h : i < (m<...n).toArray.size), (m<...n).toArray[i] = m + 1 + ↑i
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.count_of : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α), (FreeAddMonoid.count x) (FreeAddMonoid.of y) = Pi.single x 1 y
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.boundaries₁_le_cycles₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.boundaries₁ A ≤ groupHomology.cycles₁ A
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instAdd.eq_1 : ∀ {E : Type u_3} [inst : Group E],
  GroupSeminorm.instAdd = { add := fun p q => { toFun := fun x => p x + q x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instProductivenessRelation : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → Std.Iterators.ProductivenessRelation (Std.Rxi.Iterator α) Id
-- Mathlib.RingTheory.Congruence.Defs
/-- Additive congruence relations are closed under addition  -/
RingCon.add' : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (self : RingCon R) {w x y z : R},
  self.toSetoid w x → self.toSetoid y z → self.toSetoid (w + y) (x + z)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_bot : ∀ {V : Type u}, ⊥.edgeSet = ∅
-- Lean.Parser.Term.Doc
/-- Returns the recommended spellings associated with the given declaration name.  -/
Lean.Parser.Term.Doc.getRecommendedSpellingsForName : Lean.Environment → Lean.Name → Array Lean.Parser.Term.Doc.RecommendedSpelling
-- Mathlib.Logic.Equiv.Basic
/-- A subtype of a sigma-type is a sigma-type over a subtype.  -/
Equiv.subtypeSigmaEquiv : {α : Type u_9} → (p : α → Type v) → (q : α → Prop) → { y // q y.fst } ≃ (x : Subtype q) × p ↑x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.Extension.conjugate_comp_ne : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] {ψ : K →+* ℂ} [inst_2 : Algebra K L]
  (φ : NumberField.ComplexEmbedding.Extension L ψ),
  ¬NumberField.ComplexEmbedding.IsReal ψ → (NumberField.ComplexEmbedding.conjugate ↑φ).comp (algebraMap K L) ≠ ψ
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of `le_compl_comm`. -/
le_compl_iff_le_compl : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ b ≤ aᶜ
-- Mathlib.Probability.Distributions.Beta
/-- The pdf of the beta distribution integrates to 1.  -/
ProbabilityTheory.lintegral_betaPDF_eq_one : ∀ {α β : ℝ}, 0 < α → 0 < β → ∫⁻ (x : ℝ), ProbabilityTheory.betaPDF α β x = 1
-- Mathlib.Geometry.Euclidean.Projection
/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector is a
multiple of the result of subtracting a point's orthogonal projection
from that point.  -/
Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  (s : Affine.Simplex 𝕜 P n) {p₁ : P} (p₂ : P) (r : 𝕜) (hp : p₁ ∈ affineSpan 𝕜 (Set.range s.points)),
  s.orthogonalProjectionSpan (r • (p₂ -ᵥ ↑(s.orthogonalProjectionSpan p₂)) +ᵥ p₁) = ⟨p₁, hp⟩
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.instSmallPrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C},
  P.precoverage.Small
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_add : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {p q : MvPolynomial σ R}
  (f : R →+* S₁) (g : σ → S₁), MvPolynomial.eval₂ f g (p + q) = MvPolynomial.eval₂ f g p + MvPolynomial.eval₂ f g q
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_empty : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ}, Monoid.PushoutI.NormalWord.empty.prod = 1
-- Init.CbvSimproc
Lean.Parser.cbvSimprocPatternBuiltin : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} {l : List α} {k : α}
  {fallback : Unit}, Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l) k fallback = ()
-- Mathlib.Topology.Sheaves.Presheaf
/-- An equality of continuous maps induces a natural isomorphism between the pushforwards of a presheaf
along those maps.
 -/
TopCat.Presheaf.pushforwardEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} →
      {f g : X ⟶ Y} →
        f = g →
          (ℱ : TopCat.Presheaf C X) → (TopCat.Presheaf.pushforward C f).obj ℱ ≅ (TopCat.Presheaf.pushforward C g).obj ℱ
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivWithinAt_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜), HasDerivWithinAt Neg.neg (-1) s x
-- Mathlib.Data.Finset.Sups
Finset.image_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (s : Finset α) [inst_1 : DecidableEq α], Finset.image compl s = s.compls
-- Init.System.IO
IO.Process.Stdio.noConfusionType : Sort v✝ → IO.Process.Stdio → IO.Process.Stdio → Sort v✝
-- Mathlib.Analysis.Convex.Strict
/-- The preimage of a strictly convex set under an affine map is strictly convex.  -/
StrictConvex.affine_preimage : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : TopologicalSpace F] [inst_4 : AddCommGroup E] [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 F] {s : Set F},
  StrictConvex 𝕜 s → ∀ {f : E →ᵃ[𝕜] F}, Continuous ⇑f → Function.Injective ⇑f → StrictConvex 𝕜 (⇑f ⁻¹' s)
-- Init.SimpLemmas
let_body_congr : ∀ {α : Sort u} {β : α → Sort v} {b b' : (a : α) → β a} (a : α),
  (∀ (x : α), b x = b' x) →
    (have x := a;
      b x) =
      have x := a;
      b' x
-- Mathlib.Order.Preorder.Finsupp
Finsupp.support_sup_union_support_inf : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : Lattice M] (f g : ι →₀ M) [inst_2 : DecidableEq ι],
  (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support
-- Mathlib.Topology.Algebra.FilterBasis
/-- Build a module filter basis from compatible ring and additive group filter bases.  -/
ModuleFilterBasis.ofBases : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (BR : RingFilterBasis R) →
            (BM : AddGroupFilterBasis M) →
              (∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U) →
                (∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x => x₀ • x) ⁻¹' U) →
                  (∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x => x • m₀) ⁻¹' U) → ModuleFilterBasis R M
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_densityProcess_aux : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) {s : Set β},
  MeasurableSet s →
    Measurable fun p =>
      (κ p.1) (MeasurableSpace.countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (MeasurableSpace.countablePartitionSet n p.2)
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.prod_eq_of_mem_finMulAntidiag : ∀ {d n : ℕ} {f : Fin d → ℕ}, f ∈ d.finMulAntidiag n → ∏ i, f i = n
-- Mathlib.Data.Set.Image
Set.image_inter_on : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α},
  (∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y) → f '' (s ∩ t) = f '' s ∩ f '' t
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber_le_encard_self : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} (A : Set X), Metric.packingNumber ε A ≤ A.encard
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ≫ θ` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalComp : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Lean.CoreM
/-- Adjusts the `namePrefix` of `getDeclNGen` to the given name and resets the nested counter.
 -/
Lean.withDeclNameForAuxNaming : {m : Type → Type} → {α : Type} → [Monad m] → [MonadFinally m] → [Lean.MonadDeclNameGenerator m] → Lean.Name → m α → m α
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} [inst_2 : SizeOf C] [inst_3 : SizeOf J] (diag : CategoryTheory.Functor J C)
  (ι : diag ⟶ (CategoryTheory.Functor.const J).obj X) (isColimit : CategoryTheory.Limits.IsColimit { pt := X, ι := ι }),
  sizeOf { diag := diag, ι := ι, isColimit := isColimit } = 1 + sizeOf diag + sizeOf ι + sizeOf isColimit
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.intervalIntegrable_norm_iff : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {a b : ℝ},
  MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) →
    (IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.realSize_deleteMin : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {s' s : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.deleteMin le s = some (a, s') → s.realSize = s'.realSize + 1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toBoundedContinuousFunction_apply : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F) (x : E), f.toBoundedContinuousFunction x = f x
-- Lean.Parser.Term
Lean.Parser.Term.generalizingParam.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Convex.PathConnected
Path.add.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : ContinuousAdd X] {a₁ b₁ a₂ b₂ : X}
  (γ₁ γ₁_1 : Path a₁ b₁), γ₁ = γ₁_1 → ∀ (γ₂ γ₂_1 : Path a₂ b₂), γ₂ = γ₂_1 → γ₁.add γ₂ = γ₁_1.add γ₂_1