mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.differentiableOn_arcosh : DifferentiableOn ℝ Real.arcosh (Set.Ioi 1)
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
aeconst_of_dense_setOfPred_preimage_smul_eq : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : SMul M X] [ContinuousSMul M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g • x) ⁻¹' s = s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.card_edgeFinset_sup_edge : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj]
  [inst_2 : Fintype ↑(G ⊔ SimpleGraph.edge s t).edgeSet],
  ¬G.Adj s t → s ≠ t → (G ⊔ SimpleGraph.edge s t).edgeFinset.card = G.edgeFinset.card + 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeansParams.mk.inj : ∀ {uri? : Option Lean.Lsp.DocumentUri} {version? : Option ℕ} {uri?_1 : Option Lean.Lsp.DocumentUri}
  {version?_1 : Option ℕ},
  { uri? := uri?, version? := version? } = { uri? := uri?_1, version? := version?_1 } →
    uri? = uri?_1 ∧ version? = version?_1
-- Init.Data.Array.Count
Array.count_replace : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b c : α} {xs : Array α},
  Array.count c (xs.replace a b) =
    if xs.contains a = true then
      (Array.count c xs + if (b == c) = true then 1 else 0) - if (a == c) = true then 1 else 0
    else Array.count c xs
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.extendRCLikeL_symm_apply : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : StrongDual 𝕜 F), StrongDual.extendRCLikeL.symm f = RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P ≤ CategoryTheory.isCardinalPresentable C κ →
    (∀ (X : C), ∃ J x, ∃ (_ : CategoryTheory.IsCardinalFiltered J κ), P.colimitsOfShape J X) →
      P.IsCardinalFilteredGenerator κ
-- Init.System.IO
/-- The child process's working directory. Inherited from the parent current process if `none`.  -/
IO.Process.SpawnArgs.cwd : IO.Process.SpawnArgs → Option System.FilePath
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.inverse.obj A).obj x = A.X
-- Init.Data.Int.Order
Int.pos_of_mul_pos_right : ∀ {a b : ℤ}, 0 < a * b → 0 < a → 0 < b
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
PartialEquiv.IsImage.restr.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {e e_1 : PartialEquiv α β} (e_e : e = e_1) {s s_1 : Set α} (e_s : s = s_1)
  {t t_1 : Set β} (e_t : t = t_1) (h : e.IsImage s t), h.restr = ⋯.restr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on `s` and `f 0 = 0` and `a : X → A` is continuous on `t : Set X`,
and `a x` satisfies the predicate `p` associated to `𝕜` and `s` is a common neighborhood of the
quasispectra of `a x` for all `x ∈ t`, then `fun x ↦ cfcₙ f (a x)` is continuous on `t`.

This is weaker than `ContinuousOn.cfcₙ` since it requires `f` to be continuous on a
*neighborhood* of the quasispectra, but in practice it is often easier to apply because `s` is not
required to be compact, nor does it require an indexed family of compact sets. This is proven using
`ContinuousOn.cfcₙ` and `upperHemicontinuous_quasispectrum` to produce the necessary family of
compact sets.  -/
ContinuousOn.cfcₙ_of_mem_nhdsSet : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [ContinuousStar A] [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A]
  [inst_9 : TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
  s ∈ nhdsSet (⋃ x ∈ t, quasispectrum 𝕜 (a x)) →
    ContinuousOn a t →
      autoParam (∀ x ∈ t, p (a x)) ContinuousOn.cfcₙ_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) ContinuousOn.cfcₙ_of_mem_nhdsSet._auto_3 →
          autoParam (f 0 = 0) ContinuousOn.cfcₙ_of_mem_nhdsSet._auto_5 → ContinuousOn (fun x => cfcₙ f (a x)) t
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_vadd_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P} {v : V}, v ∈ s.direction → (s.WOppSide (v +ᵥ x) y ↔ s.WOppSide x y)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_eq_of_norm_add_lt_right : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]}, ‖z1 + z2‖ < ‖z2‖ → ‖z1‖ = ‖z2‖
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurableSet_interior : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α],
  MeasurableSet (interior s)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.le_multiplicity_of_pow_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → ∀ {k : ℕ}, a ^ k ∣ b → k ≤ multiplicity a b
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.IsThreeCycle → σ.cycleType = {3}
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y} (hc : CategoryTheory.Limits.IsColimit c)
  {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀ {j₀ : J} (y : X ⟶ Y.obj j₀),
      CategoryTheory.CategoryStruct.comp y (c.ι.app j₀) = 0 → ∃ j φ, CategoryTheory.CategoryStruct.comp y (Y.map φ) = 0
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_alterₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)}, Std.DHashMap.Internal.Raw.WFImp ↑(m.alterₘ a f)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.nrComplexPlaces.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.InfinitePlace.nrComplexPlaces K = NumberField.InfinitePlace.nrComplexPlaces K
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonAssocRingQuotient : {R : Type u_1} → [inst : NonAssocRing R] → (c : RingCon R) → NonAssocRing c.Quotient
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance
`< r` of a point in the other set.  -/
Metric.exists_dist_lt_of_hausdorffDist_lt' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {y : α} {r : ℝ},
  y ∈ t → Metric.hausdorffDist s t < r → Metric.hausdorffEDist s t ≠ ⊤ → ∃ x ∈ s, dist x y < r
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An invariant block of a group action is a fixed block.  -/
MulAction.IsInvariantBlock.isFixedBlock : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsInvariantBlock G B → MulAction.IsFixedBlock G B
-- Init.Data.SInt.Lemmas
Int8.toNat_toBitVec_of_le : ∀ {x : Int8}, 0 ≤ x → x.toBitVec.toNat = x.toNatClampNeg
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- Uses `xa` to compute the fold across the arguments of an application,
where `xf` provides the initial value and is evaluated in the context of the head of the application.
 -/
Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs : {α : Type} →
  {m : Type → Type} →
    [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → (α → m α) → m α
-- Mathlib.Analysis.Convex.Cone.Closure
/-- The closure of a convex cone inside a topological space as a convex cone. This
construction is mainly used for defining maps between proper cones.  -/
ConvexCone.closure : {𝕜 : Type u_1} →
  [inst : Semiring 𝕜] →
    [inst_1 : PartialOrder 𝕜] →
      {E : Type u_2} →
        [inst_2 : AddCommMonoid E] →
          [inst_3 : TopologicalSpace E] →
            [ContinuousAdd E] → [inst_5 : SMul 𝕜 E] → [ContinuousConstSMul 𝕜 E] → ConvexCone 𝕜 E → ConvexCone 𝕜 E
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
/-- A constructor for `W.FunctorsInverting D`  -/
CategoryTheory.MorphismProperty.FunctorsInverting.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          (F : CategoryTheory.Functor C D) → W.IsInvertedBy F → W.FunctorsInverting D
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.subset_zero_iff : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, s.Nonempty → (s ⊆ 0 ↔ s = 0)
-- Mathlib.Data.Sym.Sym2
/-- The set of all `Sym2 α` elements on the diagonal.  -/
Sym2.diagSet : {α : Type u_1} → Set (Sym2 α)
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.mk : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
  K.Nonempty →
    (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) →
      (Quotient.mk' '' K).Countable →
        FirstOrder.Language.Hereditary K →
          FirstOrder.Language.JointEmbedding K → FirstOrder.Language.Amalgamation K → FirstOrder.Language.IsFraisse K
-- Mathlib.Algebra.Star.StarAlgHom
/-- Reintrepret a star algebra equivalence as a star algebra homomorphism.  -/
StarAlgEquiv.toStarAlgHom : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] → [inst_5 : Star A₁] → [inst_6 : Star A₂] → (A₁ ≃⋆ₐ[R] A₂) → A₁ →⋆ₐ[R] A₂
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.step_dropWhileM : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] {it : Std.IterM m β} {P : β → m (ULift.{u_1, 0} Bool)},
  (Std.IterM.dropWhileM P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← MonadAttach.attach (P out)
        match __do_lift with
          | ⟨{ down := true }, hP⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileM P true it') ⋯))
          | ⟨{ down := false }, hP⟩ =>
            pure
              (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileM P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileM P true it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit},
  t₁.WF → t₂.WF → (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁.Equiv t₂
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- This structure encodes the data required for a morphism to be an effective epimorphism.
 -/
CategoryTheory.EffectiveEpiStruct : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : C} → (Y ⟶ X) → Type (max u_1 v_1)
-- Mathlib.Topology.Category.Profinite.Extend
/-- An abbreviation for `S.fintypeDiagram' ⋙ toProfinite`.  -/
Profinite.diagram' : (S : Profinite) → CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toProfinite) Profinite
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- A finite-product-preserving functor between Cartesian monoidal categories is monoidal.

This is not made an instance because it would create a diamond for the monoidal structure on
the identity and composition of functors.  -/
CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) → [CategoryTheory.Limits.PreservesFiniteProducts F] → F.Monoidal
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.iInf : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : ConditionallyCompleteLattice M] {ι : Sort u_3} [Nonempty ι]
  [Finite ι] {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteMulSupport (f i)) → Function.HasFiniteMulSupport fun a => ⨅ i, f i a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.lift.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {γ : Sort w} (f f_1 : Std.DTreeMap α β cmp → γ) (e_f : f = f_1)
  (h : ∀ (a b : Std.DTreeMap α β cmp), a.Equiv b → f a = f b) (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → Std.ExtDTreeMap.lift f h t = Std.ExtDTreeMap.lift f_1 ⋯ t_1
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.equiv_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) (n : ℕ) (b : B),
  ((DividedPowers.equiv h) hI).dpow n b = e (hI.dpow n (e.symm b))
-- Mathlib.CategoryTheory.Grothendieck
/-- Taking the Grothendieck construction on `F ⋙ asSmallFunctor`, where
`asSmallFunctor : Cat ⥤ Cat` is the functor which turns each category into a small category of a
(potentially) larger universe, is equivalent to the Grothendieck construction on `F` itself.  -/
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) →
      CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor) ≌ CategoryTheory.Grothendieck F
-- Std.Do.Triple.SpecLemmas
/-- Returns the element at the current cursor position.

Requires that is a current element: the suffix must be non-empty, so the cursor is not at the end of
the list.
 -/
List.Cursor.current : {α : Type u_1} → {l : List α} → (c : l.Cursor) → autoParam (0 < c.suffix.length) List.Cursor.current._auto_1 → α
-- Mathlib.Logic.IsEmpty.Basic
Function.Surjective.of_isEmpty : ∀ {α : Type u_4} {β : Type u_5} [IsEmpty β] (f : α → β), Function.Surjective f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Execution semantics of the Turing machine.  -/
Turing.TM0.step : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Λ] →
      [inst_1 : Inhabited Γ] → Turing.TM0.Machine Γ Λ → Turing.TM0.Cfg Γ Λ → Option (Turing.TM0.Cfg Γ Λ)
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.instLawfulEqOrd : ∀ {rel : ℤ → ℤ → Prop} {n m : ℤ}, Std.LawfulEqOrd (Std.Time.Internal.Bounded rel n m)
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_inter : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω},
  s.Finite →
    (ProbabilityTheory.uniformOn s) (t ∩ u) =
      (ProbabilityTheory.uniformOn (s ∩ t)) u * (ProbabilityTheory.uniformOn s) t
-- Mathlib.Topology.Order
isClosed_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] (s : Set α), IsClosed s
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Structure witnessing that a bicone is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.Bicone.IsBilimit.isLimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → {B : CategoryTheory.Limits.Bicone F} → B.IsBilimit → CategoryTheory.Limits.IsLimit B.toCone
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddCommMonoid (f i)],
  Pi.addCommMonoid = { toAddMonoid := Pi.addMonoid, add_comm := ⋯ }
-- Mathlib.Data.Fin.SuccPred
Fin.le_castSucc_pred_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0), b ≤ (a.pred ha).castSucc ↔ b < a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v : β},
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l → Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.insertMany t l) k' = some v
-- Mathlib.Order.DirSupClosed
DirSupInacc.sUnion : ∀ {α : Type u_1} [inst : Preorder α] {s : Set (Set α)}, (∀ x ∈ s, DirSupInacc x) → DirSupInacc (⋃₀ s)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go : (pat : ByteArray) → (stackPos : ℕ) → stackPos < pat.size → ℕ → ℕ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_top : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_rightUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) (c : γ) (s : Set β),
  ((κ.comap g hg) c) s = (κ (g c)) s
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonUnitalRing : {R : Type u_1} → [NonUnitalRing R] → NonUnitalRing Rᵃᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C}
  (h : V₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
        h)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts** (vector-valued).  -/
intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right : ∀ {a b : ℝ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [CompleteSpace E]
  [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x
-- Mathlib.RingTheory.Ideal.Maps
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`,
then `comap f (comap f.symm I) = I`.  -/
Ideal.comap_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} (f : R ≃+* S),
  Ideal.comap (↑f) (Ideal.comap (↑f.symm) I) = I
-- Mathlib.Order.Defs.Unbundled
rel_of_subsingleton : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Refl r] [Subsingleton α] (x y : α), r x y
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq)).comp
      (CochainComplex.mappingCone.snd φ) ⋯ =
    β
-- Mathlib.Algebra.Module.LinearMap.End
/-- Linear endomorphisms of a module, with associated ring structure
`Module.End.semiring` and algebra structure `Module.End.algebra`.  -/
Module.End : (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type v
-- Mathlib.Algebra.Star.CentroidHom
/-- Let `α` be a star ring with commutative centroid. Then the centroid is a star ring.
 -/
CentroidHom.starRingOfCommCentroidHom : {α : Type u_1} →
  [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → IsMulCommutative (CentroidHom α) → StarRing (CentroidHom α)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainAddEquiv_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (e : M ≃ N) (r : R)
  (m : M), (MonoidAlgebra.mapDomainAddEquiv R e) (MonoidAlgebra.single m r) = MonoidAlgebra.single (e m) r
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.alter.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (f : Option (β a) → Option (β a))
  (a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.alter a f (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if h : (a_1 == a) = true then
      have h' := ⋯;
      match f (some (cast ⋯ b)) with
      | none => es
      | some b => Std.DHashMap.Internal.AssocList.cons a b es
    else
      have tail := Std.DHashMap.Internal.AssocList.alter a f es;
      Std.DHashMap.Internal.AssocList.cons a_1 b tail
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_iSizeToInt : ∀ (x : ISize), Int64.ofIntLE x.toInt ⋯ ⋯ = x.toInt64