mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Condensed.Discrete.Module
/-- Auxiliary definition for `functorIsoDiscrete`.  -/
LightCondMod.LocallyConstant.functorIsoDiscreteAux₁ : (R : Type u) →
  [inst : Ring R] → (M : ModuleCat R) → M ≅ ModuleCat.of R (LocallyConstant ↑(LightProfinite.of PUnit.{u + 1}).toTop ↑M)
-- Mathlib.Order.Filter.Map
Filter.comap_bot : ∀ {α : Type u_1} {β : Type u_2} {m : α → β}, Filter.comap m ⊥ = ⊥
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKey? a x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => none
    | Std.DHashMap.Internal.AssocList.cons k value es =>
      if (k == a) = true then some k else Std.DHashMap.Internal.AssocList.getKey? a es
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent.eq_1 : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.Solution'_descent✝ S =
    { a := FermatLastTheoremForThreeGen.Solution.Y✝ S,
      b := ↑(FermatLastTheoremForThreeGen.Solution.u₄✝ S) * FermatLastTheoremForThreeGen.Solution.Z✝ S,
      c :=
        (hζ.toInteger - 1) ^ (FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 1) *
          FermatLastTheoremForThreeGen.Solution.X✝ S,
      u := FermatLastTheoremForThreeGen.Solution.u₅✝ S, ha := ⋯, hb := ⋯, hc := ⋯, coprime := ⋯, hcdvd := ⋯, H := ⋯ }
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableVAdd.toMeasurableConstVAdd : ∀ {M : Type u_2} {α : Type u_3} {inst : VAdd M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α}
  [self : MeasurableVAdd M α], MeasurableConstVAdd M α
-- Std.Sync.Channel
Std.Channel.instAsyncReadOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncRead (Std.Channel α) α
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.oppositeShiftFunctorAdd_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b : A),
  (CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).hom.app X =
    ((CategoryTheory.shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X_1 : CategoryTheory.CostructuredArrow L X),
  (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).hom.app X_1 =
    CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner : ∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] (𝕜 : Type u_2) [inst_1 : RCLike 𝕜]
  [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  (∀ (y : E),
      Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop
        (nhds 0)) →
    MeasureTheory.IsTightMeasureSet (Set.range μ)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_δ'' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc),
  CategoryTheory.CategoryStruct.comp (X.δ j.succ) (X.δ (i.castLT ⋯)) =
    CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j)
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically : @AlgebraicGeometry.GeometricallyIrreducible = AlgebraicGeometry.geometrically fun x => IrreducibleSpace ↥x
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TacticNode.mk.injEq : ∀ (ctxI : Lean.Elab.ContextInfo) (tacI : Lean.Elab.TacticInfo) (mayFail : Bool) (ctxI_1 : Lean.Elab.ContextInfo)
  (tacI_1 : Lean.Elab.TacticInfo) (mayFail_1 : Bool),
  ({ ctxI := ctxI, tacI := tacI, mayFail := mayFail } = { ctxI := ctxI_1, tacI := tacI_1, mayFail := mayFail_1 }) =
    (ctxI = ctxI_1 ∧ tacI = tacI_1 ∧ mayFail = mayFail_1)
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.instCompactSpaceCarrierDisk : ∀ (n : ℕ), CompactSpace ↑(TopCat.disk n)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.instTensorSignsNatDown : (ComplexShape.down ℕ).TensorSigns
-- Mathlib.Computability.Halting
/-- The **Halting problem** is not computable  -/
ComputablePred.halting_problem : ∀ (n : ℕ), ¬ComputablePred fun c => (c.eval n).Dom
-- Init.Data.String.TakeDrop
String.Slice.takeRightWhile : String.Slice → (Char → Bool) → String.Slice
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.trans_apply : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] (e₁₂ : A ≃ₐc[R] B)
  (e₂₃ : B ≃ₐc[R] C) (x : A), (e₁₂.trans e₂₃) x = ↑e₂₃ (↑e₁₂ x)
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.mk : Array Lean.Elab.Tactic.Omega.Proof →
  ℕ →
    Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact →
      Std.HashSet Lean.Omega.Coeffs →
        List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ) →
          (possible : Bool) →
            (proveFalse? : Option Lean.Elab.Tactic.Omega.Proof) →
              autoParam ((possible || proveFalse?.isSome) = true)
                  Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam →
                Thunk String → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Algebra.Order.Algebra
algebraMap_pos : ∀ {α : Type u_1} (β : Type u_2) [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [Nontrivial β] [SMulPosStrictMono α β] {a : α},
  0 < a → 0 < (algebraMap α β) a
-- Mathlib.Topology.Compactness.Compact
instNeBotCoclosedCompactOfNoncompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [NoncompactSpace X], (Filter.coclosedCompact X).NeBot
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.discreteUniformity_iff : ∀ {α : Type u_1} [inst : UniformSpace α], DiscreteUniformity (TopologicalSpace.Compacts α) ↔ DiscreteUniformity α
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- `m₁` is the morphism `a` of (TR 4) as presented in Stacks.  -/
CategoryTheory.Triangulated.Octahedron'.m₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃ → (Z₁₂ ⟶ Z₁₃)
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.num : ℕ → Lean.Meta.Sym.Offset
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_reflects_exact : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N1 : Type u_1}
  [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type u_2} [inst_5 : AddCommGroup N2] [inst_6 : Module R N2]
  {N3 : Type u_3} [inst_7 : AddCommGroup N3] [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3)
  [fl : Module.FaithfullyFlat R M],
  Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23) → Function.Exact ⇑l12 ⇑l23
-- Init.Data.Range.Polymorphic.UInt
USize.instHasSize_2 : Std.Rxi.HasSize USize
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n : A) (X : C),
  (CategoryTheory.shiftFunctor C (-n)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) =
    (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((CategoryTheory.shiftFunctor C (-n)).obj X)
-- Mathlib.FieldTheory.PerfectClosure
/-- The perfect closure is the smallest extension that makes frobenius surjective.  -/
PerfectClosure : (K : Type u) → [inst : CommRing K] → (p : ℕ) → [Fact (Nat.Prime p)] → [CharP K p] → Type u
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_sep : ∀ {α : Type u} (s : Set α) (t : α → Prop), Cardinal.mk ↑{x | x ∈ s ∧ t x} = Cardinal.mk ↑{x | t ↑x}
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Definable₂.out_equiv : ∀ (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [inst : ZFSet.Definable₂ f] {x₁ y₁ x₂ y₂ : PSet.{u}},
  x₁ ≈ y₁ → x₂ ≈ y₂ → ZFSet.Definable₂.out f x₁ x₂ ≈ ZFSet.Definable₂.out f y₁ y₂
-- Init.Data.ByteArray.Basic
ByteArray.instEmptyCollection : EmptyCollection ByteArray
-- Mathlib.Topology.Algebra.Monoid
addMonoidHomOfTendsto_apply : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂]
  [inst_2 : AddZeroClass M₁] [inst_3 : AddZeroClass M₂] [inst_4 : ContinuousAdd M₂] {F : Type u_8}
  [inst_5 : FunLike F M₁ M₂] [inst_6 : AddMonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F)
  [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)), ⇑(addMonoidHomOfTendsto f g h) = f
-- Mathlib.Data.Finset.Defs
Finset.mem_mk : ∀ {α : Type u_1} {a : α} {s : Multiset α} {nd : s.Nodup}, a ∈ { val := s, nodup := nd } ↔ a ∈ s
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.aeval_unique : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] {ε : PowerSeries R →ₐ[R] S}
  (hε : Continuous ⇑ε), PowerSeries.aeval ⋯ = ε
-- Init.Data.UInt.Lemmas
UInt64.toUSize_neg : ∀ (a : UInt64), (-a).toUSize = -a.toUSize
-- Init.Data.Iterators.Combinators.Monadic.Attach
/-- “Attaches” individual proofs to an iterator of values that satisfy a predicate `P`, returning an
iterator with values in the corresponding subtype `{ x // P x }`.

**Termination properties:**

* `Finite` instance: only if the base iterator is finite
* `Productive` instance: only if the base iterator is productive
 -/
Std.IterM.attachWith : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        (it : Std.IterM m β) →
          (P : β → Prop) → (∀ (out : β), it.IsPlausibleIndirectOutput out → P out) → Std.IterM m { out // P out }
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_iInf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Type u_5} {f : M →ₙ* N},
  Function.Surjective ⇑f → ∀ (S : ι → Subsemigroup N), Subsemigroup.map f (⨅ i, Subsemigroup.comap f (S i)) = iInf S
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_eq_one : ∀ {o : Ordinal.{u_1}}, o.card = 1 ↔ o = 1
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a ^ 0 = 1`  -/
CommGroupWithZero.zpow_zero' : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀] (a : G₀), a ^ 0 = 1
-- Mathlib.FieldTheory.Galois.Profinite
/-- The composition of `finGaloisGroupFunctor` with
the forgetful functor from `FiniteGrp` to `ProfiniteGrp`.  -/
InfiniteGalois.asProfiniteGaloisGroupFunctor : (k : Type u_3) →
  (K : Type u_4) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] → CategoryTheory.Functor (FiniteGaloisIntermediateField k K)ᵒᵖ ProfiniteGrp.{u_4}
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- **Alias** of `CircleIntegrable.fun_continuousOn_mul`.

---

Eta-expanded form of `CircleIntegrable.continuousOn_mul`

---

If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g * f` is
circle integrable.
 -/
CircleIntegrable.fun_mul_of_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (fun i => g i * f i) c R
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instCompactSpaceQuotientSubgroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [CompactSpace G] (N : Subgroup G), CompactSpace (G ⧸ N)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.edist_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E), edist (e x) (e y) = edist x y
-- Mathlib.Analysis.RCLike.Extend
StrongDual.extendRCLikeₗ_symm_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : StrongDual 𝕜 F), StrongDual.extendRCLikeₗ.symm f = RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.morphismProperty_eq_top : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V]
  {W : CategoryTheory.MorphismProperty (CategoryTheory.Cat.FreeRefl V)} [W.IsMultiplicative],
  (∀ {x y : V} (e : x ⟶ y), W (CategoryTheory.Cat.FreeRefl.homMk e)) → W = ⊤
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.Context.mk.sizeOf_spec : ∀ (structId : ℕ), sizeOf { structId := structId } = 1 + sizeOf structId
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Zipper α β),
  x.toList =
    match x with
    | Std.DTreeMap.Internal.Zipper.done => []
    | Std.DTreeMap.Internal.Zipper.cons k v tree next => ⟨k, v⟩ :: tree.toList ++ next.toList
-- Mathlib.Order.Sublocale
Sublocale.mk_le_mk : ∀ {X : Type u_1} [inst : Order.Frame X] (carrier₁ carrier₂ : Set X) (sInf_mem'₁ : ∀ s ⊆ carrier₁, sInf s ∈ carrier₁)
  (sInf_mem'₂ : ∀ s ⊆ carrier₂, sInf s ∈ carrier₂) (himp_mem'₁ : ∀ (a b : X), b ∈ carrier₁ → a ⇨ b ∈ carrier₁)
  (himp_mem'₂ : ∀ (a b : X), b ∈ carrier₂ → a ⇨ b ∈ carrier₂),
  { carrier := carrier₁, sInf_mem' := sInf_mem'₁, himp_mem' := himp_mem'₁ } ≤
      { carrier := carrier₂, sInf_mem' := sInf_mem'₂, himp_mem' := himp_mem'₂ } ↔
    carrier₁ ⊆ carrier₂
-- Mathlib.Data.ENat.Basic
ENat.sub_top : ∀ (a : ℕ∞), a - ⊤ = 0
-- Mathlib.Order.Antisymmetrization
AntisymmRel.le_congr_right : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → (a ≤ b ↔ a ≤ c)
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.mono_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} {y z : Filter β},
  Filter.Tendsto f x y → y ≤ z → Filter.Tendsto f x z
-- Mathlib.Data.PFun
PFun.preimage_asSubtype : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s
-- Mathlib.Order.Defs.LinearOrder
/-- Default definition of `max`.  -/
maxDefault : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → α → α
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.surjective_iff_isField : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R], Function.Surjective ⇑(algebraMap R K) ↔ IsField R
-- Mathlib.Order.Filter.Basic
Filter.Eventually.and : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_toUSize : ∀ (n : ISize) (h : System.Platform.numBits = 64), n.toUSize.toBitVec64 h = n.toBitVec64 h
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.card_neighborFinset_union_of_adj : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ}
  [inst_2 : DecidableEq V] {v w : V},
  G.IsSRGWith n k ℓ μ → G.Adj v w → (G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - ℓ
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_C : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  (a : T), (Polynomial.C a).aroots S = 0
-- Init.Data.BitVec.Basic
/-- Raises a bitvector to a natural number power. Usually accessed via the `^` operator.

Note that this is currently an inefficient implementation,
and should be replaced via an `@[extern]` with a native implementation.
See https://github.com/leanprover/lean4/issues/7887.
 -/
BitVec.pow : {n : ℕ} → BitVec n → ℕ → BitVec n
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_domain_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F} {x : E}, x ∈ f.domain ↔ ∃ y, (x, y) ∈ f.graph
-- Mathlib.Topology.Constructions
Topology.isInducing_sigmaMap : ∀ {ι : Type u_5} {κ : Type u_6} {σ : ι → Type u_7} {τ : κ → Type u_8} [inst : (i : ι) → TopologicalSpace (σ i)]
  [inst_1 : (k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)},
  Function.Injective f₁ → (Topology.IsInducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Topology.IsInducing (f₂ i))
-- Mathlib.Geometry.Euclidean.Basic
/-- Distances `r₁` `r₂` of `p` from two different points `c₁` `c₂` determine at
most two points `p₁` `p₂` in a two-dimensional subspace containing those points
(two circles intersect in at most two points).  -/
EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [FiniteDimensional ℝ ↥s.direction],
  Module.finrank ℝ ↥s.direction = 2 →
    ∀ {c₁ c₂ p₁ p₂ p : P},
      c₁ ∈ s →
        c₂ ∈ s →
          p₁ ∈ s →
            p₂ ∈ s →
              p ∈ s →
                ∀ {r₁ r₂ : ℝ},
                  c₁ ≠ c₂ →
                    p₁ ≠ p₂ →
                      dist p₁ c₁ = r₁ →
                        dist p₂ c₁ = r₁ →
                          dist p c₁ = r₁ → dist p₁ c₂ = r₂ → dist p₂ c₂ = r₂ → dist p c₂ = r₂ → p = p₁ ∨ p = p₂
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.mergeSort.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a : α) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [a], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_2 a x
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_ofCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (A : E →SL[σ] F),
  (ContinuousLinearMapWOT.ofCLM A).toCLM = A
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet β] (f : α → β) (s : Finset α), ⨆ x ∈ ↑s, f x = ⨆ x ∈ s, f x
-- Mathlib.Data.Finset.Basic
Finset.not_disjoint_iff_nonempty_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, ¬Disjoint s t ↔ (s ∩ t).Nonempty
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_vadd_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq β] [inst_1 : DecidableEq γ] [inst_2 : VAdd α β]
  [inst_3 : VAdd α γ] (f : β → γ) (a : α) (s : Finset β),
  (∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → Finset.image f (a +ᵥ s) = a +ᵥ Finset.image f s
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : PseudoEpimorphism α β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_iInf : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {ι : Sort u_1} [Nonempty ι] (f : R →+* S),
  Function.Injective ⇑f → ∀ (s : ι → Subring R), Subring.map f (iInf s) = ⨅ i, Subring.map f (s i)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Equivalence.mapCommGrp_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided], e.mapCommGrp.functor = e.functor.mapCommGrp
-- Mathlib.CategoryTheory.Products.Basic
/-- The backward direction for `functorProdFunctorEquiv`  -/
CategoryTheory.functorProdToProdFunctor : (A : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    (B : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        (C : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            CategoryTheory.Functor (CategoryTheory.Functor A (B × C))
              (CategoryTheory.Functor A B × CategoryTheory.Functor A C)
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_le_pi_nnnorm : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i)
  (i : ι), ‖f i‖₊ ≤ ‖f‖₊
-- Mathlib.Tactic.Linter.FindDeprecations
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.mk.sizeOf_spec : ∀ (module decl : Lean.Name) (rgStart rgStop : Lean.Position) (since : String),
  sizeOf { module := module, decl := decl, rgStart := rgStart, rgStop := rgStop, since := since } =
    1 + sizeOf module + sizeOf decl + sizeOf rgStart + sizeOf rgStop + sizeOf since
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Prod.snd : (x, y) ↦ y` as a bundled continuous map.  -/
ContinuousMap.snd : {α : Type u_1} → {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → C(α × β, β)