mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))),
  (s.reindex e).excenterWeightsUnnorm signs = s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm
-- Lean.Parser.Basic
Lean.Parser.instAndThenParserFn : AndThen Lean.Parser.ParserFn
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The additive `v`-adic valuation of `r : R` is the exponent of `v` in the factorization of the
ideal `(r)`, if `r` is nonzero, or infinity, if `r = 0`. `intValuationDef` is the corresponding
multiplicative valuation.  -/
IsDedekindDomain.HeightOneSpectrum.intValuationDef : {R : Type u_1} →
  [inst : CommRing R] → [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R → R → WithZero (Multiplicative ℤ)
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform integral for `f : 𝕜 → E`, with respect to the measure `μ` and additive
character `e`.  -/
Fourier.fourierIntegral : {𝕜 : Type u_1} →
  [inst : CommRing 𝕜] →
    [inst_1 : MeasurableSpace 𝕜] →
      {E : Type u_2} →
        [inst_2 : NormedAddCommGroup E] →
          [NormedSpace ℂ E] → AddChar 𝕜 Circle → MeasureTheory.Measure 𝕜 → (𝕜 → E) → 𝕜 → E
-- Mathlib.Algebra.Order.Hom.Monoid
/-- The identity map as an ordered additive monoid homomorphism.  -/
OrderAddMonoidHom.id : (α : Type u_2) → [inst : Preorder α] → [inst_1 : AddZeroClass α] → α →+o α
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear:
`‖D^n (x ↦ B (f x) (g x))‖ ≤ ‖B‖ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖`  -/
ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type uF}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {G : Type uG} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞},
  ContDiff 𝕜 N f →
    ContDiff 𝕜 N g →
      ∀ (x : D) {n : ℕ},
        ↑n ≤ N →
          ‖iteratedFDeriv 𝕜 n (fun y => (B (f y)) (g y)) x‖ ≤
            ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.comp_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β},
  Function.Semiconj₂ f ga gb → Function.bicompr f ga = Function.bicompl gb f f
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- If the structure is a ring, we store its id in the `CommRing` module at `ringId?`  -/
Lean.Meta.Grind.Arith.Linear.Struct.ringId? : Lean.Meta.Grind.Arith.Linear.Struct → Option ℕ
-- Mathlib.Data.Nat.Basic
/-- `dvd` is injective in the left argument  -/
Nat.dvd_left_injective : Function.Injective fun x1 x2 => x1 ∣ x2
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_or_odd : ∀ (n : ℤ), Even n ∨ Odd n
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The topology on the set of points of the complete lattice `L`.  -/
Locale.PT.instTopologicalSpace : (L : Type u_1) → [inst : CompleteLattice L] → TopologicalSpace (Locale.PT L)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eraseKey_eq_of_beq_minKey?_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (∀ {km : α}, Std.Internal.List.minKey? l = some km → (k == km) = false) →
      Std.Internal.List.minKey? (Std.Internal.List.eraseKey k l) = Std.Internal.List.minKey? l
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.toGrp_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C), A.toGrp.X = A.X
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.map_zero' : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] (self : ContinuousMapZero X R), self.toContinuousMap 0 = 0
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs
/-- The ideal of elements that are not units.  -/
IsLocalRing.maximalIdeal : (R : Type u_1) → [inst : CommSemiring R] → [IsLocalRing R] → Ideal R
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C),
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A =
    (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{w + 1})).obj A.X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_fst_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) {X_1 Y_1 : X}
  (f : X_1 ⟶ Y_1),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).fst.map f =
    S.fst.map (U.map f)
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_le_exponent : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α],
  0 < Monoid.exponent M → ∀ (m : M) (a : α), MulAction.period m a ≤ Monoid.exponent M
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.coe_of : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] (M : Type v) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : ContinuousAdd M] [inst_6 : ContinuousSMul R M],
  ↑(TopModuleCat.of R M).toModuleCat = M
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.State.mk.inj : ∀ {α : Type} {producers : Std.Queue (IO.Promise Bool)} {waiters : Std.Queue (Std.Broadcast.Consumer✝ α)}
  {capacity : { x // 0 < x }} {size : ℕ} {buffer : Vector (IO.Ref (Std.Slot✝ α)) ↑capacity} {write read : Fin ↑capacity}
  {receivers : Std.TreeMap ℕ ℕ compare} {nextId : ℕ} {closed : Bool} {pos : ℕ}
  {producers_1 : Std.Queue (IO.Promise Bool)} {waiters_1 : Std.Queue (Std.Broadcast.Consumer✝ α)}
  {capacity_1 : { x // 0 < x }} {size_1 : ℕ} {buffer_1 : Vector (IO.Ref (Std.Slot✝ α)) ↑capacity_1}
  {write_1 read_1 : Fin ↑capacity_1} {receivers_1 : Std.TreeMap ℕ ℕ compare} {nextId_1 : ℕ} {closed_1 : Bool}
  {pos_1 : ℕ},
  { producers := producers, waiters := waiters, capacity := capacity, size := size, buffer := buffer, write := write,
        read := read, receivers := receivers, nextId := nextId, closed := closed, pos := pos } =
      { producers := producers_1, waiters := waiters_1, capacity := capacity_1, size := size_1, buffer := buffer_1,
        write := write_1, read := read_1, receivers := receivers_1, nextId := nextId_1, closed := closed_1,
        pos := pos_1 } →
    producers = producers_1 ∧
      waiters = waiters_1 ∧
        capacity = capacity_1 ∧
          size = size_1 ∧
            buffer ≍ buffer_1 ∧
              write ≍ write_1 ∧
                read ≍ read_1 ∧ receivers = receivers_1 ∧ nextId = nextId_1 ∧ closed = closed_1 ∧ pos = pos_1
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] (f : InfTopHom β γ) (g : InfTopHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rTensor_tmul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P] (f : M →ₗ[A] P) (m : M) (n : N),
  ((TensorProduct.AlgebraTensorModule.rTensor R N) f) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT? k = Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k none
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- A local notation for the Killing complement of the ideal range of `ad`.  -/
_private.Mathlib.Algebra.Lie.Derivation.Killing.0.LieDerivation.IsKilling.«term𝕀ᗮ» : Lean.ParserDescr
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.comp : ∀ (R : Type u_1) [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [Algebra.FormallyUnramified R A] [Algebra.FormallyUnramified A B], Algebra.FormallyUnramified R B
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.ground_spanning : ∀ {α : Type u_2} (M : Matroid α), M.Spanning M.E
-- Mathlib.Order.Hom.Lattice
InfHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Min α} {inst_1 : Min β} {toFun : α → β}
  {map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b} {toFun_1 : α → β}
  {map_inf'_1 : ∀ (a b : α), toFun_1 (a ⊓ b) = toFun_1 a ⊓ toFun_1 b},
  { toFun := toFun, map_inf' := map_inf' } = { toFun := toFun_1, map_inf' := map_inf'_1 } → toFun = toFun_1
-- Mathlib.Condensed.Explicit
/-- A condensed object regarded as a sheaf on `Profinite` preserves finite products.  -/
Condensed.instPreservesFiniteProductsOppositeProfiniteObjFunctorIsSheafCoherentTopology : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A),
  CategoryTheory.Limits.PreservesFiniteProducts X.obj
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.getSimpParams : Lean.TSyntax `tactic → Array Lean.Syntax
-- Mathlib.Data.Set.Function
Set.RightInvOn.mono : ∀ {α : Type u_1} {β : Type u_2} {t t₁ : Set β} {f : α → β} {f' : β → α},
  Set.RightInvOn f' f t → t₁ ⊆ t → Set.RightInvOn f' f t₁
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- Auxiliary definition for the doubling formula (we'll show this is equal to `Gamma s`)  -/
Real.doublingGamma : ℝ → ℝ
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets_singleton_iff : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω},
  ProbabilityTheory.iIndepSets (fun i => {s i}) μ ↔ ∀ (t : Finset ι), μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.finTwoProd_one : ∀ (R : Type u_7) [inst : Semiring R], (Module.Basis.finTwoProd R) 1 = (0, 1)
-- Mathlib.FieldTheory.Finite.Basic
/-- If `F` has odd characteristic, then for nonzero `a : F`, we have that `a ^ (#F / 2) = ±1`.  -/
FiniteField.pow_dichotomy : ∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F],
  ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- A weak kernel of `f - g` is a weak equalizer of `f` and `g`.  -/
CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          {c : CategoryTheory.Limits.KernelFork (f - g)} →
            CategoryTheory.Limits.IsWeakLimit c →
              CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Preadditive.forkOfKernelFork c)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Every polynomial splits in the field extension `f : K →+* k` if `K` is algebraically closed.  -/
IsAlgClosed.splits_domain : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [IsAlgClosed k] [inst_2 : Field K] {f : k →+* K} (p : Polynomial k),
  (Polynomial.map f p).Splits
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_le_iff_of_isSuccLimit : ∀ {a b c : Ordinal.{u_4}}, Order.IsSuccLimit b → (a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c)
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.Except.map.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((err : ε) → motive (Except.error err)) → ((v : α) → motive (Except.ok v)) → motive x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.connectedSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], ConnectedSpace (TopologicalSpace.NonemptyCompacts α) ↔ ConnectedSpace α
-- Lean.Meta.Match.MatcherInfo
/-- (Conservative approximation of) which alternatives may overlap another.
 -/
Lean.Meta.Match.MatcherInfo.overlaps : Lean.Meta.MatcherInfo → Lean.Meta.Match.Overlaps
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.filterMap_equiv_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ},
  m.WF → (Std.HashMap.Raw.filterMap (fun k v => some (f k v)) m).Equiv (Std.HashMap.Raw.map f m)
-- Mathlib.CategoryTheory.Category.Basic
/-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed:
`g ≫ f = h ≫ f` implies `g = h`. 

[Stacks Tag 003B](https://stacks.math.columbia.edu/tag/003B) -/
CategoryTheory.Mono : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- Note that this is an equality of elements of `ℝ≥0∞`. See also
`MeasureTheory.ProbabilityMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`.  -/
MeasureTheory.ProbabilityMeasure.map_apply' : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'},
  MeasurableSet A → ↑(ν.map f_aemble) A = ↑ν (f ⁻¹' A)
-- Mathlib.Order.Monotone.Defs
instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {f : α → β} → {s : Set α} → [i : Decidable (∀ a ∈ s, ∀ b ∈ s, a ≤ b → f a ≤ f b)] → Decidable (MonotoneOn f s)
-- Mathlib.Topology.VectorBundle.Hom
hom_trivializationAt_apply : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] (x₀ : B)
  (x : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x),
  ↑(trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀) x =
    (x.proj, ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ x₀ x.proj x₀ x.proj x.snd)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      Std.DTreeMap.Raw.Const.get? t k = some v ↔
        ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ Std.DTreeMap.Raw.Const.toList t
-- Mathlib.Topology.Order.PartialSups
Filter.Tendsto.partialSups : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {α : Type u_2} {l : Filter α}
  {f : ℕ → α → L} {g : ℕ → L} {n : ℕ},
  (∀ k ≤ n, Filter.Tendsto (f k) l (nhds (g k))) → Filter.Tendsto ((partialSups f) n) l (nhds ((partialSups g) n))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.support_subset : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₂.IsSubwalk p₁ → p₂.support ⊆ p₁.support
-- Mathlib.CategoryTheory.Sigma.Basic
/-- To build a natural transformation over the sigma category, it suffices to specify it restricted to
each subcategory.
 -/
CategoryTheory.Sigma.natTrans : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {F G : CategoryTheory.Functor ((i : I) × C i) D} →
            ((i : I) → (CategoryTheory.Sigma.incl i).comp F ⟶ (CategoryTheory.Sigma.incl i).comp G) → (F ⟶ G)
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
    (∀ (x_2 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_2 → False) →
      (match x with
        | Lean.Grind.CommRing.Expr.num n => h_1 n
        | Lean.Grind.CommRing.Expr.var x => h_2 x
        | x => h_3 x) =
        h_3 x
-- Mathlib.Order.Cover
WCovBy.eval : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {a b : (i : ι) → α i},
  a ⩿ b → ∀ (i : ι), a i ⩿ b i
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.v.hcongr_10 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (inst_1 : CategoryTheory.Preadditive C) (inst'_1 : CategoryTheory.Preadditive C'),
          inst_1 ≍ inst'_1 →
            ∀ (F : CochainComplex C ℤ) (F' : CochainComplex C' ℤ),
              F ≍ F' →
                ∀ (G : CochainComplex C ℤ) (G' : CochainComplex C' ℤ),
                  G ≍ G' →
                    ∀ (n n' : ℤ),
                      n = n' →
                        ∀ (γ : CochainComplex.HomComplex.Cochain F G n)
                          (γ' : CochainComplex.HomComplex.Cochain F' G' n'),
                          γ ≍ γ' →
                            ∀ (p p' : ℤ),
                              p = p' →
                                ∀ (q q' : ℤ),
                                  q = q' →
                                    ∀ (hpq : p + n = q) (hpq' : p' + n' = q'),
                                      hpq ≍ hpq' → γ.v p q hpq ≍ γ'.v p' q' hpq'
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.forallProp.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Meta.Grind.SplitSource.forallProp e = Lean.Meta.Grind.SplitSource.forallProp e_1) = (e = e_1)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_const : ∀ (α : Type u_1) {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (b : β), ↑(MeasureTheory.AEEqFun.const α b) =ᵐ[μ] Function.const α b
-- Mathlib.Order.Ideal
/-- This ideal is not the whole set.  -/
Order.Ideal.IsProper.ne_univ : ∀ {P : Type u_1} {inst : LE P} {I : Order.Ideal P} [self : I.IsProper], ↑I ≠ Set.univ
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.i : {R : Type u_2} → {inst : CommRing R} → [self : WithIdeal R] → Ideal R
-- Mathlib.MeasureTheory.Measure.Support
/-- Under the assumption `OpensMeasurableSpace`, this is redundant because
the support is closed, and therefore measurable.  -/
MeasureTheory.Measure.nullMeasurableSet_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], MeasureTheory.NullMeasurableSet μ.support μ
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.ProdPreservesConnectedLimits.forgetCone_pt : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type v₂} [inst_2 : CategoryTheory.SmallCategory J] {X : C} {K : CategoryTheory.Functor J C}
  (s : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Limits.prod.functor.obj X))),
  (CategoryTheory.ProdPreservesConnectedLimits.forgetCone s).pt = s.pt
-- Mathlib.RingTheory.WittVector.Defs
WittVector.v2_coeff : ∀ {p' : ℕ} {R' : Type u_2} (x y : WittVector p' R') (i : Fin 2), (![x, y] i).coeff = ![x.coeff, y.coeff] i
-- Init.Grind.Config
/-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
or for which no patterns can be generated.  -/
Lean.Grind.Config.lax : Lean.Grind.Config → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₁_pairing : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : h.ι), h.type₁ x = ↑(h.pairing.p (h.equivII x))
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- **Alias** of `MeasureTheory.AEDisjoint.measure_sdiff_left`. -/
MeasureTheory.AEDisjoint.measure_diff_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → μ (s \ t) = μ s
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.subsingleton_h1Cotangent : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.FormallyEtale R A], Subsingleton (Algebra.H1Cotangent R A)
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.Equiv.symm : ∀ {self : Batteries.UnionFind} {a b : ℕ}, self.Equiv a b → self.Equiv b a
-- Mathlib.RingTheory.WittVector.Identities
WittVector.iterate_verschiebung_mul_left : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R) (i : ℕ),
  (⇑WittVector.verschiebung)^[i] x * y = (⇑WittVector.verschiebung)^[i] (x * (⇑WittVector.frobenius)^[i] y)
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- A sieve is effective epimorphic if the associated cocone is a colimit cocone.  -/
CategoryTheory.Sieve.EffectiveEpimorphic : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.Sieve X → Prop
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
/-- `PowerSeries.pentagonalSeries` as an infinite sum over natural numbers. In this version, terms
are ordered by strictly increasing exponent `pentagonal k` for `k = 0, 1, -1, 2, -2, 3, ...`,
and every two terms are grouped together.  -/
PowerSeries.WithPiTopology.hasSum_pow_pentagonal_sub_pentagonalSeries : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R],
  HasSum (fun k => (-1) ^ k * (PowerSeries.X ^ pentagonal (-↑k) - PowerSeries.X ^ pentagonal (↑k + 1)))
    (PowerSeries.pentagonalSeries R)
-- Mathlib.Algebra.Group.Basic
dite_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (p : Prop) [inst_1 : Decidable p] (a : p → α) (b : ¬p → α) (c : β),
  (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c