mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the centroid lies in the affine
span if the set is nonempty.  -/
centroid_mem_affineSpan_of_nonempty : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [CharZero k] {s : Finset ι} (p : ι → P),
  s.Nonempty → Finset.centroid k s p ∈ affineSpan k (Set.range p)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `sinh` is bijective, both injective and surjective.  -/
Real.sinh_bijective : Function.Bijective Real.sinh
-- Mathlib.Order.CompleteBooleanAlgebra
hnot_eq_sInf_codisjoint : ∀ {α : Type u} [inst : Order.Coframe α] {a : α}, ￢a = sInf {w | Codisjoint a w}
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_map_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {f : α → β} {g : β → ε},
  MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ →
      MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).counitIso =
    (CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.inv α.hom).symm ≪≫
      CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq ⋯ ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransId
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasStrictFDerivAt_iff_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x ↔ (fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[𝕜; nhds (x, x)] fun p => p.1 - p.2
-- Mathlib.Algebra.BigOperators.Pi
AddMonoidHom.functions_ext : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → AddCommMonoid (M i)] [Finite I]
  (N : Type u_9) [inst_3 : AddCommMonoid N] (g h : ((i : I) → M i) →+ N),
  (∀ (i : I) (x : M i), g (Pi.single i x) = h (Pi.single i x)) → g = h
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.codisjoint_left : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α], Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.mono : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {t s : Set ι}, LinearIndepOn R v s → t ⊆ s → LinearIndepOn R v t
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_le_iff : ∀ {ι : Type u_3} {f : ι → Ordinal.{max u_4 u_3}} {a : Ordinal.{max u_3 u_4}}, Ordinal.lsub f ≤ a ↔ ∀ (i : ι), f i < a
-- Mathlib.LinearAlgebra.FreeModule.Int
Int.subgroup_index_ne_zero_iff : ∀ {ι : Type u_1} [Finite ι] {H : Subgroup (ι → Multiplicative ℤ)}, H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))
-- Init.Data.SInt.Basic
/-- Arithmetic right shift for 64-bit signed integers. Usually accessed via the `<<<` operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.shiftRight : Int64 → Int64 → Int64
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.filter f m) k fallback =
      (Option.filter (fun x => f k' x) (Std.ExtDHashMap.Const.get? m k)).getD fallback
-- Mathlib.Util.Qq
/-- Variant of `inferTypeQ` that yields a type in `Type u` rather than `Sort u`.
Throws an error if the type is a `Prop` or if it's otherwise not possible to represent
the universe as `Type u` (for example due to universe level metavariables).  -/
Qq.inferTypeQ' : Lean.Expr →
  Lean.MetaM
    ((u : Lean.Level) ×
      (α :
        have u := u;
        Q(Type u)) ×
        Q(«$α»))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_eq_range_algebraMap_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  ↑(IntermediateField.adjoin F S) = Set.range ⇑(algebraMap (↥(IntermediateField.adjoin F S)) E)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unicodeVariant.sizeOf_spec : ∀ (s : String) (selector : Option Char),
  sizeOf (Mathlib.Linter.TextBased.StyleError.unicodeVariant✝ s selector) = 1 + sizeOf s + sizeOf selector
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_zero_left : ∀ {f : Bool → Bool → Bool} (m : ℕ), Nat.bitwise f 0 m = if f false true = true then m else 0
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.hi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (self : W₁.MapFactorizationData W₂ f), W₁ self.i
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.none : Lean.Meta.ACLt.ReduceMode
-- Aesop.Stats.Basic
Aesop.instInhabitedStats : Inhabited Aesop.Stats
-- Init.Data.Nat.Basic
Nat.lt_of_le_pred : ∀ {m : ℕ} {n : ℕ}, 0 < m → n ≤ m.pred → n < m
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reuse.inj : ∀ {x : Lean.IR.VarId} {i : Lean.IR.CtorInfo} {updtHeader : Bool} {ys : Array Lean.IR.Arg} {x_1 : Lean.IR.VarId}
  {i_1 : Lean.IR.CtorInfo} {updtHeader_1 : Bool} {ys_1 : Array Lean.IR.Arg},
  Lean.IR.Expr.reuse x i updtHeader ys = Lean.IR.Expr.reuse x_1 i_1 updtHeader_1 ys_1 →
    x = x_1 ∧ i = i_1 ∧ updtHeader = updtHeader_1 ∧ ys = ys_1
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_sup : ∀ {V : Type u} {G : SimpleGraph V} {H₁ H₂ : G.Subgraph}, (H₁ ⊔ H₂).edgeSet = H₁.edgeSet ∪ H₂.edgeSet
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
_private.Mathlib.Topology.Algebra.InfiniteSum.NatInt.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Lean.Server.Rpc.Basic
Lean.Server.rpcStoreRef : {α : Type u_1} → [TypeName α] → Lean.Server.WithRpcRef α → StateM Lean.Server.RpcObjectStore Lean.Lsp.RpcRef
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K) {Z : C} (h : (F.obj j).obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F j).app k) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.evaluation K C).obj k)) j) h
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.of_uncurry_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β → γ}, Measurable (Function.uncurry f) → ∀ {x : α}, Measurable (f x)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- The isometry between two weighted sum of squares of equal weights.  -/
QuadraticForm.weightedSumSquaresCongr : {ι : Type u_10} →
  {S : Type u_11} →
    {R : Type u_12} →
      [inst : Fintype ι] →
        [inst_1 : CommSemiring R] →
          [inst_2 : Monoid S] →
            [inst_3 : DistribMulAction S R] →
              [inst_4 : SMulCommClass S R R] →
                {w w' : ι → S} →
                  w = w' → (QuadraticMap.weightedSumSquares R w).IsometryEquiv (QuadraticMap.weightedSumSquares R w')
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- The annihilating ideal generator is a member of the annihilating ideal.  -/
Polynomial.annIdealGenerator_mem : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  Polynomial.annIdealGenerator 𝕜 a ∈ Polynomial.annIdeal 𝕜 a
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
CategoryTheory.Limits.ι_sigmaConstCokernelCofork_π_eq_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (R : C)
  {α : Type u_1} {β : Type u_2} (f : α → β) [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] [inst_4 : CategoryTheory.Limits.HasCoproduct fun x => R]
  (a : α) {Z : C} (h : (∐ fun x => R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) (f a))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.sigmaConstCokernelCofork R f)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpaceWeightSpaceProductAux.eq_1 : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (M : Type u_3) [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] {χ₁ χ₂ χ₃ : ↥H → R} (hχ : χ₁ + χ₂ = χ₃),
  LieAlgebra.rootSpaceWeightSpaceProductAux R L H M hχ =
    { toFun := fun x => { toFun := fun m => ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
-- Lean.Elab.DeclUtil
Lean.Meta.forallTelescopeCompatibleAux : {α : Type} →
  (Array Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM α) → ℕ → Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.pointBotFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C),
  CategoryTheory.GrothendieckTopology.pointBotFunctor.obj X = CategoryTheory.GrothendieckTopology.pointBot X
-- Init.System.FilePath
/-- Extracts the stem (non-extension) part of `p.fileName`.

If the filename contains multiple extensions, then only the last one is removed. Returns `none` if
there is no file name at the end of the path.

Examples:
 * `("app.exe" : System.FilePath).fileStem = some "app"`
 * `("file.tar.gz" : System.FilePath).fileStem = some "file.tar"`
 * `("files/" : System.FilePath).fileStem = none`
 * `("files/picture.jpg" : System.FilePath).fileStem = some "picture"`
 -/
System.FilePath.fileStem : System.FilePath → Option String
-- Mathlib.Algebra.Order.Group.Equiv
symm_toLexMulEquiv : ∀ (α : Type u_1) [inst : Mul α], (toLexMulEquiv α).symm = ofLexMulEquiv α
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : α → C) (g : β → C)
  [CategoryTheory.Limits.HasCoproduct f] (e : β ≃ α) (iso : (j : β) → g j ≅ f (e j)),
  CategoryTheory.Limits.HasCoproduct g
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.mk.injEq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toFun : C(X, Y))
  (invFun : C(Y, X)) (left_inv : (invFun.comp toFun).Homotopic (ContinuousMap.id X))
  (right_inv : (toFun.comp invFun).Homotopic (ContinuousMap.id Y)) (toFun_1 : C(X, Y)) (invFun_1 : C(Y, X))
  (left_inv_1 : (invFun_1.comp toFun_1).Homotopic (ContinuousMap.id X))
  (right_inv_1 : (toFun_1.comp invFun_1).Homotopic (ContinuousMap.id Y)),
  ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toFun = toFun_1 ∧ invFun = invFun_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instAddCommSemigroup : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Affine F} → [DecidableEq F] → AddCommSemigroup W.Point
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_im : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), RCLike.im (inner 𝕜 x x) = 0
-- Mathlib.MeasureTheory.Integral.Prod
/-- Double integrals commute with subtraction. This is the version with `(f - g) (x, y)`
(instead of `f (x, y) - g (x, y)`) in the LHS.  -/
MeasureTheory.integral_integral_sub' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f g : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫ (x : α), ∫ (y : β), (f - g) (x, y) ∂ν ∂μ =
        ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPure_1 : ∀ {φ : Prop} {σ : Type u_1} (σs : List (Type u_1)) (P : Std.Do.SPred σs) [inst : Std.Do.SPred.Tactic.IsPure P φ],
  Std.Do.SPred.Tactic.IsPure (fun x => P) φ
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.stateStack : {α β σ : Type} → Lean.ScopedEnvExtension.StateStack α β σ → List (Lean.ScopedEnvExtension.State σ)
-- Std.Data.TreeSet.Raw.Lemmas
_private.Std.Data.TreeSet.Raw.Lemmas.0.Std.TreeSet.Raw.equiv_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ ↔ t₁.inner.Equiv t₂.inner
-- Mathlib.Dynamics.Ergodic.AddCircle
AddCircle.ergodic_zsmul : ∀ {T : ℝ} [hT : Fact (0 < T)] {n : ℤ}, 1 < |n| → Ergodic (fun y => n • y) MeasureTheory.volume
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.logOrderIso_apply : ∀ (x : ENNReal), ENNReal.logOrderIso x = x.log
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Interpreting the legs of a cocone as a costructured arrow, interpreting this arrow as an arrow
over the cocone point, and finally forgetting the arrow is the same as just applying the
functor the cocone was over.  -/
CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            c.toCostructuredArrow.comp
                ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (CategoryTheory.Over.forget c.pt)) ≅
              F
-- Mathlib.Topology.Path
Path.map_trans : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y z : X} (γ : Path x y)
  (γ' : Path y z) {f : X → Y} (h : Continuous f), (γ.trans γ').map h = (γ.map h).trans (γ'.map h)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- A `HomologyPretheory` is the data of an Eilenberg-Steenrod homology theory.  -/
TopPair.HomologyPretheory : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → ComplexShape ι → Type (max (max (max (u + 1) u_1) u_2) v_1)
-- Mathlib.Topology.Order.Basic
pi_Ici_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a x : (i : ι) → X i},
  (∀ (i : ι), a i < x i) → Set.Ici a ∈ nhds x
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A sufficient criterion for a convex cone `C` to be reproducing is that `Set.univ` is a subset
of `C - C`.  -/
ConvexCone.IsReproducing.of_univ_subset : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {C : ConvexCone R M}, Set.univ ⊆ ↑C - ↑C → C.IsReproducing
-- Mathlib.Algebra.Group.Torsion
nsmul_eq_zero_iff : ∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M}, n • a = 0 ↔ a = 0 ∨ n = 0
-- Lean.Environment
Lean.PersistentEnvExtensionState.importedEntries : {α σ : Type} → Lean.PersistentEnvExtensionState α σ → Array (Array α)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_preimage : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (g : β → γ)
  (s : Set γ), ⇑(MeasureTheory.SimpleFunc.map g f) ⁻¹' s = ⇑f ⁻¹' ↑({b ∈ f.range | g b ∈ s})
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.IntegrationParams.McShane.eq_1 : BoxIntegral.IntegrationParams.McShane = { bRiemann := false, bHenstock := false, bDistortion := false }
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → List α → Sort u_2) →
    (x x_1 x_2 : List α) →
      ((l₂ acc : List α) → motive [] l₂ acc) →
        ((l₁ acc : List α) → (l₁ = [] → False) → motive l₁ [] acc) →
          ((x : α) → (xs : List α) → (y : α) → (ys acc : List α) → motive (x :: xs) (y :: ys) acc) → motive x x_1 x_2
-- Std.Async.Basic
/-- A `MaybeTask α` represents a computation that either:

- Is immediately available as an `α` value, or
- Is an asynchronous computation that will eventually produce an `α` value.
 -/
Std.Async.MaybeTask : Type → Type
-- Mathlib.Computability.RE
Partrec.merge' : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α →. σ},
  Partrec f →
    Partrec g → ∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.mk.sizeOf_spec : ∀ (ref m returnType : Lean.Syntax) (mutableVars : Lean.Elab.Term.Do.VarSet) (insideFor : Bool),
  sizeOf { ref := ref, m := m, returnType := returnType, mutableVars := mutableVars, insideFor := insideFor } =
    1 + sizeOf ref + sizeOf m + sizeOf returnType + sizeOf mutableVars + sizeOf insideFor
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.instBiprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] [CategoryTheory.Projective P] [CategoryTheory.Projective Q],
  CategoryTheory.Projective (P ⊞ Q)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)],
  P.isoClosure.colimitsClosure J = P.colimitsClosure J
-- Mathlib.Data.Int.LeastGreatest
Int.coe_leastOfBdd_eq : ∀ {P : ℤ → Prop} [inst : DecidablePred P] {b b' : ℤ} (Hb : ∀ (z : ℤ), P z → b ≤ z) (Hb' : ∀ (z : ℤ), P z → b' ≤ z)
  (Hinh : ∃ z, P z), ↑(b.leastOfBdd Hb Hinh) = ↑(b'.leastOfBdd Hb' Hinh)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_coeff : ∀ (ctx : Int.Internal.Linear.Context) (k₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (k₂ : ℤ) (p₂ : Int.Internal.Linear.Poly)
  (g : ℤ),
  Int.Internal.Linear.dvd_coeff_cert k₁ p₁ k₂ p₂ g = true →
    k₁ ∣ Int.Internal.Linear.Poly.denote' ctx p₁ → k₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.instPartialOrder : {A : Type u_1} → [NonUnitalCStarAlgebra A] → PartialOrder (Unitization ℂ A)
-- Init.Data.Array.Lemmas
Array.mem_append_right : ∀ {α : Type u_1} {a : α} (xs : Array α) {ys : Array α}, a ∈ ys → a ∈ xs ++ ys
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.mk.inj : ∀ {m : Type w → Type w'} {α : Type w} {Property : α → Prop} {operation : m (Subtype Property)} {Property_1 : α → Prop}
  {operation_1 : m (Subtype Property_1)},
  { Property := Property, operation := operation } = { Property := Property_1, operation := operation_1 } →
    Property = Property_1 ∧ operation ≍ operation_1
-- Mathlib.GroupTheory.Torsion
AddCommMonoid.torsion_sum : ∀ (G : Type u_1) {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H],
  AddCommMonoid.addTorsion (G × H) = (AddCommMonoid.addTorsion G).prod (AddCommMonoid.addTorsion H)
-- Mathlib.RingTheory.Ideal.Span
isPrincipalIdealRing_iff : ∀ (R : Type u) [inst : Semiring R], IsPrincipalIdealRing R ↔ ∀ (S : Ideal R), Submodule.IsPrincipal S
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_neg : ∀ {α β : Type u} (f : α → β) (x : FreeAbelianGroup α), f <$> (-x) = -f <$> x
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.one_counit_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit h) =
    h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      compare k k' = Ordering.eq →
        ∀
          {h' :
            Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) = true},
          k ∉ t →
            List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
              k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey k' h' = k
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.condition : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C))
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F i) ((F.obj (Opposite.op i)).map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F j) ((F.map f.op).app j)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.diff m₂).getKey? k = none
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.mul_neg : ∀ {R : Type u_2} [inst : Ring R] (a b : R), a * -b = -(a * b)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.map_monotone : ∀ {n : ℕ} (d : ℕ), Monotone ⇑(Behrend.map d)
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivWithinAt.pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x →
    ∀ (n : ℕ), HasDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ordered_keys_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => cmp a.1 b.1 = Ordering.lt) (Std.DTreeMap.Raw.Const.toList t)
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_succ : ∀ {l w : ℕ} {x : BitVec (l * w)} {n : ℕ} {acc : BitVec w},
  BitVec.addRecAux✝ x (n + 1) acc = BitVec.addRecAux✝ x n (acc + BitVec.extractLsb' (n * w) w x)