mathlib-initiative/mathlib-types huggingface dataset:
-- Plausible.Gen
/-- Tries all generators until one returns a `Some` value or all the generators failed once with `None`.
The generators are picked at random according to their weights (like `frequency` in Haskell QuickCheck),
and each generator is run at most once.  -/
Plausible.Gen.backtrack : {α : Type u_1} → List (ℕ × Plausible.Gen α) → Plausible.Gen α
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.uniformContinuousConstSMul : ∀ {𝕜₁ : 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] {M : Type u_7} [inst_7 : Monoid M] [inst_8 : DistribMulAction M F]
  [inst_9 : SMulCommClass 𝕜₂ M F] [inst_10 : UniformSpace F] [inst_11 : IsUniformAddGroup F]
  [inst_12 : UniformContinuousConstSMul M F], UniformContinuousConstSMul M (E →SL[σ] F)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk.injEq : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (toSubmodule : Submodule R M)
  (lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier) (toSubmodule_1 : Submodule R M)
  (lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier),
  ({ toSubmodule := toSubmodule, lie_mem := lie_mem } = { toSubmodule := toSubmodule_1, lie_mem := lie_mem_1 }) =
    (toSubmodule = toSubmodule_1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.isEmpty = true → m.getKey? a = none
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.mkUVarTuple : Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
PresheafOfModules.instIsNormalMonoCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  CategoryTheory.IsNormalMonoCategory (PresheafOfModules R)
-- Std.Http.Protocol.H1.Writer
/-- Determines the transfer encoding mode based on explicit setting, body closure state, or defaults to chunked.
 -/
Std.Http.Protocol.H1.Writer.determineTransferMode : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Body.Length
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl = Option.any (f k) (t.get? k)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMonoidOfContinuousMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
  [inst_3 : ContinuousMul β],
  ContinuousMap.instMonoidOfContinuousMul =
    { toSemigroup := ContinuousMap.instSemigroupOfContinuousMul, toOne := ContinuousMap.instOne, one_mul := ⋯,
      mul_one := ⋯, toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.cauchyFilter_eq : ∀ {α : Type u_1} [inst : UniformSpace α] [CompleteSpace α] [T0Space α] {f g : CauchyFilter α},
  (↑f).lim = (↑g).lim ↔ Inseparable f g
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] [inst_1 : SuccOrder α] (a : α), Order.succ a = ⨅ b, ⨅ (_ : b > a), b
-- Aesop.RulePattern.Cache
Aesop.RulePatternCache.mk : Std.HashMap Lean.Expr Aesop.RulePatternCache.Entry → Aesop.RulePatternCache
-- Mathlib.Data.Part
Part.ofOption_eq_get : ∀ {α : Type u_4} (o : Option α), ↑o = { Dom := o.isSome = true, get := o.get }
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- Riesz content `λ` (associated with a positive linear functional `Λ`) is
monotone: if `K₁ ⊆ K₂` are compact subsets in `X`, then `λ(K₁) ≤ λ(K₂)`.  -/
rieszContentAux_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [T2Space X] [LocallyCompactSpace X] {K₁ K₂ : TopologicalSpace.Compacts X},
  K₁ ≤ K₂ → rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.isBasis : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsBasis' I X → autoParam (X ⊆ M.E) Matroid.IsBasis'.isBasis._auto_1 → M.IsBasis I X
-- Lean.Server.Requests
/-- A request handler is partial if the LSP spec states that the request method implemented by
the handler should be responded to with the full state of the document, but our implementation
of the handler only returns a partial result for the document
(e.g. only for the processed regions of the document, to reduce latency after a `didChange`).
A request handler can only be partial if LSP also specifies a corresponding `refresh`
server-to-client request, e.g. `workspace/inlayHint/refresh` for `textDocument/inlayHint`.
This is necessary because we use the `refresh` request to prompt the client to re-request the
data for a partial request if we returned a partial response for that request in the past,
so that the client eventually converges to a complete set of information for the full document.
 -/
Lean.Server.RequestHandlerCompleteness.partial : String → ℕ → Lean.Server.RequestHandlerCompleteness
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.injective_of_prod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {ι : Type u_1} [inst_2 : Fintype ι] {f : ι → R},
  (∏ i, (Polynomial.X - Polynomial.C (f i))).Separable → Function.Injective f
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.zero.sizeOf_spec : ∀ (sign : Float.Model.UnpackedFloat.Sign), sizeOf (Float.Model.UnpackedFloat.zero sign) = 1 + sizeOf sign
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_prop : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r} {a b : α}, s(a, b) ∈ Sym2.fromRel sym ↔ r a b
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.Array.toListLitAux.match_1.splitter : {α : Type u_1} →
  (xs : Array α) →
    (motive : (x : ℕ) → x ≤ xs.size → List α → Sort u_2) →
      (x : ℕ) →
        (x_1 : x ≤ xs.size) →
          (x_2 : List α) →
            ((x : 0 ≤ xs.size) → (acc : List α) → motive 0 x acc) →
              ((i : ℕ) → (hi : i + 1 ≤ xs.size) → (acc : List α) → motive i.succ hi acc) → motive x x_1 x_2
-- Mathlib.GroupTheory.Subgroup.Simple
Subgroup.isSimpleGroup_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  IsSimpleGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.subgroupOf H).Normal → H' = ⊥ ∨ H' = H
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.hasSmallLocalizedHom_iff_source : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {X X' : C}
  (f : X ⟶ X'),
  W f →
    ∀ (Y : C),
      CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ CategoryTheory.Localization.HasSmallLocalizedHom W X' Y
-- Mathlib.Order.Basic
forall_lt_imp_ne_iff_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ c < a, c ≠ b) ↔ a ≤ b
-- Std.Time.Zoned
/-- Converts a `PlainDateTime` to a `Timestamp` using the `ZoneRules`.
 -/
Std.Time.PlainDateTime.toTimestamp : Std.Time.PlainDateTime → Std.Time.TimeZone.ZoneRules → Std.Time.Timestamp
-- Std.Http.Protocol.H1
/-- Returns `true` when an `Expect` header includes `100-continue`.

RFC 9110 §15.2: Since HTTP/1.0 did not define any 1xx status codes, a server MUST NOT send a 1xx response
to an HTTP/1.0 client.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.hasExpectContinue : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Bool
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] [inst_3 : CompleteLattice δ] (f : CompleteLatticeHom γ δ) (g : CompleteLatticeHom β γ)
  (h : CompleteLatticeHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.forEachExprWithExposedLevelMVars.visit : (Lean.Expr → Lean.Elab.TermElabM Unit) →
  (Lean.Expr →
      ReaderT Lean.Expr (Lean.MonadCacheT Lean.ExprStructEq Unit Lean.Elab.TermElabM) Unit →
        ReaderT Lean.Expr (Lean.MonadCacheT Lean.ExprStructEq Unit Lean.Elab.TermElabM) Unit) →
    Lean.Expr →
      optParam Bool false → ReaderT Lean.Expr (Lean.MonadCacheT Lean.ExprStructEq Unit Lean.Elab.TermElabM) Unit
-- Mathlib.Algebra.Lie.Graded
DirectSum.decompose_symm_bracket : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ]
  (x y : DirectSum ι fun i => ↥(ℒ i)),
  (DirectSum.decompose ℒ).symm ⁅x, y⁆ = ⁅(DirectSum.decompose ℒ).symm x, (DirectSum.decompose ℒ).symm y⁆
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instSuccAddOrder : SuccAddOrder Ordinal.{u_1}
-- Mathlib.Topology.MetricSpace.Gluing
Metric.separableSpaceInductiveLimit_of_separableSpace : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] [hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace (X n)]
  {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n)),
  TopologicalSpace.SeparableSpace (Metric.InductiveLimit I)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_div : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M]
  {s t : Set M}, s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (s / t) = sInf s / sSup t
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- Relation between the fiber functors on presheaves for the points `Φ.map F K`
and `Φ` when `F : C ⥤ D` is a cocontinuous functor between sites `(C, J)` and `(D, K)`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (Φ : J.Point) →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [inst_2 : F.IsCocontinuous J K] →
                  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] →
                    (A : Type u'') →
                      [inst_4 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (Φ.map F K).presheafFiber ≅
                            ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op).comp Φ.presheafFiber
-- Mathlib.Condensed.Light.Small
/-- Sheafifying is preserved under conjugating with the equivalence between light condensed objects
and sheaves on a small site.
 -/
LightCondensed.equivSmallSheafificationIso : {C : Type w} →
  [inst : CategoryTheory.Category.{v, w} C] →
    [inst_1 : CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology LightProfinite) C] →
      [inst_2 :
          CategoryTheory.HasWeakSheafify
            ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology
              (CategoryTheory.coherentTopology LightProfinite))
            C] →
        (CategoryTheory.equivSmallModel LightProfinite).op.congrLeft.inverse.comp
            ((CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).comp
              (LightCondensed.equivSmall C).functor) ≅
          CategoryTheory.presheafToSheaf
            ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology
              (CategoryTheory.coherentTopology LightProfinite))
            C
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion : CategoryTheory.Limits.WalkingReflexivePair.zero.Hom CategoryTheory.Limits.WalkingReflexivePair.one
-- Init.Data.Vector.Range
Vector.range'_concat : ∀ {step s n : ℕ}, Vector.range' s (n + 1) step = Vector.range' s n step ++ #v[s + step * n]
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.ext₁' : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsTriangulatedClosed₁],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₂ → P T.obj₃ → P.isoClosure T.obj₁
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_congr : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs ys : Vector α n},
  xs = ys → ∀ (f : (i : ℕ) → α → i < n → β), xs.mapFinIdx f = ys.mapFinIdx f
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.whiskerLeft_app_apply : ∀ (K : SSet) {L L' : SSet} (g : L ⟶ L') {Δ : SimplexCategoryᵒᵖ}
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (K.obj Δ) (g.app Δ))) x =
    (x.1, (CategoryTheory.ConcreteCategory.hom (g.app Δ)) x.2)
-- Mathlib.Data.Matrix.Basis
/-- `single i j a` is the matrix with `a` in the `i`-th row, `j`-th column,
and zeroes elsewhere.
 -/
Matrix.single : {m : Type u_2} →
  {n : Type u_3} → {α : Type u_7} → [DecidableEq m] → [DecidableEq n] → [Zero α] → m → n → α → Matrix m n α
-- Mathlib.Logic.Function.Basic
Function.Surjective.injective_comp_right : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β}, Function.Surjective f → Function.Injective fun g => g ∘ f
-- Mathlib.Data.NNReal.Defs
/-- To prove a property holds for real numbers it suffices to show that it holds for `x : ℝ≥0`,
and if it holds for `x : ℝ≥0`, then it does also for `(-↑x : ℝ)`.  -/
Real.nnreal_induction_on : ∀ {motive : ℝ → Prop}, (∀ (x : NNReal), motive ↑x) → (∀ (x : NNReal), motive ↑x → motive (-↑x)) → ∀ (r : ℝ), motive r
-- Mathlib.Data.Countable.Basic
WithBot.instUncountable : ∀ {α : Type u} [Uncountable α], Uncountable (WithBot α)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- For `a - -b = a + b`, see `sub_neg_eq_add`.  -/
sub_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a - b < 0 ↔ a < b
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_self_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (a : Polynomial R), a.wronskian a = 0
-- Mathlib.Topology.MetricSpace.Similarity
Congruent.similar : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂]
  {v₁ : ι → P₁} {v₂ : ι → P₂}, Congruent v₁ v₂ → Similar v₁ v₂
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_eq_norm_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] {x : E} (y : E), ‖x‖ = 0 → ‖x / y‖ = ‖y‖
-- Mathlib.Algebra.Torsor.Basic
/-- If subtracting two points from the same point produces equal
results, those points are equal.  -/
vsub_right_cancel : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P}, p -ᵥ p₁ = p -ᵥ p₂ → p₁ = p₂
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.natCast : {α : Type u_1} →
  [inst : AddMonoidWithOne α] →
    [inst_1 : PartialOrder α] → [AddLeftMono α] → [ZeroLEOneClass α] → NatCast { x // 0 ≤ x }
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.inductionOn : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f →
    ∀ (x : N) (motive : N → Prop),
      motive 0 →
        (∀ (m : M), motive (f m)) →
          (∀ (s : S) (n : N), motive n → motive (s • n)) →
            (∀ (n₁ n₂ : N), motive n₁ → motive n₂ → motive (n₁ + n₂)) → motive x
-- Mathlib.RingTheory.Noetherian.Basic
LinearEquiv.isNoetherian_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (f : M ≃ₛₗ[σ] P),
  IsNoetherian R M ↔ IsNoetherian S P
-- Mathlib.SetTheory.Lists
Lists'.Subset.below.nil : ∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} {l : Lists' α true}, ⋯.below
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), H.relIndex K = (H.addSubgroupOf K).index
-- Mathlib.Data.Part
Part.instOne.eq_1 : ∀ {α : Type u_1} [inst : One α], Part.instOne = { one := pure 1 }
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `F : J ⥤ C` then `F.cocones` is the functor assigning to an object `(X : C)`
the type of natural transformations from `F` to the constant functor with value `X`.
An object corepresenting this functor is a colimit of `F`.
 -/
CategoryTheory.Functor.cocones : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        CategoryTheory.Functor J C → CategoryTheory.Functor C (Type (max u₁ v₃))
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Approximate a function `α → ℝ≥0∞` by a series of simple functions taking their values
in `ℝ≥0`.  -/
MeasureTheory.SimpleFunc.eapproxDiff : {α : Type u_1} → [inst : MeasurableSpace α] → (α → ENNReal) → ℕ → MeasureTheory.SimpleFunc α NNReal
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.unitOfList_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  Std.ExtDHashMap.Const.unitOfList l = ∅ ↔ l = []
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.irreducible : ∀ {M : Type u_1} [inst : Monoid M] {p q : M}, Associated p q → Irreducible p → Irreducible q
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_invVeblen₁_invVeblen₂ : ∀ (x : Ordinal.{u_1}), Ordinal.veblen x.invVeblen₁ x.invVeblen₂ = Ordinal.omega0 ^ x
-- Mathlib.Dynamics.Flow
Flow.map_add' : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (self : Flow τ α) (t₁ t₂ : τ) (x : α), self.toFun (t₁ + t₂) x = self.toFun t₁ (self.toFun t₂ x)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.ofIsoI_isImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.ImageFactorisation f) {I' : C} (e : F.F.I ≅ I'), (F.ofIsoI e).isImage = F.isImage.ofIsoI e
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cos θ` to the value `sin ((n + 1) * θ) / sin θ`.  -/
Polynomial.Chebyshev.S_two_mul_real_cos : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (2 * Real.cos θ) (Polynomial.Chebyshev.S ℝ n) * Real.sin θ = Real.sin ((↑n + 1) * θ)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.r : (α : Type u) → [Lean.Grind.Semiring α] → α × α → α × α → Prop
-- Init.Prelude
/-- Retrieve the left-most leaf's info in the Syntax tree, or `none` if there is no token.  -/
Lean.Syntax.getHeadInfo : Lean.Syntax → Lean.SourceInfo
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropSuffix?_eq_map_skipSuffix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.dropSuffix? pat = Option.map s.sliceTo (s.skipSuffix? pat)
-- Mathlib.AlgebraicGeometry.Restrict
/-- the notation for restricting a morphism of scheme to an open subset of the target scheme  -/
AlgebraicGeometry.«term_∣__» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.snd_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : Monoid.Coprod M N),
  Monoid.Coprod.snd ((Monoid.Coprod.swap M N) x) = Monoid.Coprod.fst x
-- Mathlib.Data.List.Permutation
List.map_permutations : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (ts : List α),
  List.map (List.map f) ts.permutations = (List.map f ts).permutations
-- Init.Data.Array.Erase
Array.getElem_eraseIdx : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {j : ℕ} (h' : j < (xs.eraseIdx i h).size),
  (xs.eraseIdx i h)[j] = if h'' : j < i then xs[j] else xs[j + 1]
-- Mathlib.Tactic.Translate.Attributes
/-- For an attribute that generates new declarations,
register the implementation that returns the generated declarations.
This will be used by translation attributes for translating between generated declarations.  -/
Mathlib.Tactic.registerGeneratingAttr : Lean.Name → (Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM (Array Lean.Name)) → IO Unit
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_self_homothety : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist p₂ ((AffineMap.homothety p₁ c) p₂) = ‖1 - c‖ * dist p₁ p₂
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittNeg.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → WittVector.wittNeg p a = WittVector.wittNeg p_1 a_1
-- Mathlib.Data.Fin.VecNotation
/-- A simproc that handles terms of the form `Matrix.vecCons a f i` where `i` is a numeric literal.

In practice, this is most effective at handling `![a, b, c] i`-style terms.  -/
Matrix.cons_val : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_iCycles_odd_comp_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [inst_3 : CategoryTheory.CategoryWithHomology C] {j : ℕ},
  c.Rel (c.prev j) j →
    c.Rel j (c.next j) →
      Odd j →
        ∀ {F : C → C → Type uF} {carrier : C → Type w}
          {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
          [inst_4 : CategoryTheory.ConcreteCategory C F]
          (x : carrier ((HomologicalComplex.alternatingConst A hOdd hEven hc).cycles j)),
          (CategoryTheory.ConcreteCategory.hom ψ)
              ((CategoryTheory.ConcreteCategory.hom ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j))
                x) =
            (CategoryTheory.ConcreteCategory.hom 0) x
-- Mathlib.Analysis.Analytic.Basic
/-- Variant of `HasFPowerSeriesWithinOnBall.congr` in which one requests equality on `insert x s`
instead of separating `x` and `s`.  -/
HasFPowerSeriesWithinOnBall.congr' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    Set.EqOn g f (insert x s ∩ Metric.eball x r) → HasFPowerSeriesWithinOnBall g p s x r
-- Mathlib.Order.Partition.Equipartition
Finpartition.IsEquipartition.average_le_card_part : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {P : Finpartition s},
  P.IsEquipartition → t ∈ P.parts → s.card / P.parts.card ≤ t.card