mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_sub : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  MeasureTheory.FinMeasAdditive μ T →
    ∀ {f g : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.Integrable (⇑g) μ →
          MeasureTheory.SimpleFunc.setToSimpleFunc T (f - g) =
            MeasureTheory.SimpleFunc.setToSimpleFunc T f - MeasureTheory.SimpleFunc.setToSimpleFunc T g
-- Mathlib.Topology.Spectral.Hom
isSpectralMap_id : ∀ {α : Type u_2} [inst : TopologicalSpace α], IsSpectralMap id
-- Init.Data.BitVec.Bitblast
/-- We show that the output of `divSubtractShift` is lawful, which tells us that it
obeys the division equation.  -/
BitVec.lawful_divSubtractShift : ∀ {w : ℕ} {args : BitVec.DivModArgs w} (qr : BitVec.DivModState w),
  BitVec.DivModState.Poised args qr → BitVec.DivModState.Lawful args (BitVec.divSubtractShift args qr)
-- Mathlib.Data.ENNReal.Operations
ENNReal.toNNReal_sInf : ∀ (s : Set ENNReal), (∀ r ∈ s, r ≠ ⊤) → (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_closedBall_ball_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'],
  IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomSurjective.ids : ∀ {R₁ : Type u_1} [inst : Semiring R₁], RingHomSurjective (RingHom.id R₁)
-- Mathlib.Topology.Order
/-- **Alias** of `setOfPred_isOpen_sup`. -/
setOf_isOpen_sup : ∀ {α : Type u} (t₁ t₂ : TopologicalSpace α), {s | IsOpen s} = {s | IsOpen s} ∩ {s | IsOpen s}
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.instCreatesLimitsForget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.CreatesLimits (CategoryTheory.Mon.forget C)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_nonempty : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux_nonneg : ∀ {c : ℝ} {f : ℕ → Bool} {n : ℕ}, 0 ≤ c → 0 ≤ Cardinal.cantorFunctionAux c f n
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_self : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.LocallySmall.{v, v, u} C
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.top_pos : ∀ {α : Type u} [inst : Zero α] [inst_1 : LT α], 0 < ⊤
-- Mathlib.Data.Multiset.Find
Multiset.find?_singleton : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α) (hp : {x | x ∈ {a} ∧ p x}.Subsingleton),
  Multiset.find? p {a} hp = if p a then some a else none
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_of_neg : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] {n : ℤ}, n < 0 → selfZPow x B n = IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsStableUnderFiniteProductsTrWOfIsTriangulated : ∀ {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) [P.IsTriangulated], P.trW.IsStableUnderFiniteProducts
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_addSubmonoid_sup : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α] {P Q : AddSubmonoid M},
  AddAction.fixedPoints (↥(P ⊔ Q)) α = AddAction.fixedPoints (↥P) α ∩ AddAction.fixedPoints (↥Q) α
-- Mathlib.Combinatorics.Hindman
/-- If `m` and `m'` are finite sums in `M`, then so is `m + m'`, provided that `m'`
is obtained from a subsequence of `M` starting sufficiently late.  -/
Hindman.FS.add : ∀ {M : Type u_1} [inst : AddSemigroup M] {a : Stream' M} {m : M},
  m ∈ Hindman.FS a → ∃ n, ∀ m' ∈ Hindman.FS (Stream'.drop n a), m + m' ∈ Hindman.FS a
-- Init.Control.Lawful.Instances
StateT.run_monadMap : ∀ {n : Type u → Type u_1} {m : Type u → Type u_2} {σ α : Type u} [inst : MonadFunctorT n m]
  (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ), (monadMap f x).run s = monadMap f (x.run s)
-- Mathlib.Analysis.Quaternion
Quaternion.instCStarRingReal : CStarRing (Quaternion ℝ)
-- Init.Grind.Util
/-- Gadget for annotating the equalities in `match`-equations conclusions.
`_origin` is the term used to instantiate the `match`-equation using E-matching.
When `EqMatch a b origin` is `True`, we mark `origin` as a resolved case-split.
 -/
Lean.Grind.EqMatch : {α : Sort u_1} → α → α → {_origin : α} → Prop
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleRing.ext_iff : ∀ {L : Type u_1} {x y : LieAdmissibleRing L},
  x = y ↔
    Add.add = Add.add ∧
      Zero.zero = Zero.zero ∧
        NSMul.nsmul = NSMul.nsmul ∧
          Neg.neg = Neg.neg ∧ Sub.sub = Sub.sub ∧ ZSMul.zsmul = ZSMul.zsmul ∧ Mul.mul = Mul.mul
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.inclusion.eq_1 : ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} (h : S ≤ T),
  AddSubsemigroup.inclusion h = (AddMemClass.subtype S).codRestrict T ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ_σ₀Iter : ∀ {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (h : autoParam (m + (j + 1) = n + 1) SimplexCategory.δ_σ₀Iter._auto_1),
  autoParam (↑i ≤ j + 1) SimplexCategory.δ_σ₀Iter._auto_3 →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) (SimplexCategory.σ₀Iter (j + 1) h) =
      SimplexCategory.σ₀Iter j ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (n : ℕ),
  Int.Internal.Linear.cooper_left_cert p₁ p₂ n = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 →
        Int.Internal.Linear.OrOver n (Int.Internal.Linear.cooper_left_split ctx p₁ p₂)
-- Mathlib.Data.List.Sigma
List.kunion_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  (List.kerase a l₁).kunion (List.kerase a l₂) = List.kerase a (l₁.kunion l₂)
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- `Submodule.pointwiseNeg` is involutive.

This is available as an instance in the `Pointwise` locale.  -/
Submodule.involutivePointwiseNeg : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → InvolutiveNeg (Submodule R M)
-- Init.Data.Float.Float
/-- Converts a floating-point number to a 16-bit unsigned integer.

If the given `Float` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt16`. Returns `0` if the `Float` is negative or `NaN`, and returns the
largest `UInt16` value (i.e. `UInt16.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float.Model`.
 -/
Float.toUInt16 : Float → UInt16
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  {Y x : (Finset (CategoryTheory.Discrete α))ᵒᵖ} (h : Y ⟶ x),
  ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).obj F).map h =
    CategoryTheory.Limits.Pi.lift fun y => CategoryTheory.Limits.Pi.π (fun x => F.obj ↑x) ⟨↑y, ⋯⟩
-- Mathlib.Order.Antichain
IsAntichain.image_embedding : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → ∀ (φ : α ↪o β), IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s)
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_zero : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.toSpanSingleton R M 0 = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_sub : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x y : M →₀ R),
  AddMonoidAlgebra.ofCoeff (x - y) = AddMonoidAlgebra.ofCoeff x - AddMonoidAlgebra.ofCoeff y
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.tensorObj.mul_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.finrank_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : EuclideanGeometry.Sphere P} {p : P},
  p ≠ s.center → Module.finrank ℝ ↥(s.orthRadius p).direction + 1 = Module.finrank ℝ V
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumber.congr_simp : ∀ (α : Type u_1) {inst : DecidableEq α} [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  ruzsaSzemerediNumber α = ruzsaSzemerediNumber α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.ofπ_pt : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (π : Y ⟶ P)
  (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π),
  (CategoryTheory.Limits.Cofork.ofπ π w).pt = P
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.zero_le_orderTop_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R},
  0 ≤ x.orderTop ↔ 0 ≤ x.order
-- Mathlib.Data.Nat.Factorization.Defs
/-- The only prime factor of prime `p` is `p` itself, with multiplicity `1`  -/
Nat.Prime.factorization : ∀ {p : ℕ}, Nat.Prime p → p.factorization = fun₀ | p => 1
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prodMk_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a)
  (y : G.obj a),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.snd.app a))
      (CategoryTheory.FunctorToTypes.prodMk x y) =
    y
-- Lean.Parser.Extra
Lean.Parser.scientificLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl_zero_eq_of_one_sub_one : ∀ (α : Type u_1) (V : Type u_2) [inst : AddGroup α] [inst_1 : One α] [inst_2 : DecidableEq V] [inst_3 : DecidableEq α],
  Matrix.compl 0 = Matrix.of 1 - 1
-- Lean.Elab.Tactic.Induction
/-- Returns true if the alternative is for a wildcard, and that the wildcard is not due to a syntax error.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.isAltWildcard : Lean.Syntax → Bool
-- Lean.Elab.Command
/-- Lifts an action in `CommandElabM` into `CoreM`, updating the environment,
messages, info trees, traces, the name generator, and macro scopes.
The action is run in a context with an empty message log, empty trace state, and empty info trees.

If `throwOnError` is true, then if the command produces an error message, it is converted into an exception.
In this case, info trees and messages are not carried over.

Commands that modify the processing of subsequent commands,
such as `open` and `namespace` commands,
only have an effect for the remainder of the `CommandElabM` computation passed here,
and do not affect subsequent commands.

*Warning:* when using this from `MetaM` monads, the caches are *not* reset.
If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache`
to reset the instance cache.
While the `modifyEnv` function for `MetaM` clears its caches entirely,
`liftCommandElabM` has no way to reset these caches.
 -/
Lean.liftCommandElabM : {α : Type} → Lean.Elab.Command.CommandElabM α → optParam Bool true → Lean.CoreM α
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instCategoryTransported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → CategoryTheory.Category.{v₂, u₂} (CategoryTheory.Monoidal.Transported e)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.ret.injEq : ∀ (k k_1 : Turing.PartrecToTM2.Cont'), (Turing.PartrecToTM2.Λ'.ret k = Turing.PartrecToTM2.Λ'.ret k_1) = (k = k_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.nonempty_iff_ne_bot : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (Q : AffineSubspace k P), (↑Q).Nonempty ↔ Q ≠ ⊥
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mul_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
-- Mathlib.Topology.Algebra.Group.Basic
IsClosed.right_addCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {U : Set G},
  IsClosed U → ∀ (x : G), IsClosed (AddOpposite.op x +ᵥ U)
-- Mathlib.Algebra.Group.Torsion
nsmul_right_inj : ∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a b : M}, n ≠ 0 → (n • a = n • b ↔ a = b)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a b : Associates α),
  (a * b).factors = a.factors + b.factors
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.cotTermUpperBound.congr_simp : ∀ (k k_1 : ℕ),
  k = k_1 →
    ∀ (A A_1 : ℝ),
      A = A_1 →
        ∀ (B B_1 : ℝ) (e_B : B = B_1) (hB : 0 < B) (a a_1 : ℕ),
          a = a_1 → cotTermUpperBound✝ k A B hB a = cotTermUpperBound✝ k_1 A_1 B_1 ⋯ a_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} [inst_1 : Inhabited (β a)],
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.get! a = if compare k a = Ordering.eq then default else t.get! a
-- Mathlib.Algebra.Module.End
IsAddUnit.smul_left : ∀ {S : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {x : M} [inst_1 : DistribSMul S M],
  IsAddUnit x → ∀ (s : S), IsAddUnit (s • x)
-- Mathlib.Order.Bounds.Basic
DirectedOn.isCofinalFor_fst_image_prod_snd_image : ∀ {α : Type u_1} [inst : Preorder α] {β : Type u_4} [inst_1 : Preorder β] {s : Set (α × β)},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodX_ext_from_iff : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι}
  {f g : (K ⊞ L).X i ⟶ A},
  f = g ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) g ∧
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) g
-- Init.Data.Range.Polymorphic.SInt
Int8.le.eq_1 : ∀ (a b : Int8), a.le b = (a.toBitVec.sle b.toBitVec = true)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.FG.map : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N]
  (f : L.Hom M N) {s : L.Substructure M}, s.FG → (FirstOrder.Language.Substructure.map f s).FG
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instOne : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → One (MvPowerSeries σ R)
-- Mathlib.Order.Types.Defs
/-- `OrderType.{u}` is the type of linear orders in `Type u`, up to order isomorphism.  -/
OrderType : Type (u + 1)
-- Mathlib.CategoryTheory.Sites.Closed
/-- If presheaf of `J₁`-closed sieves is a `J₂`-sheaf then `J₁ ≤ J₂`. Note the converse is true by
`classifier_isSheaf` and `isSheaf_of_le`.
 -/
CategoryTheory.le_topology_of_closedSieves_isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₂).toFunctor → J₁ ≤ J₂
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The equivalence between functions on the generators and group homomorphisms from a free group
given by those generators.  -/
IsFreeGroup.lift : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : IsFreeGroup G] → {H : Type u_2} → [inst_2 : Group H] → (IsFreeGroup.Generators G → H) ≃ (G →* H)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_add_pi_div_two : ∀ (θ : Real.Angle), (θ + ↑(Real.pi / 2)).cos = -θ.sin
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv
      CategoryTheory.Limits.prod.snd =
    TypeCat.ofHom Prod.snd
-- Std.Data.Internal.List.Associative
/-- Given a proof that the list is nonempty, returns the smallest key in an associative list.  -/
Std.Internal.List.maxKey! : {α : Type u} → {β : α → Type v} → [Ord α] → [Inhabited α] → List ((a : α) × β a) → α
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_restrictScalars : ∀ (R : Type u_1) {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] {A : Type u_7} [inst_7 : Semiring A] [inst_8 : SMul R A] [inst_9 : Module A M]
  [inst_10 : Module A N] [inst_11 : IsScalarTower R A M] [inst_12 : IsScalarTower R A N] (f : M [⋀^ι]→L[A] N),
  ⇑(ContinuousAlternatingMap.restrictScalars R f) = ⇑f
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (method : String) (param : α),
  sizeOf { method := method, param := param } = 1 + sizeOf method + sizeOf param
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.compCreatesLimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {E : Type u₃} →
              [ℰ : CategoryTheory.Category.{v₃, u₃} E] →
                (F : CategoryTheory.Functor C D) →
                  (G : CategoryTheory.Functor D E) →
                    [CategoryTheory.CreatesLimitsOfShape J F] →
                      [CategoryTheory.CreatesLimitsOfShape J G] → CategoryTheory.CreatesLimitsOfShape J (F.comp G)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hom_ext_iff : ∀ {X Y : FinBddDistLat} {f g : X ⟶ Y}, f = g ↔ FinBddDistLat.Hom.hom f = FinBddDistLat.Hom.hom g
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_flip : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  P.flip.pairing i j = P.pairing j i
-- Mathlib.Analysis.RCLike.Basic
RCLike.continuous_re : ∀ {K : Type u_1} [inst : RCLike K], Continuous ⇑RCLike.re
-- Mathlib.GroupTheory.Abelianization.Defs
/-- Use `map` as the preferred simp normal form.  -/
Abelianization.lift_of_comp : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (f : G →* H),
  Abelianization.lift (Abelianization.of.comp f) = Abelianization.map f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.add_iff_left : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : AddCommGroup β] [IsTopologicalAddGroup β],
  MeasureTheory.StronglyMeasurable f → (MeasureTheory.StronglyMeasurable (g + f) ↔ MeasureTheory.StronglyMeasurable g)
-- Init.Data.Rat.Lemmas
Rat.abs_zero : Rat.abs 0 = 0
-- Lean.Elab.Tactic.Grind.Main
_private.Lean.Elab.Tactic.Grind.Main.0.Lean.Elab.Tactic.elabGrindPattern.elabCnstrs : Array Lean.Expr →
  Option (Lean.TSyntax `Lean.Parser.Command.grindPatternCnstrs) →
    Lean.Elab.TermElabM (List Lean.Meta.Grind.EMatchTheoremConstraint)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofNotLE? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_eval_sub : ∀ {R : Type u_1} [inst : CommRing R] (r : R) (f : Polynomial R) (s : R),
  Polynomial.eval (s - r) ((Polynomial.taylor r) f) = Polynomial.eval s f
-- Mathlib.Data.Nat.Factorization.Basic
Nat.exists_eq_pow_of_pow_eq_pow : ∀ {a b m n : ℕ}, m ≠ 0 ∨ n ≠ 0 → a ^ m = b ^ n → ∃ c, a = c ^ (n / m.gcd n) ∧ b = c ^ (m / m.gcd n)
-- Init.Prelude
/-- Converts a `String` into a `Substring` that denotes the entire string.
 -/
String.toRawSubstring : String → Substring.Raw
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.length_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.mapLe h p).length = p.length
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.μ_limsup_le_one : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {s : ℕ → ℕ},
  (∀ (n : ℕ), s n ≤ n) →
    ∀ {x : R} {ψ : ℕ → ℕ},
      Filter.Tendsto ((fun n => ↑(s n) / ↑n) ∘ ψ) Filter.atTop (nhds 0) →
        Filter.limsup (fun n => μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) Filter.atTop ≤ 1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, Monotone CategoryTheory.Sieve.generate
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points to `s`, then the average value of `g ∘ f` is less than or equal to the value of `g`
at the average value of `f` provided that both `f` and `g ∘ f` are integrable. See also
`ConcaveOn.le_map_centerMass` for a finite sum version of this lemma.  -/
ConcaveOn.le_map_average : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [NeZero μ],
  ConcaveOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ → ⨍ (x : α), g (f x) ∂μ ≤ g (⨍ (x : α), f x ∂μ)
-- Mathlib.Combinatorics.Additive.FreimanHom
isMulFreimanIso_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {f : α → β} {n : ℕ},
  IsMulFreimanIso n ∅ ∅ f