mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.groupoidProd : {α : Type u} →
  {β : Type v} → [CategoryTheory.Groupoid α] → [CategoryTheory.Groupoid β] → CategoryTheory.Groupoid (α × β)
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of seminormed groups, using the sup norm.  -/
Pi.normedAddGroup : {ι : Type u_1} → {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → NormedAddGroup (G i)] → NormedAddGroup ((i : ι) → G i)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_eq_rpow_prod : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {B : Type u_2} [inst_10 : PartialOrder B]
  [inst_11 : Ring B] [inst_12 : StarRing B] [inst_13 : TopologicalSpace B] [inst_14 : StarOrderedRing B]
  [inst_15 : Algebra ℝ B] [inst_16 : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint]
  [inst_17 : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsSemitopologicalRing B] [T2Space B]
  [inst_20 : StarOrderedRing (A × B)] [inst_21 : NonnegSpectrumClass ℝ B] [inst_22 : NonnegSpectrumClass ℝ (A × B)]
  {a : A} {b : B} {x : ℝ},
  IsUnit a →
    IsUnit b →
      autoParam (0 ≤ a) CFC.rpow_eq_rpow_prod._auto_1 →
        autoParam (0 ≤ b) CFC.rpow_eq_rpow_prod._auto_3 → CFC.rpow (a, b) x = (a, b) ^ x
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.below.prec : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop} {n : ℕ} {f : List.Vector ℕ n → ℕ}
  {g : List.Vector ℕ (n + 2) → ℕ} (a : Nat.Primrec' f) (a_1 : Nat.Primrec' g),
  Nat.Primrec'.below a → motive f a → Nat.Primrec'.below a_1 → motive g a_1 → Nat.Primrec'.below ⋯
-- Init.System.IO
IO.FS.DirEntry.mk.sizeOf_spec : ∀ (root : System.FilePath) (fileName : String),
  sizeOf { root := root, fileName := fileName } = 1 + sizeOf root + sizeOf fileName
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.gciMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f),
  AddSubsemigroup.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instCategory : CategoryTheory.Category.{u, u + 1} AddMonCat
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β k}, (m.containsThenInsert k v).1 = m.contains k
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Coindep.closure_compl : ∀ {α : Type u_2} {M : Matroid α} {X : Set α}, M.Coindep X → M.closure (M.E \ X) = M.E
-- Mathlib.Data.Stream.Init
Stream'.get_interleave_right : ∀ {α : Type u} (n : ℕ) (s₁ s₂ : Stream' α), (s₁ ⋈ s₂).get (2 * n + 1) = s₂.get n
-- Mathlib.Data.Opposite
/-- The type of objects of the opposite of `α`; used to define the opposite category.

Now that Lean 4 supports definitional eta equality for records,
both `unop (op X) = X` and `op (unop X) = X` are definitional equalities.
 -/
«term_ᵒᵖ» : Lean.TrailingParserDescr
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- An abbreviation for `S.fintypeDiagram ⋙ FintypeCat.toProfinite`.  -/
LightProfinite.diagram : LightProfinite → CategoryTheory.Functor ℕᵒᵖ LightProfinite
-- Std.Http.Protocol.H1.Message
/-- Checks whether the message indicates that the connection should be kept alive.
 -/
Std.Http.Protocol.H1.Message.Head.shouldKeepAlive : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Message.Head dir → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, Std.DTreeMap.Raw.Const.getD t a fallback = t.getD a fallback
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec.eq_def : ∀ {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)) (n : ℕ),
  Nat.binaryRec zero bit n =
    if n0 : n = 0 then ⋯ ▸ zero
    else
      have x := bit (1 &&& n != 0) (n >>> 1) (Nat.binaryRec zero bit (n >>> 1));
      ⋯ ▸ x
-- Mathlib.Data.Rat.Lemmas
Rat.intCast_sub_den : ∀ (n : ℤ) (q : ℚ), (↑n - q).den = q.den
-- Mathlib.Analysis.Complex.Exponential
Complex.isCauSeq_norm_exp : ∀ (z : ℂ), IsCauSeq abs fun n => ∑ m ∈ Finset.range n, ‖z ^ m / ↑m.factorial‖
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.DHashMap.Const.unitOfList l).getKey? k' = some k
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (U : CategoryTheory.Comonad C) [inst_2 : U.Additive] (F G : U.Coalgebra), CategoryTheory.Comonad.Coalgebra.Hom.f 0 = 0
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Skeleton.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.Skeleton C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.IsInduced.adj : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.IsInduced → ∀ {a b : ↑G'.verts}, G'.Adj ↑a ↑b ↔ G.Adj ↑a ↑b
-- Init.PropLemmas
Decidable.imp_or : ∀ {a b c : Prop} [Decidable a], a → b ∨ c ↔ (a → b) ∨ (a → c)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_inf_le_add : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f₁ f₂ : Module.End R M)
  (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞),
  Commute f₁ f₂ → (f₁.genEigenspace μ₁) k₁ ⊓ (f₂.genEigenspace μ₂) k₂ ≤ ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) (k₁ + k₂)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian.  -/
ProbabilityTheory.gaussianReal_map_div_const : ∀ {μ : ℝ} {v : NNReal} (c : ℝ),
  MeasureTheory.Measure.map (fun x => x / c) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (μ / c) (v / NNReal.mk (c ^ 2) ⋯)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.toHoCat_map_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.FibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.FibrantObject.homRel C f g →
    HomotopicalAlgebra.FibrantObject.toHoCat.map f = HomotopicalAlgebra.FibrantObject.toHoCat.map g
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul'' : ∀ {α : Type u_1} {inst : PseudoMetricSpace α} {inst_1 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : IsUnifLocDoublingMeasure μ],
  ∃ C,
    ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor from the costructured arrow category on `L` over `R.obj b` to the costructured
arrow category on `snd L R` over `b : B`.  -/
CategoryTheory.Comma.costructuredArrowSndInclusion : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (b : B) →
                  CategoryTheory.Functor (CategoryTheory.CostructuredArrow L (R.obj b))
                    (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.one_lt_cosh : ∀ {x : ℝ}, 1 < Real.cosh x ↔ x ≠ 0
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_add : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {m n : ℕ} {a : α},
  Std.PRange.succMany (m + n) a = Std.PRange.succMany n (Std.PRange.succMany m a)
-- Mathlib.Order.Height
Set.not_isChain_of_chainHeight_lt_encard : ∀ {α : Type u_1} (r : α → α → Prop) (s t : Set α), t ⊆ s → s.chainHeight r < t.encard → ¬IsChain r t
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.instLiftingFunctorOppositeSheafPresheafToSheafWPresheafFiberSheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                  CategoryTheory.Localization.Lifting (CategoryTheory.presheafToSheaf J A) J.W Φ.presheafFiber
                    Φ.sheafFiber
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.natDegree_coeff_preΨ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree✝ n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree✝ n) = ↑(WeierstrassCurve.expCoeff✝ n)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instIsEquivalenceIntRingCatForget₂AlgHomCarrierRingHomCarrier : (CategoryTheory.forget₂ (AlgCat ℤ) RingCat).IsEquivalence
-- Mathlib.Algebra.Group.EvenFunction
/-- A function `f` is _odd_ if it satisfies `f (-x) = -f x` for all `x`.  -/
Function.Odd : {α : Type u_1} → {β : Type u_2} → [Neg α] → [Neg β] → (α → β) → Prop
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.orderIsoMapComap_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') (N : LieSubmodule R L M),
  (LieSubmodule.orderIsoMapComap e) N = LieSubmodule.map e.toLieModuleHom N
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates finite products, then `F.unop : C ⥤ D` creates finite
coproducts.  -/
CategoryTheory.Limits.createsFiniteCoproductsUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteProducts F] → CategoryTheory.Limits.CreatesFiniteCoproducts F.unop
-- Mathlib.Algebra.Module.Basic
map_inv_natCast_smul : ∀ {M : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {F : Type u_5}
  [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7)
  [inst_4 : DivisionSemiring R] [inst_5 : DivisionSemiring S] [inst_6 : Module R M] [inst_7 : Module S M₂] (n : ℕ)
  (x : M), f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.expandReportIssueMacro : Lean.Syntax → Lean.MacroM Lean.DoElem
-- Mathlib.Util.WithWeakNamespace
/-- Changes the current namespace without causing scoped things to go out of scope  -/
Lean.Elab.Command.commandWith_weak_namespace__ : Lean.ParserDescr
-- Mathlib.Topology.Constructions
ContinuousAt.finInit : ∀ {X : Type u} [inst : TopologicalSpace X] {n : ℕ} {A : Fin (n + 1) → Type u_9}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (A i)] {f : X → (j : Fin (n + 1)) → A j} {x : X},
  ContinuousAt f x → ContinuousAt (fun a => Fin.init (f a)) x
-- Mathlib.Order.CompleteLattice.Basic
iInf_split_single : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (i₀ : β),
  ⨅ i, f i = f i₀ ⊓ ⨅ i, ⨅ (_ : i ≠ i₀), f i
-- Batteries.Classes.Order
Std.LawfulBCmp.toTransCmp : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {inst_2 : BEq α} {cmp : α → α → Ordering} [self : Std.LawfulBCmp cmp],
  Std.TransCmp cmp
-- Mathlib.Algebra.FreeMonoid.Symbols
FreeMonoid.mem_symbols : ∀ {α : Type u_1} [inst : DecidableEq α] {m : α} {a : FreeMonoid α}, m ∈ a.symbols ↔ m ∈ a
-- Lean.Parser.Tactic
Lean.Parser.Tactic.matchAlts.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Core
/-- The core of the composition of F and G is the composition of the cores.  -/
CategoryTheory.Functor.coreComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) → (G : CategoryTheory.Functor D E) → (F.comp G).core ≅ F.core.comp G.core
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.restrict_contract_eq_contract_restrict : ∀ {α : Type u_1} {R C : Set α} (M : Matroid α), C ⊆ R → (M.restrict R).contract C = (M.contract C).restrict (R \ C)
-- Aesop.Builder.Apply
Aesop.RuleBuilder.applyCore : Aesop.ElabRuleTerm →
  Option Aesop.RulePattern →
    Option Aesop.IndexingMode →
      Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Aesop.PhaseSpec → Lean.MetaM Aesop.LocalRuleSetMember
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] (p : P) {x : P},
  (s.signedInfDist p) x =
    ((signedDist (p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)))
        ↑((EuclideanGeometry.orthogonalProjection s) x))
      x
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.IsSetAlgebra.compl_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, MeasureTheory.IsSetAlgebra 𝒜 → ∀ ⦃s : Set α⦄, s ∈ 𝒜 → sᶜ ∈ 𝒜
-- Mathlib.Tactic.Translate.Reorder
/-- The syntax category for the reorder syntax.  -/
Lean.Parser.Category.translateReorder : Lean.Parser.Category
-- Mathlib.Algebra.DirectSum.Internal
mul_apply_eq_zero : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [inst_4 : Semiring R] [inst_5 : SetLike σ R] [inst_6 : AddSubmonoidClass σ R] {A : ι → σ}
  [inst_7 : SetLike.GradedMonoid A] {r r' : DirectSum ι fun i => ↥(A i)} {m n : ι},
  (∀ i < m, r i = 0) → (∀ i < n, r' i = 0) → ∀ ⦃k : ι⦄, k < m + n → (r * r') k = 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_ext_iff : ∀ {M N : AddMonCat} {f g : M ⟶ N}, f = g ↔ AddMonCat.Hom.hom f = AddMonCat.Hom.hom g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- `BoundedContinuousFunction.const` as a `RingHom`.  -/
BoundedContinuousFunction.C : {α : Type u} →
  {γ : Type w} →
    {𝕜 : Type u_1} →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : NormedRing γ] → [NormedAlgebra 𝕜 γ] → 𝕜 →+* BoundedContinuousFunction α γ
-- Mathlib.Analysis.Calculus.ParametricIntervalIntegral
/-- Differentiation under integral of `x ↦ ∫ t in a..b, F x t` at a given point `x₀`, assuming
`F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a neighborhood of `x₀` for ae `a`
(with a neighborhood independent of `a`) with integrable Lipschitz bound, and `F x` is ae-measurable
for `x` in a possibly smaller neighborhood of `x₀`.  -/
intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace 𝕜 E] {H : Type u_3} [inst_4 : NormedAddCommGroup H]
  [inst_5 : NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H},
  s ∈ nhds x₀ →
    (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
      IntervalIntegrable (F x₀) μ a b →
        MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b)) →
          (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) →
            IntervalIntegrable bound μ a b →
              (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasFDerivAt (fun x => F x t) (F' t) x₀) →
                IntervalIntegrable F' μ a b ∧
                  HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.neg : ℝ → ℝ
-- Mathlib.Algebra.Group.Subgroup.Defs
NegMemClass.coe_neg : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  (x : ↥H), ↑(-x) = -↑x
-- Mathlib.Order.PiLex
Pi.lex_le_iff_of_unique : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Unique ι] [inst_1 : LinearOrder ι] [inst_2 : (i : ι) → PartialOrder (β i)]
  {x y : Lex ((i : ι) → β i)}, x ≤ y ↔ x default ≤ y default
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.const_down_toOrderHom : ∀ (n : ℕ) (k : Fin (n + 1)) (m : SimplexCategoryᵒᵖ),
  SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.const n k m).down =
    (OrderHom.const (Fin ((Opposite.unop m).len + 1))) k
-- Mathlib.Geometry.Convex.Hull
Convexity.convexHull_min : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {C s : Set X}, s ⊆ C → Convexity.IsConvexSet R C → (Convexity.convexHull R) s ⊆ C
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → ∀ {fallback : α}, (t.insertIfNew k v).minKeyD fallback = k
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_tmod : ∀ (a b : ℤ), (a.tmod b).natAbs = a.natAbs % b.natAbs
-- Mathlib.Order.Category.DistLat
DistLat.instCoeSortType : CoeSort DistLat (Type u)
-- Mathlib.CategoryTheory.Opposites
Quiver.Hom.unop_op : ∀ {C : Type u₁} [inst : Quiver C] {X Y : C} (f : X ⟶ Y), f.op.unop = f
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- `r` is a unit as a section on the basic open defined by `r`.  -/
AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))),
  IsUnit ((CategoryTheory.ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r)
-- Lean.ResolveName
/-- Helper function for `resolveGlobalConstCore`.  -/
Lean.filterFieldList : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → List (Lean.Name × List String) → m (List Lean.Name)
-- Init.Data.BitVec.Bitblast
BitVec.ne_intMin_of_lt_of_msb_false : ∀ {w : ℕ} {x : BitVec w}, 0 < w → x.msb = false → x ≠ BitVec.intMin w
-- Mathlib.Analysis.Convex.Function
ConvexOn.lt_right_of_left_lt' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f →
    ∀ {x y : E} {a b : 𝕜}, x ∈ s → y ∈ s → 0 < a → 0 < b → a + b = 1 → f x < f (a • x + b • y) → f (a • x + b • y) < f y
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.map : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} {p q : Path x₀ x₁},
  p.Homotopic q → ∀ (f : C(X, Y)), (p.map ⋯).Homotopic (q.map ⋯)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.eq_1 : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : Fintype ι] (I : BoxIntegral.Box ι)
  (l : BoxIntegral.IntegrationParams) (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (y : F),
  BoxIntegral.HasIntegral I l f vol y =
    Filter.Tendsto (BoxIntegral.integralSum f vol) (BoxIntegral.IntegrationParams.toFilteriUnion I ⊤) (nhds y)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_reindex_hom_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)] (b : β) {Z : C}
  (h : ∐ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.reindex ε f).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f (ε b)) h
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.toPowerSeries_apply : ∀ {R : Type u_2} [inst : Semiring R] (f : HahnSeries ℕ R), HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxoLawfulHasSize : ∀ {n : ℕ}, Std.Rxo.LawfulHasSize (BitVec n)
-- Mathlib.Order.Partition.Finpartition
/-- Combine a family of partitions of pairwise disjoint elements into a partition of their sup.  -/
Finpartition.combine : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      [IsModularLattice α] →
        [DecidableEq α] →
          {ι : Type u_2} →
            {I : Finset ι} → {a : ι → α} → ((i : ι) → Finpartition (a i)) → I.SupIndep a → Finpartition (I.sup a)
-- Mathlib.RingTheory.Ideal.Maps
/-- Kernel of a ring homomorphism as an ideal of the domain.  -/
RingHom.ker : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : FunLike F R S] → [rcf : RingHomClass F R S] → F → Ideal R
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Reindexing by an equivalence and its inverse yields the original simplex.  -/
Affine.Simplex.reindex_reindex_symm : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)),
  (s.reindex e).reindex e.symm = s
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.HasFactorization.over : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C] (W₁ W₂ : CategoryTheory.MorphismProperty C)
  [W₁.HasFactorization W₂] (S : C), W₁.over.HasFactorization W₂.over
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyoneda_obj_obj_coe : ∀ (M : AddCommGrpCatᵒᵖ) (N : AddCommGrpCat), ↑((AddCommGrpCat.coyoneda.obj M).obj N) = (↑(Opposite.unop M) →+ ↑N)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_piecewise_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : CommSemiring 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] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (c : ι → R) (m : ι → M) (s : Finset ι),
  f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_coe_nnreal_real : Measurable NNReal.toReal
-- Mathlib.Logic.Equiv.Fin.Rotate
/-- The permutation on `Fin n` that adds `k` to each number.  -/
finCycle : {n : ℕ} → Fin n → Equiv.Perm (Fin n)