mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Regular
RegularSpace.t3Space_iff_t0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X], T3Space X ↔ T0Space X
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.empty : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Int.borelSpace : BorelSpace ℤ
-- Mathlib.Order.Concept
/-- The lower polar of `t : Set β` along a relation `r : α → β → Prop` is the set of all elements
which `r` relates to all elements of `t`.  -/
lowerPolar : {α : Type u_2} → {β : Type u_3} → (α → β → Prop) → Set β → Set α
-- Mathlib.RingTheory.Ideal.Span
Ideal.iSup_eq_span : ∀ {α : Type u} [inst : Semiring α] {ι : Sort u_1} (p : ι → Ideal α), ⨆ i, p i = Ideal.span (⋃ i, ↑(p i))
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Ioo : ∀ {n : ℕ} (i j : Fin n), Fin.succ '' Set.Ioo i j = Set.Ioo i.succ j.succ
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.instModule : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : IsLocalRing R] →
        [inst_2 : CommRing S] →
          [inst_3 : IsLocalRing S] →
            [inst_4 : Algebra R S] →
              [IsLocalHom (algebraMap R S)] → Module (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_8 : {α : Type u} → Std.Rii.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_natTrailingDegree : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.natTrailingDegree = p.natTrailingDegree
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.IsPrimitive.eq_1 : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] (ψ : AddChar R R'),
  ψ.IsPrimitive = ∀ ⦃a : R⦄, a ≠ 0 → ψ.mulShift a ≠ 1
-- Init.Data.UInt.Bitwise
UInt64.not_eq_comm : ∀ {a b : UInt64}, ~~~a = b ↔ a = ~~~b
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.initializationOptions? : Lean.Lsp.InitializeParams → Option Lean.Lsp.InitializationOptions
-- Lean.Elab.DeclModifiers
Lean.Elab.instInhabitedRecKind.default : Lean.Elab.RecKind
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.forIn_filterMap : ∀ {α β β₂ γ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α Id β] [inst_1 : Monad n]
  [inst_2 : Std.Internal.Do.Assertion Pred] [inst_3 : Std.Internal.Do.Assertion EPred]
  [inst_4 : Std.Internal.Do.WPMonad n Pred EPred] [Std.Iterators.Finite α Id] [inst_6 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)}
  {P : Pred} {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc =>
        match f out with
        | some c => g c acc
        | none => pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.Iter.filterMap f it) init g ⦃ Q; eQ ⦄
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom.category_comp_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (X Y : CategoryTheory.Bicategory.InducedBicategory C F) {X_1 Y_1 Z : X ⟶ Y}
  (u : CategoryTheory.Bicategory.InducedBicategory.Hom₂ X_1 Y_1)
  (v : CategoryTheory.Bicategory.InducedBicategory.Hom₂ Y_1 Z),
  (CategoryTheory.CategoryStruct.comp u v).hom = CategoryTheory.CategoryStruct.comp u.hom v.hom
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.isSorted.go : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Bool
-- Mathlib.Algebra.Group.Action.Units
AddUnits.instVAdd : {M : Type u_3} → {α : Type u_5} → [inst : AddMonoid M] → [VAdd M α] → VAdd (AddUnits M) α
-- Mathlib.RingTheory.Jacobson.Ideal
TwoSidedIdeal.asIdeal_jacobson : ∀ {R : Type u} [inst : Ring R] (I : TwoSidedIdeal R),
  TwoSidedIdeal.asIdeal I.jacobson = (TwoSidedIdeal.asIdeal I).jacobson
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- To show that `η_X` is an equalizer for `(UFη_X, η_UFX)`, it suffices to assume it's always an
equalizer of something (i.e. a regular mono).
 -/
CategoryTheory.LiftRightAdjoint.unitEqualises : {A : Type u₁} →
  {B : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} A] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {U : CategoryTheory.Functor A B} →
          {F : CategoryTheory.Functor B A} →
            (adj₁ : F ⊣ U) →
              ((X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) →
                (X : B) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (adj₁.unit.app X) ⋯)
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : NonAssocSemiring α} {inst_1 : Preorder α} {inst_2 : NonAssocSemiring β}
  {inst_3 : Preorder β} {toRingHom : α →+* β} {monotone' : Monotone (↑↑toRingHom).toFun} {toRingHom_1 : α →+* β}
  {monotone'_1 : Monotone (↑↑toRingHom_1).toFun},
  { toRingHom := toRingHom, monotone' := monotone' } = { toRingHom := toRingHom_1, monotone' := monotone'_1 } →
    toRingHom = toRingHom_1
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom₂.mk : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} →
        {X Y : CategoryTheory.Bicategory.InducedBicategory C F} →
          {f g : X ⟶ Y} → (f.hom ⟶ g.hom) → CategoryTheory.Bicategory.InducedBicategory.Hom₂ f g
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySheafFor.isStronglySeparatedFor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)}, E.IsStronglySheafFor F → E.IsStronglySeparatedFor F
-- Mathlib.FieldTheory.Perfect
Polynomial.rootsExpandEquivRoots_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R)
  [inst_3 : DecidableEq R] [inst_4 : PerfectRing R p] (x : ↥((Polynomial.expand R p) f).roots.toFinset),
  ↑((Polynomial.rootsExpandEquivRoots p f) x) = ↑x ^ p
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.of_isEmpty : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [IsEmpty β] (f : α → β)
  (μa : MeasureTheory.Measure α) (μb : MeasureTheory.Measure β), MeasureTheory.MeasurePreserving f μa μb
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.xs : {α : Type u} → SubarrayIterator α → Subarray α
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_units : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (u : ℤ_[p]ˣ), ‖↑u‖ = 1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitArg.mk : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.SplitArg
-- Mathlib.RingTheory.Smooth.AdicCompletion
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux.eq_def : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (I : Ideal S) (f : A →ₐ[R] S ⧸ I) [inst_5 : Algebra.FormallySmooth R A]
  (x : ℕ),
  Algebra.FormallySmooth.liftAdicCompletionAux✝ I f x =
    match x with
    | 0 => default
    | 1 => (↑(Ideal.quotientEquivAlgOfEq R ⋯)).comp f
    | m.succ.succ =>
      Algebra.FormallySmooth.lift (Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
        ((↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp
          (Algebra.FormallySmooth.liftAdicCompletionAux✝ I f (m + 1)))
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.toFinsupp 1 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldl_eq_foldl : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type u_1} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DTreeMap.Internal.Impl.foldl f init t = List.foldl (fun acc p => f acc p.fst p.snd) init t.toListModel
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition'.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (fb : γ) → motive (some fb)),
  (match none with
    | none => h_1 ()
    | some fb => h_2 fb) =
    h_1 ()
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.const_inv_smul₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : Neg β]
  [inst_2 : GroupWithZero γ] [inst_3 : DistribMulAction γ α],
  Function.Antiperiodic f c → ∀ {a : γ}, a ≠ 0 → Function.Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.fromIso_map_one_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y)
  (f : CategoryTheory.WalkingIso.one ⟶ CategoryTheory.WalkingIso.one),
  (CategoryTheory.WalkingIso.fromIso e).map f = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Computability.Primrec.List
Primrec.vector_cons : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec₂ List.Vector.cons
-- Mathlib.RingTheory.ChainOfDivisors
mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [inst_3 : Subsingleton Mˣ] [inst_4 : Subsingleton Nˣ] [inst_5 : UniqueFactorizationMonoid M]
  [inst_6 : UniqueFactorizationMonoid N] {m p : M} {n : N},
  m ≠ 0 →
    n ≠ 0 →
      ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) {d : { l // l ∣ m } ≃ { l // l ∣ n }},
        (∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') →
          ↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.get_eq_of_lt_skipPrefixWhile_char : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile c), pos.get ⋯ = c
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.Nat.unaryCast.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.not_isUnit : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [inst_1 : CommRing R] {v : Valuation R Γ}
  [hv : v.IsRankOneDiscrete] {π : ↥v.integer}, v.IsUniformizer ↑π → ¬IsUnit π
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerLeft_counit_iso_of_L_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful],
  CategoryTheory.IsIso (L.whiskerLeft h.counit)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_lTensor : ∀ {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [Module.Flat R M₂] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs → RingTheory.Sequence.IsWeaklyRegular (TensorProduct R M₂ M) rs
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_refl : ∀ {C : Type u_1} {D₁ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] (W : CategoryTheory.MorphismProperty C)
  (L₁ : CategoryTheory.Functor C D₁) [inst_2 : L₁.IsLocalization W] {X Y : C} (f : L₁.obj X ⟶ L₁.obj Y),
  (CategoryTheory.Localization.homEquiv W L₁ L₁) f = f
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.assoc_toCoalgEquiv : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Semiring D] [inst_9 : Bialgebra S C]
  [inst_10 : Bialgebra R D] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C],
  ↑(Bialgebra.TensorProduct.assoc R S A C D) = Coalgebra.TensorProduct.assoc R S A C D
-- Mathlib.Order.Minimal
IsGreatest.maximal_iff : ∀ {α : Type u_2} {a x : α} {s : Set α} [inst : PartialOrder α], IsGreatest s a → (Maximal (fun x => x ∈ s) x ↔ x = a)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c RBTree.RBNode.nil v r).min? = some v
-- Mathlib.Data.List.AList
AList.perm_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ s₃ s₄ : AList β},
  s₁.entries.Perm s₂.entries → s₃.entries.Perm s₄.entries → (s₁ ∪ s₃).entries.Perm (s₂ ∪ s₄).entries
-- Mathlib.MeasureTheory.Integral.IntervalAverage
interval_average_eq_div : ∀ (f : ℝ → ℝ) (a b : ℝ), ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_add_closedBall_subset : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E), p.closedBall x₁ r₁ + p.closedBall x₂ r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.mk'_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ),
  IsLocalization.mk' (LaurentPolynomial R) p ⟨Polynomial.X ^ n, ⋯⟩ = Polynomial.toLaurent p * LaurentPolynomial.T (-↑n)
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank_def : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : Group.FG G], CommGroup.freeRank G = Group.rank (G ⧸ CommGroup.torsion G)
-- Mathlib.MeasureTheory.Integral.Prod
/-- Double integrals commute with subtraction.  -/
MeasureTheory.integral_integral_sub : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] ⦃f g : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) →
    MeasureTheory.Integrable g (μ.prod ν) →
      ∫ (x : α), ∫ (y : β), f (x, y) - g (x, y) ∂ν ∂μ =
        ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_inl_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.lift AddMonoid.Coprod.inl AddMonoid.Coprod.inr = AddMonoidHom.id (AddMonoid.Coprod M N)
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
SeminormedCommGroup.dist_eq : ∀ {E : Type u_8} [self : SeminormedCommGroup E] (x y : E), dist x y = ‖x⁻¹ * y‖
-- Lean.CoreM
Lean.Core.instMonadRecDepthCoreM : Lean.MonadRecDepth Lean.CoreM
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- An alias for `toSheafedSpace`, where the result type is a `RingedSpace`.
This allows us to use dot-notation for the `RingedSpace` namespace.
 -/
AlgebraicGeometry.LocallyRingedSpace.toRingedSpace : AlgebraicGeometry.LocallyRingedSpace → AlgebraicGeometry.RingedSpace
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.mulOp_apply_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (a : Mᵐᵒᵖ),
  (AddHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- Copy of a Delone set with new fields equal to the old ones.
Useful to fix definitional equalities.  -/
Delone.DeloneSet.copy : {X : Type u_1} →
  [inst : MetricSpace X] →
    (D : Delone.DeloneSet X) →
      (carrier : Set X) →
        (packingRadius coveringRadius : NNReal) →
          carrier = D.carrier → packingRadius = D.packingRadius → coveringRadius = D.coveringRadius → Delone.DeloneSet X
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.continuous : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), Continuous ⇑e
-- Mathlib.Topology.Maps.Basic
IsOpenMap.nhds_le : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDidCloseTextDocumentParams : Lean.Lsp.FileSource Lean.Lsp.DidCloseTextDocumentParams
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.orthogonal_eq_top_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), Kᗮ = ⊤ ↔ K = ⊥
-- Mathlib.Algebra.Group.Action.Prod
Prod.vaddAssocClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : VAdd M α] [inst_1 : VAdd M β] [inst_2 : VAdd N α]
  [inst_3 : VAdd N β] [inst_4 : VAdd M N] [VAddAssocClass M N α] [VAddAssocClass M N β], VAddAssocClass M N (α × β)
-- Lean.Meta.Tactic.Grind.Arith.EvalNum
Lean.Meta.Grind.Arith.checkExp : ℕ → OptionT Lean.Meta.Grind.GrindM Unit
-- Mathlib.Analysis.SpecificLimits.FloorPow
/-- If a monotone sequence `u` is such that `u n / n` tends to a limit `l` along subsequences with
exponential growth rate arbitrarily close to `1`, then `u n / n` tends to `l`.  -/
tendsto_div_of_monotone_of_exists_subseq_tendsto_div : ∀ (u : ℕ → ℝ) (l : ℝ),
  Monotone u →
    (∀ (a : ℝ),
        1 < a →
          ∃ c,
            (∀ᶠ (n : ℕ) in Filter.atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
              Filter.Tendsto c Filter.atTop Filter.atTop ∧
                Filter.Tendsto (fun n => u (c n) / ↑(c n)) Filter.atTop (nhds l)) →
      Filter.Tendsto (fun n => u n / ↑n) Filter.atTop (nhds l)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.exists_pow_neg_lt_rat : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {ε : ℚ}, 0 < ε → ∃ k, ↑p ^ (-↑k) < ε
-- Mathlib.Algebra.Polynomial.Roots
/-- A version of `mem_rootSet` that requires the polynomial to be non-zero after mapping
instead of requiring it to be non-zero and `NoZeroSMulDivisors`.  -/
Polynomial.mem_rootSet' : ∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S] {a : S}, a ∈ p.rootSet S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_compl_eq_mk_compl_finite_same : ∀ {α : Type u} [Finite α] {s t : Set α}, Cardinal.mk ↑s = Cardinal.mk ↑t → Cardinal.mk ↑sᶜ = Cardinal.mk ↑tᶜ
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.symm_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D), f.symm.hom = f.inv
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Measure.toTemperedDistribution.congr_simp : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : SecondCountableTopology E] (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1)
  [hμ : μ.HasTemperateGrowth], μ.toTemperedDistribution = μ_1.toTemperedDistribution
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_lt_degree_mul_X : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.degree < (p * Polynomial.X).degree
-- Lean.Setup
Lean.instReprModuleArtifacts.repr : Lean.ModuleArtifacts → ℕ → Std.Format
-- Mathlib.ModelTheory.Order
/-- Any model of a theory of partial orders is a partial order.  -/
FirstOrder.Language.partialOrderOfModels : (L : FirstOrder.Language) →
  (M : Type w') → [inst : L.IsOrdered] → [inst_1 : L.Structure M] → [h : M ⊨ L.partialOrderTheory] → PartialOrder M
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_tensorObj : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  (X Y : C₁ × C₂),
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y =
    (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 Y.1, CategoryTheory.MonoidalCategoryStruct.tensorObj X.2 Y.2)
-- Init.Data.Array.MinMax
Array.max_eq_get_max? : ∀ {α : Type u_1} [inst : Max α] (xs : Array α) (h : xs ≠ #[]), xs.max h = xs.max?.get ⋯
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderivWithin_continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} {M : ι → Type u_6}
  [inst_3 : (i : ι) → NormedAddCommGroup (M i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H}
  [inst_7 : Fintype ι],
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      ∀ (u : (i : ι) → M i), fderivWithin 𝕜 (fun y => (c y) u) s x = (fderivWithin 𝕜 c s x).flipMultilinear u
-- Init.Data.Ord.Basic
Ordering.isGE_of_eq_eq : ∀ {o : Ordering}, o = Ordering.eq → o.isGE = true
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_mul : ∀ (x y : Cardinal.{u_1}), Cardinal.toNat (x * y) = Cardinal.toNat x * Cardinal.toNat y
-- Mathlib.Data.Rat.Defs
Rat.pos : ∀ (a : ℚ), 0 < a.den
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent_to_quotient_square : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (x : ↥I),
  I.cotangentToQuotientSquare (I.toCotangent x) = (Submodule.mkQ (I ^ 2)) ↑x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k a : α}
  {fallback v : β},
  Std.DTreeMap.Const.getD (t.insert k v) a fallback =
    if cmp k a = Ordering.eq then v else Std.DTreeMap.Const.getD t a fallback
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_smul_left : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (c : ℝ)
  (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.setToSimpleFunc (fun s => c • T s) f = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.ι_colimitLimitIso_limit_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (a : K) (b : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.limit F) a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLimitIso F).hom
        (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.colimit F.flip) b)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F b).app a)
      ((CategoryTheory.Limits.colimit.ι F.flip a).app b)