mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $(a, ∞)$ of elements `x` such that `a < x`. Basically `Set.Ioi a` as a finset.  -/
Finset.Ioi : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → α → Finset α
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_two : ∀ {R : Type u_1} [inst : NatCast R], ↑2 = 2
-- Mathlib.Topology.Order.OrderClosed
closure_le_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α}, Continuous f → Continuous g → closure {b | f b ≤ g b} = {b | f b ≤ g b}
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- The `setToFun` operation is measurable. This shows that the integrand of (the right-hand-side
of) Fubini's theorem is measurable. This version has `f` in curried form.  -/
MeasureTheory.StronglyMeasurable.setToFun_prod_right : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {β : Type u_7} {mβ : MeasurableSpace β} [MeasureTheory.SFinite μ]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set (β × α)), MeasurableSet s → MeasureTheory.StronglyMeasurable fun x => T (Prod.mk x ⁻¹' s)) →
    ∀ ⦃f : β → α → E⦄,
      MeasureTheory.StronglyMeasurable (Function.uncurry f) →
        MeasureTheory.StronglyMeasurable fun x => MeasureTheory.setToFun μ T hT (f x)
-- Init.Data.SInt.Basic
instMinInt32 : Min Int32
-- Mathlib.Topology.Order.AtTopBotIxx
comap_coe_nhdsGT_eq_atBot_iff : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  Filter.comap Subtype.val (nhdsWithin b (Set.Ioi b)) = Filter.atBot ↔
    s ⊆ Set.Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Set.Ioo b a).Nonempty)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `(F ⨯ G).obj a` is in bijection with the product of `F.obj a` and `G.obj a`.  -/
CategoryTheory.FunctorToTypes.binaryProductEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → (a : C) → (F ⨯ G).obj a ≃ F.obj a × G.obj a
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Note: the priority is set to 90 to ensure that this instance is only applied after
`EMetricSpace.metrizableSpace`. This prevents unnecessary attempts to infer completeness.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X],
  TopologicalSpace.MetrizableSpace X
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_concat_of_startsWithVar : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) [inst₁ : Std.Associative ctx.op] [inst₂ : Std.IdempotentOp ctx.op]
  (s : Lean.Grind.AC.Seq) (x : Lean.Grind.AC.Var),
  s.startsWithVar_k x = true →
    Lean.Grind.AC.Seq.denote ctx ((Lean.Grind.AC.Seq.var x).concat_k s) = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Order.Filter.IsBounded
/-- A filter which is eventually bounded is in particular frequently bounded (in the opposite
direction). At least if the filter is not trivial.  -/
Filter.IsBounded.isCobounded_flip : ∀ {α : Type u_1} {r : α → α → Prop} {f : Filter α} [IsTrans α r] [f.NeBot],
  Filter.IsBounded r f → Filter.IsCobounded (flip r) f
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.true_imp : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, (⌜True⌝ → P) ⊣⊢ₛ P
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.isAtomistic_of_sSup_eq_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → IsAtomistic α
-- Mathlib.Tactic.Simproc.VecPerm
/-- Given an expression representing a vector `perm : Fin n → Fin n`, computes the corresponding
list of term of type `Fin n`. This is meant to be used when `perm` corresponds to a permutation
of `Fin n`, e.g. `perm = Equiv.swap 0 1`, etc.  -/
_private.Mathlib.Tactic.Simproc.VecPerm.0.Mathlib.Tactic.FinVec.arrayOfVecFinQ : (n : Q(ℕ)) → ℕ → Q(Fin «$n» → Fin «$n») → Lean.Meta.SimpM (Option (Array ℕ))
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
/-- A functor `F : C ⥤ H` has a pointwise right derived functor with respect to
`W : MorphismProperty C` if it has a pointwise right derived functor at `X`
for any `X : C`.  -/
CategoryTheory.Functor.HasPointwiseRightDerivedFunctor : {C : Type u₁} →
  {H : Type u₃} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.ghostComponent_verschiebungFun : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  (WittVector.ghostComponent (n + 1)) x.verschiebungFun = ↑p * (WittVector.ghostComponent n) x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfc_nnreal_eq_real : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [IsSemitopologicalRing A] [T2Space A]
  [inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (f : NNReal → NNReal)
  (a : A), autoParam (0 ≤ a) cfc_nnreal_eq_real._auto_1 → cfc f a = cfc (fun x => ↑(f x.toNNReal)) a
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- When `M` is `I`-adic complete, the canonical map from `M` to its `I`-adic completion is a linear
equivalence.
 -/
AdicCompletion.ofLinearEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [IsAdicComplete I M] → M ≃ₗ[R] AdicCompletion I M
-- Lean.Meta.CollectMVars
/-- Collect the metavariables appearing in the expression `e`,
including metavariables in the type or local context of any such metavariables, etc.  -/
Lean.Expr.getMVarDependencies : Lean.Expr → optParam Bool false → Lean.MetaM (Std.HashSet Lean.MVarId)
-- Std.Async.UDP
Std.Async.UDP.Membership.leaveGroup.sizeOf_spec : sizeOf Std.Async.UDP.Membership.leaveGroup = 1
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_forget_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂),
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget D)) ↔
    CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddHom.pi_injective`. -/
Pi.addHom_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {γ : Type w} [Nonempty I] [inst_2 : Add γ]
  (g : (i : I) → γ →ₙ+ f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddHom.pi g)
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_pi : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_5} {M : ι → Type u_6} [Finite ι]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] {p : (i : ι) → Submodule R (M i)},
  (∀ (i : ι), (p i).FG) → (Submodule.pi Set.univ p).FG
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are collinear if and only if they are not affinely independent.  -/
collinear_iff_not_affineIndependent_set : ∀ {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] {p₁ p₂ p₃ : P}, Collinear k {p₁, p₂, p₃} ↔ ¬AffineIndependent k ![p₁, p₂, p₃]
-- Plausible.Arbitrary
Plausible.BitVec.Arbitrary : {n : ℕ} → Plausible.Arbitrary (BitVec n)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOps.mk.sizeOf_spec : ∀ (mkPureApp : Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (mkBindApp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr)
  (isPureApp? : Lean.Expr → Option Lean.Expr)
  (splitMonadApp? : Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr)))
  (mkMonadApp : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr),
  sizeOf
      { mkPureApp := mkPureApp, mkBindApp := mkBindApp, isPureApp? := isPureApp?, splitMonadApp? := splitMonadApp?,
        mkMonadApp := mkMonadApp } =
    1
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- The map makes the triangle with the two natural transformations commute  -/
CategoryTheory.Limits.IsWeakLimit.fac_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (self : CategoryTheory.Limits.IsWeakLimit t) (s : CategoryTheory.Limits.Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.lift s) (CategoryTheory.CategoryStruct.comp (t.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (s.π.app j) h
-- Mathlib.Data.Num.Basic
PosNum.instLE : LE PosNum
-- Mathlib.Topology.Bornology.Constructions
/-- **Alias** of the reverse direction of `boundedSpace_subtype_iff`. -/
Bornology.IsBounded.boundedSpace_subtype : ∀ {α : Type u_1} [inst : Bornology α] {p : α → Prop}, Bornology.IsBounded {x | p x} → BoundedSpace (Subtype p)
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (r : α → β → Prop) (s : Set α) (x : α),
  SemicontinuousWithinAt r s x = ∀ (y : β), r x y → ∀ᶠ (x' : α) in nhdsWithin x s, r x' y
-- Init.Data.Order.Ord
Std.OrientedCmp.isGE_iff_isLE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp a b).isGE = true ↔ (cmp b a).isLE = true
-- Lean.MetavarContext
Lean.setMCtx : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MetavarContext → m Unit
-- Init.Data.SInt.Lemmas
Int8.lt_of_le_of_lt : ∀ {a b c : Int8}, a ≤ b → b < c → a < c
-- Mathlib.Topology.Clopen
Topology.IsQuotientMap.isClopen_preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsQuotientMap f → ∀ {s : Set Y}, IsClopen (f ⁻¹' s) ↔ IsClopen s
-- Std.Sat.AIG.Basic
/-- A `RefVec` bundled with a `RefVec` as distance to be shifted by.
 -/
Std.Sat.AIG.ArbitraryShiftTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Analysis.CStarAlgebra.Fuglede
_private.Mathlib.Analysis.CStarAlgebra.Fuglede.0.expMulMulExp_eq_expUnitary_mul_mul_expUnitary : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a b x : A} [IsStarNormal a] [IsStarNormal b],
  SemiconjBy x a b →
    ∀ (z : ℂ),
      expMulMulExp✝ a b x z =
        ↑(selfAdjoint.expUnitary (2 • imaginaryPart (z • star b))) * x *
          ↑(selfAdjoint.expUnitary (2 • imaginaryPart (star z • a)))
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- An affine combination of two `C^k` connections is a `C^k` connection.  -/
CovariantDerivative.ContMDiffCovariantDerivative.affineCombination : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] (cov cov' : CovariantDerivative I F V) {f : M → 𝕜} {n : WithTop ℕ∞},
  ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n f →
    cov.ContMDiffCovariantDerivative n →
      cov'.ContMDiffCovariantDerivative n → (cov.affineCombination cov' f).ContMDiffCovariantDerivative n
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_const : ∀ {α : Type u_1} {ι : Sort u_5} [Nonempty ι] {f : ι → Set α} {s : Set α}, (∀ (i : ι), f i = s) → ⋃ i, f i = s
-- Mathlib.Condensed.Explicit
/-- A condensed object preserves finite products.  -/
Condensed.instPreservesFiniteProductsOppositeCompHausObjFunctorIsSheafCoherentTopology : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (X : Condensed A),
  CategoryTheory.Limits.PreservesFiniteProducts X.obj
-- Init.Data.Iterators.Basic
Std.Shrink.inflate_deflate : ∀ {α : Type u_1} {x : α}, (Std.Shrink.deflate x).inflate = x
-- Mathlib.Order.Completion
/-- The right set of a Dedekind cut. This is an alias for `Concept.intent`.  -/
DedekindCut.right : {α : Type u_1} → [inst : Preorder α] → DedekindCut α → Set α
-- Mathlib.Topology.ClusterPt
isClosed_iff_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s ↔ ∀ (x : X), (∀ U ∈ nhds x, (U ∩ s).Nonempty) → x ∈ s
-- Mathlib.Order.FixedPoints
OrderHom.prevFixed_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x), ↑(f.prevFixed x hx) ≤ x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_2 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (val : BitVec w)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.const val with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_2 w val
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.comp : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N]
  [inst_5 : Convexity.ConvexSpace R P] {g : N → P},
  Convexity.IsAffineMap R g → ∀ {f : M → N}, Convexity.IsAffineMap R f → Convexity.IsAffineMap R (g ∘ f)
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeffOn.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a a_1 : ℝ} (e_a : a = a_1) {b b_1 : ℝ}
  (e_b : b = b_1) (hab : a < b) (f f_1 : ℝ → E),
  f = f_1 → ∀ (n n_1 : ℤ), n = n_1 → fourierCoeffOn hab f n = fourierCoeffOn ⋯ f_1 n_1
-- Init.Data.UInt.Lemmas
UInt64.le_iff_toBitVec_le : ∀ {a b : UInt64}, a ≤ b ↔ a.toBitVec ≤ b.toBitVec
-- Batteries.Classes.Order
Std.LawfulLECmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α] [inst_3 : LE α],
  (∀ (x : α), ¬x < x) →
    (∀ {x y z : α}, x < y → y < z → x < z) →
      (∀ {x y : α}, ¬x < y ↔ y ≤ x) →
        (∀ {x y : α}, x ≤ y → y ≤ x → x = y) → Std.LawfulLECmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.card_nonuniformWitness_sdiff_biUnion_star : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {V : Finset α},
  V ∈ P.parts →
    U ≠ V →
      ¬G.IsUniform ε U V →
        (G.nonuniformWitness ε U V \ (SzemerediRegularity.star hP G ε hU V).biUnion id).card ≤
          2 ^ (P.parts.card - 1) * (Fintype.card α / SzemerediRegularity.stepBound P.parts.card)
-- Lean.Util.PPExt
Lean.pp.raw : Lean.Option Bool
-- Batteries.Data.Fin.Fold
Fin.dfoldlM.eq_1 : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (n : ℕ) (α : Fin (n + 1) → Type u_1)
  (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (init : α 0), Fin.dfoldlM n α f init = Fin.dfoldlM.loop n α f 0 ⋯ init
-- Mathlib.Data.ENNReal.Action
ENNReal.instIsScalarTowerNNReal : ∀ {M : Type u_1} {N : Type u_2} [inst : MulAction ENNReal M] [inst_1 : MulAction ENNReal N] [inst_2 : SMul M N]
  [IsScalarTower ENNReal M N], IsScalarTower NNReal M N
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- If a function is `C^k` on open sets `s i`, it is `C^k` on their union  -/
ContMDiffOn.iUnion_of_isOpen : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {n : WithTop ℕ∞} {ι : Type u_11} {s : ι → Set M},
  (∀ (i : ι), ContMDiffOn I I' n f (s i)) → (∀ (i : ι), IsOpen (s i)) → ContMDiffOn I I' n f (⋃ i, s i)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryₘ_eq_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} (h : Std.Internal.List.containsKey k t.toListModel = true)
  {h' : (t.getEntry?ₘ k).isSome = true}, t.Ordered → t.getEntryₘ k h' = Std.Internal.List.getEntry k t.toListModel h
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_lt_top_iff_isBoundedUnder : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F},
  MeasureTheory.eLpNormEssSup f μ < ⊤ ↔
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) fun x => ‖f x‖₊
-- Init.Data.SInt.Basic
/-- The power operation, raising a word-sized signed integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
ISize.pow : ISize → ℕ → ISize
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.measure_univ : ∀ (T : ℝ) [hT : Fact (0 < T)], MeasureTheory.volume Set.univ = ENNReal.ofReal T
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.strictMonoOn_log : StrictMonoOn Real.log (Set.Ioi 0)
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceFoldingRangeParams : Lean.Lsp.FileSource Lean.Lsp.FoldingRangeParams
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.Options.mk.sizeOf_spec : ∀ (overwrite ignoreIfExists : Bool),
  sizeOf { overwrite := overwrite, ignoreIfExists := ignoreIfExists } = 1 + sizeOf overwrite + sizeOf ignoreIfExists
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + t/x) ^ x` as `x → ∞` is `exp t` for `t : ℝ`.  -/
Real.tendsto_one_add_div_rpow_exp : ∀ (t : ℝ), Filter.Tendsto (fun x => (1 + t / x) ^ x) Filter.atTop (nhds (Real.exp t))
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsCoinducing.connectedComponentsHomeomorph_mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsCoinducing f) (hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})) (x : X),
  (hf.connectedComponentsHomeomorph hf') (ConnectedComponents.mk x) = ConnectedComponents.mk (f x)
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Integrating `f` against `partialTraj κ a b` and then against `partialTraj κ b c` is the same
as integrating `f` against `partialTraj κ a c`.  -/
ProbabilityTheory.Kernel.lmarginalPartialTraj_self : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b c : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))},
  a ≤ b →
    b ≤ c →
      ∀ {f : ((n : ℕ) → X n) → ENNReal},
        Measurable f →
          ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b (ProbabilityTheory.Kernel.lmarginalPartialTraj κ b c f) =
            ProbabilityTheory.Kernel.lmarginalPartialTraj κ a c f
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.coe_directSumRight : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_2) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'],
  ⇑(TensorProduct.directSumRight R S M₁' M₂) = ⇑(TensorProduct.directSumRight R R M₁' M₂)
-- Mathlib.Algebra.Homology.DerivedCategory.KProjective
/-- When `K` is a K-projective cochain complex, cohomology classes
in `CohomologyClass K L n` identify to elements in a type `SmallShiftedHom` relatively
to quasi-isomorphisms.  -/
CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          [inst_2 :
              CategoryTheory.Localization.HasSmallLocalizedShiftedHom
                (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] →
            [K.IsKProjective] →
              CochainComplex.HomComplex.CohomologyClass K L n ≃
                CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.JordanDecomposition.mk.congr_simp : ∀ {α : Type u_2} [inst : MeasurableSpace α] (posPart posPart_1 : MeasureTheory.Measure α)
  (e_posPart : posPart = posPart_1) (negPart negPart_1 : MeasureTheory.Measure α) (e_negPart : negPart = negPart_1)
  [posPart_finite : MeasureTheory.IsFiniteMeasure posPart] [negPart_finite : MeasureTheory.IsFiniteMeasure negPart]
  (mutuallySingular : posPart.MutuallySingular negPart),
  { posPart := posPart, negPart := negPart, posPart_finite := posPart_finite, negPart_finite := negPart_finite,
      mutuallySingular := mutuallySingular } =
    { posPart := posPart_1, negPart := negPart_1, posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }