mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- A smooth bump function around `c i`.  -/
SmoothBumpCovering.toFun : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : optParam (Set M) Set.univ} →
                        (self : SmoothBumpCovering ι I M s) → (i : ι) → SmoothBumpFunction I (self.c i)
-- Init.Core
PUnit.eq_punit : ∀ (a : PUnit.{u_1}), a = PUnit.unit
-- Mathlib.Algebra.Order.Group.PosPart
sub_abs_eq_neg_two_nsmul_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a : α), a - |a| = -(2 • a⁻)
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.CanonM.run : {α : Type} →
  Lean.Meta.CanonM α →
    optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.instances →
      optParam Lean.Meta.Canonicalizer.State { } → Lean.MetaM (α × Lean.Meta.Canonicalizer.State)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.not_realize_bot : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M], ¬M ⊨ ⊥
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β}, f.NeBot → g.NeBot → (f • g).NeBot
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₀.X₁` is the kernel of `v₁₂.τ₁ : L₁.X₁ ⟶ L₂.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₀τ₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.v₀₁.τ₁ ⋯)
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLT.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α],
  (∀ ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, a • b₁ < a • b₂ → b₁ < b₂) → PosSMulReflectLT α β
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instZero : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Zero (LieSubalgebra R L)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.meas_le_of_le_of_forall_le_meas_thickening_add : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] {ε₁ ε₂ : ENNReal}
  (μ ν : MeasureTheory.Measure Ω),
  ε₁ ≤ ε₂ → ∀ {B : Set Ω}, μ B ≤ ν (Metric.thickening ε₁.toReal B) + ε₁ → μ B ≤ ν (Metric.thickening ε₂.toReal B) + ε₂
-- Mathlib.CategoryTheory.Sites.EpiMono
/-- Given a functorial surjective/injective factorizations of morphisms in a concrete
category `A`, this is the induced functorial locally surjective/locally injective
factorization of morphisms in the category `Sheaf J A`.  -/
CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {FA : A → A → Type u_1} →
            {CA : A → Type w} →
              [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory A FA] →
                  [J.WEqualsLocallyBijective A] →
                    CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A →
                      [CategoryTheory.HasWeakSheafify J A] →
                        (CategoryTheory.Sheaf.locallySurjective J A).FunctorialFactorizationData
                          (CategoryTheory.Sheaf.locallyInjective J A)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.IsStrictSegal.hom_ext : ∀ {n : ℕ} {X Y : SSet.Truncated (n + 1)} [Y.IsStrictSegal] {f g : X ⟶ Y},
  (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := ⋯ })),
      (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { obj := { len := 1 }, property := ⋯ }))) x =
        (CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { obj := { len := 1 }, property := ⋯ }))) x) →
    f = g
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
integralClosure.isIntegralClosure : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  IsIntegralClosure (↥(integralClosure R A)) R A
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_def : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (a : MvPowerSeries τ S) (f : PowerSeries R), PowerSeries.subst a f = MvPowerSeries.subst (fun x => a) f
-- Mathlib.Data.Finset.Union
Finset.disjoint_disjiUnion_left : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → Finset β) (hf : (↑s).PairwiseDisjoint f) (t : Finset β),
  Disjoint (s.disjiUnion f hf) t ↔ ∀ i ∈ s, Disjoint (f i) t
-- Mathlib.Logic.Equiv.Prod
/-- If `α` is a subsingleton, then it is equivalent to `α × α`.  -/
subsingletonProdSelfEquiv : {α : Type u_9} → [Subsingleton α] → α × α ≃ α
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMin'_all : ∀ {α : Type u_1} {P : α → Prop} (t : Ordnode α) (x : α), Ordnode.All P t → P x → P (t.findMin' x)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcReleaseParams : Lean.ToJson Lean.Lsp.RpcReleaseParams
-- Init.Data.String.Subslice
String.Slice.Subslice.mk.sizeOf_spec : ∀ {s : String.Slice} (startInclusive endExclusive : s.Pos)
  (startInclusive_le_endExclusive : startInclusive ≤ endExclusive),
  sizeOf
      { startInclusive := startInclusive, endExclusive := endExclusive,
        startInclusive_le_endExclusive := startInclusive_le_endExclusive } =
    1 + sizeOf startInclusive + sizeOf endExclusive + sizeOf startInclusive_le_endExclusive
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.restrictScalars_obj : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R')
  (M' : PresheafOfModules R'), (PresheafOfModules.restrictScalars α).obj M' = M'.restrictScalarsObj α
-- Mathlib.Data.PNat.Xgcd
/-- `IsReduced'` is an alternative of `IsReduced`.  -/
PNat.XgcdType.IsReduced' : PNat.XgcdType → Prop
-- Mathlib.LinearAlgebra.Projection
Submodule.existsUnique_add_of_isCompl_prod : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E},
  IsCompl p q → ∀ (x : E), ∃! u, ↑u.1 + ↑u.2 = x
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.coverEntropyEntourage_le_netEntropyEntourage : ∀ {X : Type u_1} {U : SetRel X X} (T : X → X) (F : Set X) [U.IsRefl] [U.IsSymm],
  Dynamics.coverEntropyEntourage T F (U.comp U) ≤ Dynamics.netEntropyEntourage T F U
-- Aesop.Forward.RuleInfo
/-- Construct a `ForwardRuleInfo` for the theorem `thm`.  -/
Aesop.ForwardRuleInfo.ofExpr : Lean.Expr → Option Aesop.RulePattern → Aesop.UnorderedArraySet Aesop.PremiseIndex → Lean.MetaM Aesop.ForwardRuleInfo
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_mul_left : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x, y - z * x} = Ideal.span {x, y}
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.map.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : PartialOrder X] [inst_1 : PartialOrder Y]
  (s : PartialOrder.NonemptyFiniteChains X) (f : X →o Y),
  s.map f = { finset := Finset.image (⇑f) s.finset, nonempty := ⋯, comparable := ⋯ }
-- Mathlib.Order.Defs.Unbundled
instIsTransOfTrans : ∀ {α : Sort u_1} {r : α → α → Prop} [Trans r r r], IsTrans α r
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is maximized when `f` and
`g` monovary together on `s`. Stated by permuting the entries of `g`.  -/
MonovaryOn.sum_mul_comp_perm_le_sum_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i * g (σ i) ≤ ∑ i ∈ s, f i * g i
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.IterM.step_append.match_1.eq_2 : ∀ {α₁ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_empty : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M), v.restrict ∅ = 0
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.isNoetherianRing : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [h : Algebra.FiniteType R S] [IsNoetherianRing R], IsNoetherianRing S
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.mk_id : ∀ {α : Sort u_1}, { toFun := id, inj' := ⋯ } = Function.Embedding.refl α
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.add_compat_left : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (a + c) (b + c)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instSub : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : AddGroup γ] → [IsTopologicalAddGroup γ] → Sub (α →ₘ[μ] γ)
-- Std.Time.Format.Modifier
Std.Time.Modifier.S.inj : ∀ {presentation presentation_1 : Std.Time.Fraction},
  Std.Time.Modifier.S presentation = Std.Time.Modifier.S presentation_1 → presentation = presentation_1
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_zero_eq_mul_div' : ∀ {R : Type u_1} {a b : R} [inst : Field R], a ≠ 1 → ∀ (n : ℕ), arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₄_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.ComposableArrows C 4),
  ∃ X₀ X₁ X₂ X₃ X₄ f₀ f₁ f₂ f₃, X = CategoryTheory.ComposableArrows.mk₄ f₀ f₁ f₂ f₃
-- Qq.Macro
_private.Qq.Macro.0.Qq.Impl.push : {m : Type → Type u_1} →
  [Monad m] → Lean.Syntax → Lean.Syntax → Lean.Syntax → StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Unit
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 500 status code.
 -/
Std.Http.Response.internalServerError : Std.Http.Response.Builder
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_natCast : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] (n : ℕ), (↑n).toAddMonoidAlgebra = ↑n
-- Init.Data.String.Defs
String.toSubstring : String → Substring.Raw
-- Lean.DocString.Markdown
/-- Renderers registered in the current module.  -/
Lean.Doc.MdRendererState.current : Lean.Doc.MdRendererState → Lean.NameMap Lean.Name
-- Mathlib.CategoryTheory.Limits.FunctorToTypes
CategoryTheory.FunctorToTypes.jointly_surjective' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type w)))
  [inst_2 : ∀ (k : K), CategoryTheory.Limits.HasColimit (F.flip.obj k)] (k : K)
  (x : (CategoryTheory.Limits.colimit F).obj k),
  ∃ j y, x = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.colimit.ι F j).app k)) y
-- Mathlib.Order.Zorn
zorn_subset : ∀ {α : Type u_1} (S : Set (Set α)),
  (∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) → ∃ m, Maximal (fun x => x ∈ S) m
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural transformation `t.truncLE a ⟶ t.truncLE b` when `a ≤ b`.  -/
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → (a b : ℤ) → a ≤ b → (t.truncLE a ⟶ t.truncLE b)
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_ne_of_le` -/
ssubset_of_ne_of_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ≠ b → a ⊆ b → a ⊂ b
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableAtFilter_congr : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f g : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  f =ᵐ[μ] g → (MeasureTheory.IntegrableAtFilter f l μ ↔ MeasureTheory.IntegrableAtFilter g l μ)
-- Lean.DocString.Links
/-- The manual domain for error explanations.

We expose this because it is used to populate the URL of the error message description widget.
 -/
Lean.errorExplanationManualDomain : String
-- Mathlib.CategoryTheory.LiftingProperties.Limits
CategoryTheory.instHasLiftingPropertyMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} {A B : J → C}
  [inst_1 : CategoryTheory.Limits.HasProduct A] [inst_2 : CategoryTheory.Limits.HasProduct B] (f : (j : J) → A j ⟶ B j)
  {X Y : C} (p : X ⟶ Y) [∀ (j : J), CategoryTheory.HasLiftingProperty p (f j)],
  CategoryTheory.HasLiftingProperty p (CategoryTheory.Limits.Pi.map f)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The natural isomorphism between two functors out of the walking pair, specified by its
components.  -/
CategoryTheory.Limits.mapPairIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} →
      (F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅
          G.obj { as := CategoryTheory.Limits.WalkingPair.left }) →
        (F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅
            G.obj { as := CategoryTheory.Limits.WalkingPair.right }) →
          (F ≅ G)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
CommRingCat.FilteredColimits.instNontrivialCarrierColimitOfIsFilteredOrEmptyOfObj : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  [CategoryTheory.IsFilteredOrEmpty J] [inst_2 : CategoryTheory.Limits.HasColimit F] [∀ (i : J), Nontrivial ↑(F.obj i)],
  Nontrivial ↑(CategoryTheory.Limits.colimit F)
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ : MvPowerSeries σ R}, φ ≠ 0 → ∃ d, φ.lexOrder = ↑(toLex d)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk'.inj : ∀ {X : SSet} {A : X.Subcomplex} {toN : X.N} {notMem : toN.simplex ∉ A.obj (Opposite.op { len := toN.dim })}
  {toN_1 : X.N} {notMem_1 : toN_1.simplex ∉ A.obj (Opposite.op { len := toN_1.dim })},
  { toN := toN, notMem := notMem } = { toN := toN_1, notMem := notMem_1 } → toN = toN_1
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.map_units_map_submonoid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Sₘ : Type u_5) [inst_3 : CommSemiring Sₘ] [inst_4 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_5 : Algebra R Sₘ] [IsScalarTower R S Sₘ] (y : ↥M),
  IsUnit ((algebraMap R Sₘ) ↑y)
-- Init.Data.Array.Basic
/-- Returns the size of the array as a platform-native unsigned integer.

This is a low-level version of `Array.size` that directly queries the runtime system's
representation of arrays. While this is not provable, `Array.usize` always returns the exact size of
the array since the implementation only supports arrays of size less than `USize.size`.
 -/
Array.usize : {α : Type u} → Array α → USize
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toNat = n % 2 ^ 16
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of seminormed groups, using the sup norm.  -/
Pi.normedAddCommGroup : {ι : Type u_1} →
  {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → NormedAddCommGroup (G i)] → NormedAddCommGroup ((i : ι) → G i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey_modifyKey_eq_maxKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {he : (Std.Internal.List.Const.modifyKey k f l).isEmpty = false},
      Std.Internal.List.maxKey (Std.Internal.List.Const.modifyKey k f l) he = Std.Internal.List.maxKey l ⋯
-- Mathlib.Topology.UniformSpace.Basic
instTopUniformSpace : {α : Type ua} → Top (UniformSpace α)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.leftAdjointOfEquiv_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (he :
    ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
      (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g))
  {X X' : C} (f : X ⟶ X'),
  (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).map f =
    (e X (F_obj X')).symm
      (CategoryTheory.CategoryStruct.comp f ((e X' (F_obj X')) (CategoryTheory.CategoryStruct.id (F_obj X'))))
-- Mathlib.Analysis.Normed.Group.FunctionSeries
tendstoUniformlyOn_tsum_nat_eventually : ∀ {α : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → α → F} {u : ℕ → ℝ},
  Summable u →
    ∀ {s : Set α},
      (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ s, ‖f n x‖ ≤ u n) →
        TendstoUniformlyOn (fun N x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' (n : ℕ), f n x) Filter.atTop s
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.eq_from : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : Y ⟶ X),
  f = h.from_ Y
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitor_inv_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b}
  (h : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp η
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) h)
-- Init.Data.Slice.Array.Lemmas
Subarray.size_mkSlice_rci : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = Std.Slice.size xs - lo
-- Lean.Meta.AppBuilder
Lean.Meta.mkImpCongrCtx : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.instSubsingletonOfMulArchimedean : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] [MulArchimedean M],
  Subsingleton (FiniteMulArchimedeanClass M)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- If a scalar is central, then its right action is measurable when its left action is.  -/
MeasurableSMul.op : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace α] [inst_2 : SMul M α]
  [inst_3 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableSMul M α], MeasurableSMul Mᵐᵒᵖ α
-- Mathlib.Data.Sum.Basic
Sum.elim_update_right : ∀ {α : Type u} {β : Type v} {γ : Sort u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → γ) (g : β → γ)
  (b : β) (x : γ), Sum.elim f (Function.update g b x) = Function.update (Sum.elim f g) (Sum.inr b) x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instInhabited : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → Inhabited (Π₀ (i : ι), β i)
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
/-- The generating trivial cofibrations: this is the family of morphisms in `SSet`
which consists of horn inclusions `Λ[n, i].ι : Λ[n, i] ⟶ Δ[n]` (for positive `n`).  -/
SSet.modelCategoryQuillen.J : CategoryTheory.MorphismProperty SSet
-- Mathlib.Algebra.Polynomial.Degree.CardPowDegree
AbsoluteValue.mk.congr_simp : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (toMulHom toMulHom_1 : R →ₙ* S) (e_toMulHom : toMulHom = toMulHom_1) (nonneg' : ∀ (x : R), 0 ≤ toMulHom.toFun x)
  (eq_zero' : ∀ (x : R), toMulHom.toFun x = 0 ↔ x = 0)
  (add_le' : ∀ (x y : R), toMulHom.toFun (x + y) ≤ toMulHom.toFun x + toMulHom.toFun y),
  { toMulHom := toMulHom, nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' } =
    { toMulHom := toMulHom_1, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.HomologyData.map_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.HomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.left.IsPreservedBy F]
  [inst_6 : h.right.IsPreservedBy F], (h.map F).left = h.left.map F
-- Mathlib.Data.Rat.Cast.CharZero
Rat.cast_zpow : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α] (p : ℚ) (n : ℤ), ↑(p ^ n) = ↑p ^ n
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- The equivalence of categories `(CochainComplex C ℤ)ᵒᵖ ≌ CochainComplex Cᵒᵖ ℤ`.  -/
CochainComplex.opEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (CochainComplex C ℤ)ᵒᵖ ≌ CochainComplex Cᵒᵖ ℤ
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.getCommRingId?.goQ? : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.insert : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)],
  MeasureTheory.NullMeasurableSet s μ → ∀ (a : α), MeasureTheory.NullMeasurableSet (insert a s) μ
-- Mathlib.Order.Interval.Multiset
Multiset.card_Ioo_eq_card_Ico_sub_one : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Multiset.Ioo a b).card = (Multiset.Ico a b).card - 1
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.dvd_of_le : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x y : O}, v ((algebraMap O F) x) ≤ v ((algebraMap O F) y) → y ∣ x