mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The relation on a type `X` coming from a pair of maps `R ⟶ X`.  -/
TypeCat.Rel.ofPair : {X R : Type w} → (R ⟶ X) → (R ⟶ X) → X → X → Prop
-- Mathlib.Algebra.Order.Floor.Ring
Int.le_floor_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a b : R),
  ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {km : α}, Std.Internal.List.maxKey? l = some km → Std.Internal.List.containsKey km l = true
-- Lean.Language.Basic
Lean.Language.SnapshotBundle.mk : {α : Type} →
  Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α)) → IO.Promise α → Lean.Language.SnapshotBundle α
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.homMk_eq_comp_iff : ∀ {X Y Z : FintypeCat} (f : X.obj → Y.obj) (g : Y.obj → Z.obj) (h : X.obj → Z.obj),
  FintypeCat.homMk h = CategoryTheory.CategoryStruct.comp (FintypeCat.homMk f) (FintypeCat.homMk g) ↔ h = g ∘ f
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Productive.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it it_1 : Std.IterM m β),
  ({ it := it } = { it := it_1 }) = (it = it_1)
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms an element of `SizedBalancedTree` into a `BalancedTree`.  -/
Std.DTreeMap.Internal.Impl.SizedBalancedTree.toBalancedTree : {α : Type u} →
  {β : α → Type v} →
    {lb ub : ℕ} → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub → Std.DTreeMap.Internal.Impl.BalancedTree α β
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.sup_toSubalgebra_of_isAlgebraic_left : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (E1 E2 : IntermediateField K L) [Algebra.IsAlgebraic K ↥E1],
  (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- Additive congruence relations preserve sum indexed by a list.  -/
AddCon.list_sum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (c : AddCon M) {l : List ι} {f g : ι → M},
  (∀ x ∈ l, c (f x) (g x)) → c (List.map f l).sum (List.map g l).sum
-- Init.Data.List.Lemmas
List.nil_eq_flatten_iff : ∀ {α : Type u_1} {L : List (List α)}, [] = L.flatten ↔ ∀ l ∈ L, l = []
-- Mathlib.Analysis.Calculus.Deriv.Pow
derivWithin_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x → ∀ (n : ℕ), derivWithin (f ^ n) s x = ↑n * f x ^ (n - 1) * derivWithin f s x
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.mk_set_nat : Cardinal.mk (Set ℕ) = Cardinal.continuum
-- Std.Time.Format.Modifier
/-- 06:00–12:00
 -/
Std.Time.ExtendedDayPeriod.morning : Std.Time.ExtendedDayPeriod
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_fun_finsetSum : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {ι : Type u_6} (s : Finset ι) (f : ι → ↥(MeasureTheory.Lp E p μ)),
  ↑↑(∑ i ∈ s, f i) =ᵐ[μ] fun x => ∑ i ∈ s, ↑↑(f i) x
-- ProofWidgets.Component.RefreshComponent
/-- Create a `RefreshComponent` instance together with a token to manage it.  -/
ProofWidgets.mkRefreshComponent : optParam ProofWidgets.Html (ProofWidgets.Html.text "") → BaseIO (ProofWidgets.Html × ProofWidgets.RefreshToken)
-- Mathlib.NumberTheory.GaussSum
/-- When `F` and `F'` are finite fields and `χ : F → F'` is a nontrivial quadratic character,
then `(χ(-1) * #F)^(#F'/2) = χ #F'`.  -/
Char.card_pow_card : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] {F' : Type u_2} [inst_2 : Field F'] [inst_3 : Fintype F']
  {χ : MulChar F F'},
  χ ≠ 1 →
    χ.IsQuadratic →
      ringChar F' ≠ ringChar F →
        ringChar F' ≠ 2 → (χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ Std.DHashMap.Const.ofList l ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  [inst_3 : L.IsLocalization W] [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX eX_1 : L.obj X ≅ X'),
  eX = eX_1 →
    ∀ (eY eY_1 : L.obj Y ≅ Y'),
      eY = eY_1 →
        ∀ (f₁ f₁_1 : X' ⟶ Y'),
          f₁ = f₁_1 →
            ∀ (f₂ f₂_1 : X' ⟶ Y'),
              f₂ = f₂_1 →
                CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂ =
                  CategoryTheory.Localization.Preadditive.add W_1 eX_1 eY_1 f₁_1 f₂_1
-- Init.Data.BitVec.Bitblast
BitVec.getElem_neg : ∀ {w i : ℕ} {x : BitVec w} (h : i < w), (-x)[i] = (x[i] ^^ decide (∃ j < i, x.getLsbD j = true))
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.image_of_comp : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : ι → ι') (g : ι' → M), LinearIndepOn R (g ∘ f) s → LinearIndepOn R g (f '' s)
-- Lean.Elab.PreDefinition.Basic
/-- Adds constant info to the definition name. This should occur after executing post-compilation
attributes, in case they have an effect on hovers.
 -/
Lean.Elab.addPreDefInfo : Lean.Elab.PreDefinition → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Show that the extension of `f : S.functor ⟶ P` to all of `yoneda.obj X` is in fact an extension,
i.e. that the triangle below commutes, provided `P` is a sheaf for `S`
```
      f
   S  →  P
   ↓  ↗
   yX
```
 -/
CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) (f : S.functor ⟶ P),
  CategoryTheory.CategoryStruct.comp S.functorInclusion (h.extend f) = f
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.map.congr_simp : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  (x x_1 : HahnSeries Γ R),
  x = x_1 →
    ∀ {F : Type u_5} [inst_3 : FunLike F R S] [inst_4 : ZeroHomClass F R S] (f f_1 : F), f = f_1 → x.map f = x_1.map f_1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.hasOfPrecompProperty_epimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange], P.HasOfPrecompProperty (CategoryTheory.MorphismProperty.epimorphisms C)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.symm_bijective : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X},
  Function.Bijective ContinuousMap.HomotopyRel.symm
-- Init.Data.SInt.Lemmas
Int32.ofNat_add : ∀ (a b : ℕ), Int32.ofNat (a + b) = Int32.ofNat a + Int32.ofNat b
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- An integral domain is a Dedekind domain if and only if it is
Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.
In particular, this definition does not depend on the choice of this fraction field.  -/
isDedekindRing_iff : ∀ (A : Type u_2) [inst : CommRing A] (K : Type u_4) [inst_1 : CommRing K] [inst_2 : Algebra A K] [IsFractionRing A K],
  IsDedekindRing A ↔
    IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.instGroupWithZeroSubtypeMemSubmonoidMrange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : GroupWithZero G] → [inst_1 : GroupWithZero H] → (f : G →*₀ H) → GroupWithZero ↥(MonoidHom.mrange f)
-- Mathlib.Data.Complex.Basic
/-- The equivalence between the complex numbers and `ℝ × ℝ`.  -/
Complex.equivRealProd : ℂ ≃ ℝ × ℝ
-- Lean.EnvExtension
/-- Environment extension for tagging declarations.
Declarations must only be tagged in the module where they were declared.  -/
Lean.TagDeclarationExtension : Type
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.mk'_mem_maximal_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (x : R) (y : ↥I.primeCompl) (h : optParam (IsLocalRing S) ⋯),
  IsLocalization.mk' S x y ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I
-- Mathlib.Analysis.Convex.Segment
openSegment_subset_segment : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E), openSegment 𝕜 x y ⊆ segment 𝕜 x y
-- Mathlib.Analysis.Normed.Ring.Units
/-- In a normed ring with summable geometric series, the coercion from `Rˣ` (equipped with the
induced topology from the embedding in `R × R`) to `R` is an open embedding.  -/
Units.isOpenEmbedding_val : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], Topology.IsOpenEmbedding Units.val
-- Mathlib.Algebra.Star.TransferInstance
/-- Transfer `StarRing` across an `Equiv`. See note [reducible non-instances].  -/
Equiv.starRing : {R : Type u_1} → {S : Type u_2} → (e : R ≃ S) → [inst : NonUnitalNonAssocSemiring S] → [StarRing S] → StarRing R
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x ⤳ y),
  AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) X
-- Mathlib.RingTheory.Smooth.Kaehler
Algebra.Extension.infinitesimal.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  P.infinitesimal =
    { Ring := P.Ring ⧸ P.ker ^ 2, commRing := Ideal.Quotient.commRing (P.ker ^ 2),
      algebra₁ := Ideal.instAlgebraQuotient R (P.ker ^ 2), algebra₂ := Ideal.Algebra.kerSquareLift, isScalarTower := ⋯,
      σ := ⇑(Ideal.Quotient.mk (P.ker ^ 2)) ∘ P.σ, algebraMap_σ := ⋯ }
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.parenthesizeTerm : Lean.Syntax → Lean.CoreM Lean.Syntax
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.ofReal_rpow_of_pos : ∀ {x p : ℝ}, 0 < x → ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
-- Lean.Parser.Basic
Lean.Parser.suppressInsideQuot : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.equivalence : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X}, Equivalence Path.Homotopic
-- Mathlib.Order.SuccPred.Basic
/-- Predecessor function  -/
PredOrder.pred : {α : Type u_3} → {inst : Preorder α} → [self : PredOrder α] → α → α
-- Mathlib.Data.Seq.Defs
Stream'.Seq.mem_cons_of_mem : ∀ {α : Type u} (y : α) {a : α} {s : Stream'.Seq α}, a ∈ s → a ∈ Stream'.Seq.cons y s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.liftPred_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {p : β → Prop} {x : β}, p x → Filter.Germ.LiftPred p ↑x
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.NeBot.ne_bot : ∀ {β : Type u_2} {L : SummationFilter β} [self : L.NeBot], L.filter.NeBot
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impFrom.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) (x : Bᵒᵖ) (x_1 : Opposite.unop x ⟶ a),
  (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).app x).toFunctor.obj x_1 =
    CategoryTheory.CategoryStruct.comp x_1 f
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Lift a cf to a scf using the inclusion map.  -/
ContFract.instCoeGenContFract : {α : Type u_1} → [inst : One α] → [inst_1 : Zero α] → [inst_2 : LT α] → Coe (ContFract α) (GenContFract α)
-- Mathlib.Data.Set.Basic
Set.Nonempty.right : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty → t.Nonempty
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.foldl.eq_1 : ∀ {α : Type u} (f : α → Char → α) (init : α) (s : String), String.foldl f init s = String.Slice.foldl f init s.toSlice
-- Mathlib.Data.Nat.Nth
Nat.range_nth_of_infinite : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → Set.range (Nat.nth p) = Set.ofPred p
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Retract.projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y)
  [p : CategoryTheory.Projective Y], CategoryTheory.Projective X
-- Mathlib.Topology.Ultrafilter
continuous_iff_ultrafilter : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))
-- Mathlib.Order.Filter.NAry
Filter.map₂_inf_subset_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f₁ f₂ : Filter α} {g : Filter β},
  Filter.map₂ m (f₁ ⊓ f₂) g ≤ Filter.map₂ m f₁ g ⊓ Filter.map₂ m f₂ g
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- Let `u` be a family of units. Then the ratio `regOfFamily u / regulator K` is equal to the index
of the subgroup generated by `u` and `torsion K` inside the group of units of `K`.
 -/
NumberField.Units.regOfFamily_div_regulator : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ),
  NumberField.Units.regOfFamily u / NumberField.Units.regulator K =
    ↑(Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K).index
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.lift.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (x : S) (h : P.HasMap x),
  P.lift x h =
    Ideal.Quotient.liftₐ (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})
      (Polynomial.aevalAeval x ↑⋯.unit⁻¹) ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.comp.match_1.eq_4 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2)
  (x : CategoryTheory.WithTerminal C) (_Y : C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithTerminal.of _X) (CategoryTheory.WithTerminal.of _Y)
        (CategoryTheory.WithTerminal.of _Z))
  (h_2 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive (CategoryTheory.WithTerminal.of _X) x CategoryTheory.WithTerminal.star)
  (h_3 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _X) x)
  (h_4 :
    (x : CategoryTheory.WithTerminal C) →
      (_Y : C) → motive x CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _Y))
  (h_5 :
    Unit → motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star),
  (match x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => h_2 _X x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => h_3 _X x
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => h_4 x _Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star => h_5 ()) =
    h_4 x _Y
-- Mathlib.Data.NNReal.Defs
NNReal.exists_pow_lt_of_lt_one : ∀ {a b : NNReal}, 0 < a → b < 1 → ∃ n, b ^ n < a
-- Mathlib.RingTheory.Localization.Integral
/-- An element of a ring is algebraic over the ring `A` iff it is algebraic
over the field of fractions of `A`.
 -/
IsFractionRing.isAlgebraic_iff : ∀ (A : Type u_3) (K : Type u_4) (C : Type u_5) [inst : CommRing A] [IsDomain A] [inst_2 : Field K]
  [inst_3 : Algebra A K] [IsFractionRing A K] [inst_5 : CommRing C] [inst_6 : Algebra A C] [inst_7 : Algebra K C]
  [IsScalarTower A K C] {x : C}, IsAlgebraic A x ↔ IsAlgebraic K x
-- Mathlib.FieldTheory.RatFunc.Valuation
/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity.  -/
RatFunc.CompletionAtInfty : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → Type u_1
-- Init.Data.BitVec.Lemmas
/-- Shifting right by `n`, which is larger than the bitwidth `w` produces `0.  -/
BitVec.ushiftRight_eq_zero : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, w ≤ n → x >>> n = 0#w
-- Mathlib.Probability.Process.Filtration
/-- The filtration of events which only depends on finitely many coordinates
on the product space `Π i, X i`, `piFinset s` consists of measurable sets depending only on
coordinates in `s`, where `s : Finset ι`.  -/
MeasureTheory.Filtration.piFinset : {ι : Type u_4} →
  {X : ι → Type u_5} → [inst : (i : ι) → MeasurableSpace (X i)] → MeasureTheory.Filtration (Finset ι) MeasurableSpace.pi
-- Mathlib.Order.SaddlePoint
/-- Minimax formulation of saddle points  -/
isSaddlePointOn_value : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [inst : CompleteLinearOrder β]
  {a : E},
  a ∈ X →
    ∀ {b : F}, b ∈ Y → IsSaddlePointOn X Y f a b → ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : SizeOf R] (f : R) (n : ℕ) (g : Fin n → R),
  sizeOf { f := f, n := n, g := g } = 1 + sizeOf f + sizeOf n
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.coe_of : ∀ (X : Type u) [inst : UniformSpace X] [inst_1 : CompleteSpace X] [inst_2 : T0Space X], (CpltSepUniformSpace.of X).α = X
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Ioc : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.Ioc i j = Set.Ioc i.succ j.succ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Std.Data.DTreeMap.Internal.Operations
/-- An empty tree.  -/
Std.DTreeMap.Internal.Impl.empty : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The functor `C(·, R)₀` from topological spaces with zero (and `ContinuousMapZero` maps) to
non-unital star algebras.  -/
ContinuousMapZero.nonUnitalStarAlgHom_precomp : {X : Type u_1} →
  {Y : Type u_2} →
    (R : Type u_4) →
      [inst : Zero X] →
        [inst_1 : Zero Y] →
          [inst_2 : TopologicalSpace X] →
            [inst_3 : TopologicalSpace Y] →
              [inst_4 : TopologicalSpace R] →
                [inst_5 : CommSemiring R] →
                  [inst_6 : StarRing R] →
                    [inst_7 : IsTopologicalSemiring R] →
                      [inst_8 : ContinuousStar R] →
                        ContinuousMapZero X Y → ContinuousMapZero Y R →⋆ₙₐ[R] ContinuousMapZero X R
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_lt_sum : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {ι : Type u_6} {s : Finset ι} {f : ι → R} {g : Γ₀}, g ≠ ⊤ → (∀ i ∈ s, g < v (f i)) → g < v (∑ i ∈ s, f i)
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n →
    (UInt16.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.below.of_mem : ∀ {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)]
  {motive : (a : C) → P.limitsClosure J a → Prop} (X : C) (hX : P X),
  CategoryTheory.ObjectProperty.limitsClosure.below ⋯
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, Set.Icc a ⊤ = Set.Ici a
-- Batteries.Data.List.Lemmas
List.swapAt_def : ∀ {α : Type u_1} {xs : List α} {i : ℕ} {v : α}, xs.swapAt i v = (xs[i]?.getD v, xs.set i v)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- The function `fun x ↦ f x / r` tends to negative infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity.  -/
Filter.tendsto_div_const_atBot_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔
    0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.x : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget aig w) → aig.RefVec (self.len * w)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.ready : ℕ → optParam Bool false → optParam Bool false → Lean.Meta.Grind.SplitStatus
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.instNonemptyUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.Nonempty],
  P.unop.Nonempty
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tprod_setProd_singleton_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Set β) (c : γ)
  (f : β × γ → α), ∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (a : α) (s : α → β), ⨆ x ∈ {a}, s x = s a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → ∀ {fallback : α}, (t.insertIfNew k v).minKeyD fallback = k
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.dvd_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} {p : Polynomial A},
  minpoly A x ∣ p ↔ (Polynomial.aeval x) p = 0