mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.SplitBy
/-- A characterization of `splitBy m r` as the unique list `l` such that:

* The lists of `l` join to `m`.
* It does not contain the empty list.
* Every list in `l` is `IsChain` of `r`.
* The last element of each list in `l` is not related by `r` to the head of the next.
 -/
List.splitBy_eq_iff : ∀ {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List (List α)},
  List.splitBy r m = l ↔
    m = l.flatten ∧
      [] ∉ l ∧
        (∀ m ∈ l, List.IsChain (fun x y => r x y = true) m) ∧
          List.IsChain (fun a b => ∃ (ha : a ≠ []) (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l
-- Mathlib.CategoryTheory.Enriched.Basic
/-- `X ⟶[V] Y` is the `V` object of morphisms from `X` to `Y`.  -/
CategoryTheory.EnrichedCategory.Hom : {V : Type v} →
  {inst : CategoryTheory.Category.{w, v} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u₁} → [self : CategoryTheory.EnrichedCategory V C] → C → C → V
-- Init.Conv
/-- Traverses into the function of a (unary) function application.
For example, `| f a b` turns into `| f a`. (Use `arg 0` to traverse into `f`.)   -/
Lean.Parser.Tactic.Conv.fun : Lean.ParserDescr
-- Init.Data.BitVec.Bitblast
/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_le`.  -/
BitVec.signExtend_neg_of_ne_intMin : ∀ {v w : ℕ} (b : BitVec v), b ≠ BitVec.intMin v → BitVec.signExtend w (-b) = -BitVec.signExtend w b
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasFDerivWithinAt.hasLineDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s : Set E} {x : E} {L : E →L[𝕜] F}, HasFDerivWithinAt f L s x → ∀ (v : E), HasLineDerivWithinAt 𝕜 f (L v) s x v
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.card_base_support_eq_two : ∀ {ι : 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} [P.IsG2] (b : P.Base)
  [Finite ι] [CharZero R] [IsDomain R], b.support.card = 2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams.mk : Lean.Lsp.TextDocumentPositionParams → String → Lean.Lsp.RenameParams
-- Mathlib.Util.Export
Lean.Export.State.names : Lean.Export.State → Lean.Export.Alloc Lean.Name
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.ofQuaternion_toQuaternion : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)),
  CliffordAlgebraQuaternion.ofQuaternion (CliffordAlgebraQuaternion.toQuaternion c) = c
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_infty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  ContMDiffAt I I' (↑⊤) f x ↔ ∀ (n : ℕ), ContMDiffAt I I' (↑n) f x
-- Mathlib.RingTheory.SimpleModule.Isotypic
LinearMap.le_comap_isotypicComponent : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup S] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R S]
  [IsSimpleModule R S] (f : M →ₗ[R] N), isotypicComponent R M S ≤ Submodule.comap f (isotypicComponent R N S)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G}, ↑U ≤ ↑V ↔ U ≤ V
-- Init.Data.SInt.Lemmas
Int32.add_mul : ∀ {a b c : Int32}, (a + b) * c = a * c + b * c
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finite : ∀ {G : Type u} [inst : AddMonoid G],
  (∀ (g : G), 0 < addOrderOf g) → (AddMonoid.exponent G ≠ 0 ↔ (Set.range addOrderOf).Finite)
-- Mathlib.Algebra.Ring.Parity
Odd.sub_odd : ∀ {α : Type u_2} [inst : Ring α] {a b : α}, Odd a → Odd b → Even (a - b)
-- Batteries.Data.Fin.Basic
/-- Inner loop for `Fin.dfoldlM`.
  ```
Fin.foldM.loop n α f i h xᵢ = do
  let xᵢ₊₁ : α (i+1) ← f i xᵢ
  ...
  let xₙ : α n ← f (n-1) xₙ₋₁
  pure xₙ
```
 -/
Fin.dfoldlM.loop : {m : Type u_1 → Type u_2} →
  [Monad m] →
    (n : ℕ) →
      (α : Fin (n + 1) → Type u_1) →
        ((i : Fin n) → α i.castSucc → m (α i.succ)) → (i : ℕ) → (h : i < n + 1) → α ⟨i, h⟩ → m (α (Fin.last n))
-- Mathlib.Analysis.Complex.Basic
Complex.instProperSpace : ProperSpace ℂ
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
ConvexOn.comp_rnDeriv_map_le : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} {g : 𝓧 → 𝓨},
  μ.AbsolutelyContinuous ν →
    Measurable g →
      MeasureTheory.StronglyMeasurable f →
        ConvexOn ℝ (Set.Ici 0) f →
          ContinuousWithinAt f (Set.Ici 0) 0 →
            MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
              (fun x => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g x)).toReal) ≤ᵐ[ν]
                ν[fun x => f (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
-- Init.Data.Vector.Basic
/-- Makes a vector of size `n` with all cells containing `v`.  -/
Vector.replicate : {α : Type u_1} → (n : ℕ) → α → Vector α n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_diff_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ((t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).keysArray.isEmpty = (↑m).isEmpty
-- Init.Data.String.Basic
/-- Returns the byte at the given position in the string, or `none` if the position is the end
position.  -/
String.Slice.Pos.get? : {s : String.Slice} → s.Pos → Option Char
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_sq : ∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R),
  Polynomial.derivative (p ^ 2) = Polynomial.C 2 * p * Polynomial.derivative p
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts a `Nat` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofNat : Float.Model.Format → ℕ → Float.Model.UnpackedFloat
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport.module : Lean.Lsp.LeanImport → Lean.Lsp.LeanModule
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.mk.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {binderName : Lean.Name} {type : Lean.Expr} {borrow : Bool}
  {fvarId_1 : Lean.FVarId} {binderName_1 : Lean.Name} {type_1 : Lean.Expr} {borrow_1 : Bool},
  { fvarId := fvarId, binderName := binderName, type := type, borrow := borrow } =
      { fvarId := fvarId_1, binderName := binderName_1, type := type_1, borrow := borrow_1 } →
    fvarId = fvarId_1 ∧ binderName = binderName_1 ∧ type = type_1 ∧ borrow = borrow_1
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the projection to the image  -/
CategoryTheory.Abelian.AbelianStruct.imageπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Abelian.AbelianStruct f) → X ⟶ self.image
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.numeratorHom_apply : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r : R},
  AddOreLocalization.numeratorHom r = r -ₒ 0
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rci : ∀ {α : Type u_1} {xs : List α} {lo : ℕ},
  Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (List.drop lo xs).toArray
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.withCatchingRuntimeEx : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.prod_left_iff : ∀ {α : Type u_1} {I : Type u_2} [inst : CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I},
  IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_ne_zero_iff : ∀ {n k : ℕ}, n.choose k ≠ 0 ↔ k ≤ n
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoals.mk.inj : ∀ {goals goals_1 : Array Lean.Widget.InteractiveGoal}, { goals := goals } = { goals := goals_1 } → goals = goals_1
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ofHom_id : ∀ {X : Type u} [inst : AddGroup X],
  AddGrpCat.ofHom (AddMonoidHom.id X) = CategoryTheory.CategoryStruct.id (AddGrpCat.of X)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.factor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f.hom)
      (CategoryTheory.Limits.image.map sq) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.Limits.factorThruImage g.hom)
-- Mathlib.Order.Antisymmetrization
AntisymmRel.decidableRel : {α : Type u_1} → {r : α → α → Prop} → [DecidableRel r] → DecidableRel (AntisymmRel r)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.closure_eq_closure_iff_eq_or_dep : ∀ {α : Type u_1} {M : Matroid α} {e f : α},
  M.IsNonloop e → M.IsNonloop f → (M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f})
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- We can turn any colimit cocone over a pair into a bilimit bicone.  -/
CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {t : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)} →
          (ht : CategoryTheory.Limits.IsColimit t) → (CategoryTheory.Limits.BinaryBicone.ofColimitCocone ht).IsBilimit
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticM : Lean.Name → Aesop.RuleTacDescr
-- Mathlib.Data.Sum.Order
Sum.swap_le_swap_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α ⊕ β}, a.swap ≤ b.swap ↔ a ≤ b
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- `HasExactLimitsOfShape` can be "pushed forward" along initial functors  -/
CategoryTheory.hasExactLimitsOfShape_of_initial : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] {J : Type u_1}
  {J' : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_1} J] [inst_3 : CategoryTheory.Category.{v_2, u_2} J']
  (F : CategoryTheory.Functor J J') [F.Initial] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J' C]
  [inst_6 : CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C],
  CategoryTheory.HasExactLimitsOfShape J' C
-- Mathlib.Logic.Equiv.Defs
Equiv.symmEquiv_symm_apply_symm_apply : ∀ (α : Sort u_1) (β : Sort u_2) (e : β ≃ α) (a : β), ((Equiv.symmEquiv α β).symm e).symm a = e.toFun a
-- Init.Data.Iterators.Consumers.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.Iter.size : {α β : Type u_1} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → ℕ
-- Mathlib.Geometry.Euclidean.Volume.Measure
MeasureTheory.euclideanHausdorffMeasure_homothety_preimage : ∀ {𝕜 : Type u_3} {V : Type u_4} {P : Type u_5} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor V P]
  [inst_6 : BorelSpace P] (d : ℕ) (x : P) {c : 𝕜},
  c ≠ 0 →
    ∀ (s : Set P),
      (MeasureTheory.Measure.euclideanHausdorffMeasure d) (⇑(AffineMap.homothety x c) ⁻¹' s) =
        ‖c‖₊⁻¹ ^ d • (MeasureTheory.Measure.euclideanHausdorffMeasure d) s
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `liminf (c + xᵢ) = c + liminf xᵢ`.  -/
liminf_const_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R),
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f → Filter.liminf (fun i => c + f i) F = c + Filter.liminf f F
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finsetProd' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n (∏ i ∈ t, f i)
-- Aesop.Stats.Report
_private.Aesop.Stats.Report.0.Aesop.StatsReport.scriptsCore.fmtScriptGenerated : Option Aesop.ScriptGenerated → Std.Format
-- Mathlib.Logic.Small.Defs
/-- Due to https://github.com/leanprover/lean4/issues/2297, this is useless as an instance.

See however `Logic.UnivLE`, whose API is able to indirectly provide this instance.  -/
small_max : ∀ (α : Type v), Small.{max w v, v} α
-- Mathlib.Order.Filter.Extr
IsMinOn.max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsMinOn f s a → IsMinOn g s a → IsMinOn (fun x => max (f x) (g x)) s a
-- Mathlib.Geometry.Euclidean.PerpBisector
/-- Perpendicular bisector of a segment in a Euclidean affine space.  -/
AffineSubspace.perpBisector : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → P → P → AffineSubspace ℝ P
-- Mathlib.Order.Interval.Set.Image
StrictMono.mapsTo_Ico : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMono f → Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
-- Mathlib.Analysis.Convex.Hull
convexHull_mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, s ⊆ t → (convexHull 𝕜) s ⊆ (convexHull 𝕜) t
-- Lean.Compiler.LCNF.Types
/-- Whether the type might be an actual pointer (crucially this excludes `tagged`).
 -/
Lean.Compiler.LCNF.ImpureType.Lean.Expr.isPossibleRef : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.instIsLeftDerivabilityStructureIdOfContainsIdentities : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁}
  [W₁.ContainsIdentities], (CategoryTheory.LocalizerMorphism.id W₁).IsLeftDerivabilityStructure
-- Mathlib.RingTheory.Ideal.Colon
/-- **Alias** of `Submodule.iInf_colon_iUnion`. -/
Submodule.iInf_colon_iSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (ι₁ : Sort u_3)
  (f : ι₁ → Submodule R M) (ι₂ : Sort u_4) (g : ι₂ → Set M), (⨅ i, f i).colon (⋃ j, g j) = ⨅ i, ⨅ j, (f i).colon (g j)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.le_of_opNorm₂_le_of_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {x : E} {y : F} {a b c : ℝ},
  ‖f‖ ≤ a → ‖x‖ ≤ b → ‖y‖ ≤ c → ‖(f x) y‖ ≤ a * b * c
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.instStarMemClass : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H],
  StarMemClass (VonNeumannAlgebra H) (H →L[ℂ] H)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition'.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (fb : γ) (h_1 : Unit → motive none) (h_2 : (fb : γ) → motive (some fb)),
  (match some fb with
    | none => h_1 ()
    | some fb => h_2 fb) =
    h_2 fb
-- Mathlib.RingTheory.Support
Module.support_eq_empty_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.support R M = ∅ ↔ Subsingleton M
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorRing.ceil a` computes the least integer `z` such that `a ≤ (z : α)`.  -/
FloorRing.ceil : {α : Type u_4} → {inst : Ring α} → {inst_1 : LinearOrder α} → [self : FloorRing α] → α → ℤ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_inv_comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsMonHom f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f))
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.associated_pow_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {x : R},
  x ≠ 0 → ∀ {ϖ : R}, Irreducible ϖ → ∃ n, Associated x (ϖ ^ n)
-- Mathlib.Order.Filter.Pointwise
Filter.coe_pureMonoidHom : ∀ {α : Type u_2} [inst : MulOneClass α], ⇑Filter.pureMonoidHom = pure
-- Mathlib.Analysis.Normed.Group.Uniform
dist_div_div_le_of_le : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ},
  dist a₁ b₁ ≤ r₁ → dist a₂ b₂ ≤ r₂ → dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.arrowCongr_apply : ∀ {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [inst : Add P] [inst_1 : Add Q] (f : M ≃ N)
  (g : P ≃+ Q) (h : M → P) (n : N), (AddEquiv.arrowCongr f g) h n = g (h (f.symm n))
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
/-- The (pre)image under `inv` of `Ioo a 0` is `Iio a⁻¹`.  -/
Set.inv_Ioo_0_right : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  a < 0 → (Set.Ioo a 0)⁻¹ = Set.Iio a⁻¹
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.isZero.match_1.eq_2 : ∀ (motive : Nat.Internal.Linear.Poly → Sort u_1) (x : Nat.Internal.Linear.Poly) (h_1 : Unit → motive [])
  (h_2 : (x : Nat.Internal.Linear.Poly) → motive x),
  (x = [] → False) →
    (match x with
      | [] => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Init.Grind.Util
Lean.Grind.natCastUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Order.Interval.Basic
Interval.coe_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DecidableLE α] (s t : Interval α), ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.associated_prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] [inst_7 : Invertible 2] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P),
  QuadraticMap.associated (Q₁.prod Q₂) =
    LinearMap.compl₁₂ (QuadraticMap.associated Q₁) (LinearMap.fst R M₁ M₂) (LinearMap.fst R M₁ M₂) +
      LinearMap.compl₁₂ (QuadraticMap.associated Q₂) (LinearMap.snd R M₁ M₂) (LinearMap.snd R M₁ M₂)
-- Mathlib.Algebra.Order.UpperLower
_private.Mathlib.Algebra.Order.UpperLower.0.LowerSet.zero_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s : LowerSet α),
  0 + s = s
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_int16ToInt : ∀ (x : Int16), Int32.ofIntLE x.toInt ⋯ ⋯ = x.toInt32
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_dual_eq : ∀ {α : Type u_1} (I E : Set α), (Matroid.uniqueBaseOn I E)✶ = Matroid.uniqueBaseOn (E \ I) E
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mul_def' : ∀ {R : Type u_3} [inst : CommRing R] {S : Submonoid R} {P : Type u_4} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), I.mul J = ⟨↑I * ↑J, ⋯⟩
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toArray_flatMapM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β},
  (Std.IterM.flatMapM f it₁).toArray =
    Array.flatten <$>
      (Std.IterM.mapM
          (fun b => do
            let __do_lift ← f b
            __do_lift.toArray)
          it₁).toArray
-- Mathlib.Probability.Kernel.Condexp
/-- Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies
`μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω)`.
It is defined as the conditional distribution of the identity given the identity, where the second
identity is understood as a map from `Ω` with the σ-algebra `mΩ` to `Ω` with σ-algebra `m ⊓ mΩ`.
We use `m ⊓ mΩ` instead of `m` to ensure that it is a sub-σ-algebra of `mΩ`. We then use
`Kernel.comap` to get a kernel from `m` to `mΩ` instead of from `m ⊓ mΩ` to `mΩ`.  -/
ProbabilityTheory.condExpKernel : {Ω : Type u_3} →
  [mΩ : MeasurableSpace Ω] →
    [StandardBorelSpace Ω] →
      (μ : MeasureTheory.Measure Ω) →
        [MeasureTheory.IsFiniteMeasure μ] → (m : MeasurableSpace Ω) → ProbabilityTheory.Kernel Ω Ω
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_zipIdx_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β},
  Vector.mapIdx f xs =
    Vector.map
      (fun x =>
        match x with
        | (a, i) => f i a)
      xs.zipIdx
-- Mathlib.Data.Vector.Basic
List.Vector.getElem_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (v : List.Vector α n) (f : α → β) {i : ℕ} (hi : i < n),
  (List.Vector.map f v)[i] = f v[i]
-- Mathlib.Data.ULift
PLift.forall : ∀ {α : Sort u} {p : PLift α → Prop}, (∀ (x : PLift α), p x) ↔ ∀ (x : α), p { down := x }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The configuration state of the TM.  -/
Turing.TM1to1.Λ' : Type u_1 → Type u_2 → Type u_3 → Type (max (max u_1 u_2) u_3)
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.range_inl_eq_ker_rightHom : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  SemidirectProduct.inl.range = SemidirectProduct.rightHom.ker