mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.fixedBy.eq_1 : ∀ {M : Type u_1} (α : Type u_3) [inst : Monoid M] [inst_1 : MulAction M α] (m : M),
  MulAction.fixedBy α m = {x | m • x = x}
-- Mathlib.Data.Num.Basic
Num.decidableLT : DecidableLT Num
-- Batteries.Data.Float.Lemmas
Float.Model.mk.congr_simp : ∀ (toBits toBits_1 : UInt64) (e_toBits : toBits = toBits_1) (valid : Float.Model.Format.binary64.Valid toBits.toBitVec),
  { toBits := toBits, valid := valid } = { toBits := toBits_1, valid := ⋯ }
-- Mathlib.GroupTheory.Perm.Fin
Fin.instNeZeroNatHSubVal_mathlib : ∀ {n : ℕ} {i : Fin n}, NeZero (n - ↑i)
-- Init.Data.Int.Gcd
Int.lcm_lcm_self_left_left : ∀ (m n : ℤ), (↑(m.lcm n)).lcm m = n.lcm m
-- Mathlib.Data.Sym.Basic
Sym.cons_inj_right : ∀ {α : Type u_1} {n : ℕ} (a : α) (s s' : Sym α n), a ::ₛ s = a ::ₛ s' ↔ s = s'
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_idempotent : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.normalCore.normalCore = H.normalCore
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + -1 = q)
  {Z : C} (h : G.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v q q ⋯) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_inter_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Antitone f → Monotone g → Monotone fun x => Set.Ico (f x) (g x)
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.RecArgInfo.mk.inj : ∀ {fnName : Lean.Name} {fixedParamPerm : Lean.Elab.FixedParamPerm} {recArgPos : ℕ} {indicesPos : Array ℕ}
  {indGroupInst : Lean.Elab.Structural.IndGroupInst} {indIdx : ℕ} {fnName_1 : Lean.Name}
  {fixedParamPerm_1 : Lean.Elab.FixedParamPerm} {recArgPos_1 : ℕ} {indicesPos_1 : Array ℕ}
  {indGroupInst_1 : Lean.Elab.Structural.IndGroupInst} {indIdx_1 : ℕ},
  { fnName := fnName, fixedParamPerm := fixedParamPerm, recArgPos := recArgPos, indicesPos := indicesPos,
        indGroupInst := indGroupInst, indIdx := indIdx } =
      { fnName := fnName_1, fixedParamPerm := fixedParamPerm_1, recArgPos := recArgPos_1, indicesPos := indicesPos_1,
        indGroupInst := indGroupInst_1, indIdx := indIdx_1 } →
    fnName = fnName_1 ∧
      fixedParamPerm = fixedParamPerm_1 ∧
        recArgPos = recArgPos_1 ∧ indicesPos = indicesPos_1 ∧ indGroupInst = indGroupInst_1 ∧ indIdx = indIdx_1
-- Mathlib.CategoryTheory.Products.Unitor
/-- The left inverse unitor `C ⥤ 1 × C`  -/
CategoryTheory.prod.leftInverseUnitor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} × C)
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.le_W : ∀ (k : ℕ), (2 * ↑k + 1) / (2 * ↑k + 2) * (Real.pi / 2) ≤ Real.Wallis.W k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_mem_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtDTreeMap α (fun x => Unit) cmp}, (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁ = t₂
-- Lean.Parser.Term
Lean.Parser.Term.pipeCompletion : Lean.Parser.TrailingParser
-- Aesop.Tree.Data
Aesop.Goal.setParent : Aesop.MVarClusterRef → Aesop.Goal → Aesop.Goal
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km fallback : α}, t.minKey? = some km → t.getKeyD km fallback = km
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- See `toBelow`  -/
_private.Lean.Elab.PreDefinition.Structural.BRecOn.0.Lean.Elab.Structural.toBelowAux : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.Rayleigh
/-- In this variant of the Beatty sequence for `r`, the `k`th term is `⌈k * r⌉ - 1`.  -/
beattySeq' : ℝ → ℤ → ℤ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The cosine of the oriented angle at `p` between two points not equal to `p` equals that of the
unoriented angle.  -/
EuclideanGeometry.cos_oangle_eq_cos_angle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ : P}, p₁ ≠ p → p₂ ≠ p → (EuclideanGeometry.oangle p₁ p p₂).cos = Real.cos (EuclideanGeometry.angle p₁ p p₂)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isSup : ℕ → ℕ → ℕ → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.GroupTheory.ArchimedeanDensely
WithZero.denselyOrdered_set_iff_subsingleton : ∀ {X : Type u_3} [inst : LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithZero X)},
  DenselyOrdered ↑s ↔ s.Subsingleton
-- Mathlib.Analysis.Convex.Extrema
/-- A local maximum of a concave function is a global maximum.  -/
IsMaxOn.of_isLocalMax_of_convex_univ : ∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [inst_5 : AddCommGroup β] [inst_6 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_8 : Module ℝ β] [IsOrderedModule ℝ β] [PosSMulReflectLE ℝ β] {f : E → β} {a : E},
  IsLocalMax f a → ConcaveOn ℝ Set.univ f → ∀ (x : E), f x ≤ f a
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmL_apply_of_notMem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → ∀ (y : F), (Bundle.Trivialization.symmL R e b) y = 0
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center of isomorphic (not necessarily associative) semirings are isomorphic.  -/
Subsemiring.centerCongr : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] → R ≃+* S → ↥(Subsemiring.center R) ≃+* ↥(Subsemiring.center S)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) ((algebraMap R K) r) = 1 ↔ r ∉ v.asIdeal
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.of_ringEquiv_left : ∀ {R : Type u_6} [inst : CommSemiring R] {S : Type u_7} [inst_1 : CommSemiring S] {K : Type u_8}
  [inst_2 : CommSemiring K] [inst_3 : Algebra R K] (e : R ≃+* S) [inst_4 : Algebra S K],
  (∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)) → ∀ [IsFractionRing S K], IsFractionRing R K
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.lift_of : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : Semiring P] [inst_10 : Algebra R P] (g : (i : ι) → G i →ₐ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i),
  (DirectLimit.Algebra.lift G f P g Hg) ((DirectLimit.Algebra.of G f i) x) = (g i) x
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctorLeft_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (X : C), (CategoryTheory.Join.mkFunctorLeft F G α).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhdsLeft : ∀ (a : ℝ), intervalIntegral.FTCFilter a (nhdsWithin a (Set.Iic a)) (nhdsWithin a (Set.Iic a))
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `... ⊢ₛ ...⌝` syntax from applications of `SPred.entails`.
 -/
Std.Do.SPred.Notation.unexpandEntails : Lean.PrettyPrinter.Unexpander
-- Lean.Structure
Lean.getProjFnForField? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Data.SetLike.Basic
/-- **Alias** of the forward direction of `SetLike.le_def`. -/
mem_of_le_of_mem : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : LE A] [IsConcreteLE A B] {S T : A},
  S ≤ T → ∀ ⦃x : B⦄, x ∈ S → x ∈ T
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.rotateL_lemma₂ : ∀ {a b c : ℕ}, 2 * (b + c) ≤ 9 * a + 3 → b < 2 * c → b < 3 * a + 1
-- Mathlib.Topology.MetricSpace.HausdorffDimension
AntilipschitzWith.dimH_preimage_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
  AntilipschitzWith K f → ∀ (s : Set Y), dimH (f ⁻¹' s) ≤ dimH s
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.symExtensionsRef : IO.Ref (Array (Lean.Meta.Sym.SymExtension Lean.Meta.Sym.SymExtensionState))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_one_eq_singleton : (*...1).toList = [0]
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The `MulHom` from the preimage of a subsemigroup to itself.  -/
MulHom.subsemigroupComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → (N' : Subsemigroup N) → ↥(Subsemigroup.comap f N') →ₙ* ↥N'
-- Init.Data.List.Lex
List.not_lt_of_cons_le_cons : ∀ {α : Type u_1} [inst : LT α] [i₁ : Std.Asymm fun x1 x2 => x1 < x2] [i₂ : Std.Trichotomous fun x1 x2 => x1 < x2]
  {a b : α} {l₁ l₂ : List α}, a :: l₁ ≤ b :: l₂ → ¬b < a
-- Mathlib.Order.Hom.Lattice
SupHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Max α] [inst_1 : Max β] [inst_2 : FunLike F α β],
  (∀ (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b) → SupHomClass F α β
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- Whether the two suggestions are duplicates of each other.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.isDuplicate : Mathlib.Tactic.ClickSuggestions.ApplyAtKey → Mathlib.Tactic.ClickSuggestions.ApplyAtKey → Lean.MetaM Bool
-- Init.Data.SInt.Bitwise
Bool.toBitVec_toInt16 : ∀ {b : Bool}, b.toInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.isZero_of_hasInjectiveDimensionLT_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  [CategoryTheory.HasInjectiveDimensionLT X 0], CategoryTheory.Limits.IsZero X
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_neg`. -/
ContinuousLinearMap.coe_neg : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂]
  (f : M →SL[σ₁₂] M₂), ↑(-f) = -↑f
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.rank_of_bijective_algebraMap : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [StrongRankCondition R], Function.Bijective ⇑(algebraMap R S) → Module.rank R S = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleEquiv h =
    {
      toFun := fun α =>
        CategoryTheory.CategoryStruct.comp (α.v p q h) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom,
      invFun := fun f => CochainComplex.HomComplex.Cochain.toSingleMk f h, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.lieQuotientLieAlgebra : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → LieAlgebra R (L ⧸ I)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : Cᵒᵖ} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g → CategoryTheory.IsPushout g.unop f.unop snd.unop fst.unop
-- Mathlib.Logic.Equiv.Fintype
/-- Any two same-cardinality finsets are related by a permutation.  -/
Equiv.Perm.exists_map_finset_eq : ∀ {β : Type u_2} (s t : Finset β), s.card = t.card → ∃ σ, Finset.map (Equiv.toEmbedding σ) s = t
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
hasDerivAt_of_tendstoUniformlyOn : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g : 𝕜 → G} {f' : ι → 𝕜 → G} {g' : 𝕜 → G}
  {x : 𝕜} [IsRCLikeNormedField 𝕜] [l.NeBot] {s : Set 𝕜},
  IsOpen s →
    TendstoUniformlyOn f' g' l s →
      (∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasDerivAt g (g' x) x
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_eq_filter_Icc_two : ∀ (n : ℕ), n.primesLE = Finset.filter Nat.Prime (Finset.Icc 2 n)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- Auxiliary definition for `IsType₂.simplex`. This gives the underlying
data of the type (I) simplex reconstructed from a type (II) simplex.  -/
SSet.prodStdSimplex.pairingCore.IsType₂.φ : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) →
        {d : ℕ} → x.dim = d → Fin (d + 2) → Fin (m + 2) × Fin (n + 1)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_image_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set M),
  ⇑h.symm '' ⇑h '' s = s
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-open right-closed range as a list in ascending order.
 -/
Std.Roc.toList : {α : Type u} →
  [inst : LE α] →
    [DecidableLE α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxc.IsAlwaysFinite α] → Std.Roc α → List α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.keyAtIdx?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.Equiv t₂ → t₁.keyAtIdx? i = t₂.keyAtIdx? i
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.smul_eq_zero_of_mem : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, ∀ p ∈ P.ker, ∀ (m : P.ker.Cotangent), p • m = 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.compl_inf : ∀ {α : Type u_2} {ι : Type u_5} [inst : BooleanAlgebra α] (s : Finset ι) (f : ι → α), (s.inf f)ᶜ = s.sup fun i => (f i)ᶜ
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_const : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal),
  (μ.withDensity fun x => c) = c • μ
-- Mathlib.Topology.Covering.Quotient
isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd : ∀ {E : Type u_1} [inst : TopologicalSpace E] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G E]
  [ContinuousConstVAdd G E] [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E],
  IsCoveringMapOn (Quotient.mk (AddAction.orbitRel G E))
    (Quotient.mk (AddAction.orbitRel G E) '' {e | AddAction.stabilizer G e = ⊥})
-- Mathlib.Order.BooleanAlgebra.Defs
GeneralizedBooleanAlgebra.mk : {α : Type u} →
  [toDistribLattice : DistribLattice α] →
    [toSDiff : SDiff α] →
      [toBot : Bot α] →
        (∀ (a b : α), a ⊓ b ⊔ a \ b = a) → (∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥) → GeneralizedBooleanAlgebra α
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.charpoly = M.charmatrix.det
-- Mathlib.Tactic.Translate.Reorder
/-- Permute the array using a sequence of indices defining a cyclic permutation.
If the list of indices `l = [i₁, i₂, ..., iₙ]` are all distinct then
`(cyclicPermute! a l)[iₖ₊₁] = a[iₖ]` and `(cyclicPermute! a l)[i₀] = a[iₙ]`  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.Permutation.permute!.cyclicPermute! : {α : Type u_1} → [Inhabited α] → Array α → List ℕ → Array α
-- Mathlib.Topology.Path
/-- Casting a path from `x` to `y` to a path from `x'` to `y'` when `x' = x` and `y' = y`  -/
Path.cast : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Path x y → {x' y' : X} → x' = x → y' = y → Path x' y'
-- Mathlib.Data.ULift
ULift.map_injective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective (ULift.map f) ↔ Function.Injective f
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edge_le_iff : ∀ {V : Type u_1} (G : SimpleGraph V) {v w : V}, SimpleGraph.edge v w ≤ G ↔ v = w ∨ G.Adj v w
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.Gamma_eq_GammaAux : ∀ (s : ℂ) (n : ℕ), -s.re < ↑n → Complex.Gamma s = Complex.GammaAux✝ n s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instSMulCommClass : ∀ {S : Type u_1} {T : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Monoid S]
  [inst_6 : Monoid T] [inst_7 : DistribMulAction S N] [inst_8 : DistribMulAction T N] [inst_9 : SMulCommClass S R N]
  [inst_10 : SMulCommClass T R N] [SMulCommClass S T N], SMulCommClass S T (QuadraticMap R M N)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_comp_coe_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), (↑e).comp ↑e.symm = ContinuousAlgHom.id R B
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.card_le_beth : ∀ (o : Ordinal.{u_1}), o.card ≤ Cardinal.beth o
-- Mathlib.Combinatorics.Hindman
Hindman.exists_idempotent_ultrafilter_le_FS : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M), ∃ U, U + U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ Hindman.FS a
-- Mathlib.Data.NNReal.Defs
Real.le_coe_toNNReal : ∀ (r : ℝ), r ≤ ↑r.toNNReal
-- Init.Data.UInt.Lemmas
UInt16.div_self : ∀ {a : UInt16}, a / a = if a = 0 then 0 else 1
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.hom_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C}
  (m : W ⟶ t.pt),
  m = h.lift { pt := W, π := { app := fun b => CategoryTheory.CategoryStruct.comp m (t.π.app b), naturality := ⋯ } }
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhdsWithin_top : nhdsWithin ⊤ {⊤}ᶜ = Filter.map Real.toEReal Filter.atTop
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint of the composition of two operators is the composition of the two adjoints
in reverse order.  -/
ContinuousLinearMap.adjoint_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 E]
  [inst_5 : InnerProductSpace 𝕜 F] [inst_6 : InnerProductSpace 𝕜 G] [inst_7 : CompleteSpace E]
  [inst_8 : CompleteSpace G] [inst_9 : CompleteSpace F] (A : F →L[𝕜] G) (B : E →L[𝕜] F),
  ContinuousLinearMap.adjoint (A ∘SL B) = ContinuousLinearMap.adjoint B ∘SL ContinuousLinearMap.adjoint A
-- Mathlib.Topology.Order
generateFrom_union_isOpen : ∀ {α : Type u} (a b : TopologicalSpace α), TopologicalSpace.generateFrom ({s | IsOpen s} ∪ {s | IsOpen s}) = a ⊓ b
-- Mathlib.GroupTheory.Perm.DomMulAct
/-- The `invFun` component of `MulEquiv` from `MulAction.stabilizer (Perm α) p`
to the product of the `Equiv.Perm {a | f a = i}` (as an `Equiv.Perm α`).  -/
DomMulAct.stabilizerEquiv_invFun_aux : {α : Type u_1} → {ι : Type u_2} → {f : α → ι} → ((i : ι) → Equiv.Perm { a // f a = i }) → Equiv.Perm α
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonnegg.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((a b : ℕ) → motive (Int.ofNat a) (Int.ofNat b)) →
      ((a b : ℕ) → motive (Int.ofNat a) (Int.negSucc b)) →
        ((a b : ℕ) → motive (Int.negSucc a) (Int.ofNat b)) →
          ((a a_1 : ℕ) → motive (Int.negSucc a) (Int.negSucc a_1)) → motive x x_1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_one : CategoryTheory.Limits.walkingParallelPairOpEquiv.unitIso.app CategoryTheory.Limits.WalkingParallelPair.one =
  CategoryTheory.Iso.refl CategoryTheory.Limits.WalkingParallelPair.one
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instOne : {α : Type u_1} → [CommGroup α] → [inst : Preorder α] → One (UpperSet α)
-- Mathlib.Topology.Algebra.Module.PerfectPairing
/-- Turn a continuous perfect pairing between `M` and `N` into a map from `M` to continuous linear
maps `N → R`.  -/
LinearMap.toContPerfPair : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : TopologicalSpace R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : TopologicalSpace M] →
                [inst_5 : AddCommGroup N] →
                  [inst_6 : Module R N] →
                    [inst_7 : TopologicalSpace N] →
                      (p : M →ₗ[R] N →ₗ[R] R) →
                        [p.IsContPerfPair] → [inst_9 : IsTopologicalRing R] → M ≃ₗ[R] StrongDual R N
-- Lean.Meta.Instances
Lean.Meta.registerInstance : Lean.Name → Lean.AttributeKind → ℕ → Lean.MetaM Unit
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_pos_mul_lt : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ 0 → ∃ c, 0 < c ∧ c * a < b