mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanAlgebra.Basic
himp_eq_left : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Reinterpret a ring homomorphism `f : α →+* β` as a non-unital ring homomorphism `α →ₙ+* β`. The
`simp`-normal form is `(f : α →ₙ+* β)`.  -/
RingHom.toNonUnitalRingHom : {α : Type u_5} → {β : Type u_6} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →ₙ+* β
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_inj : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] (i : ι) {x y : M i},
  Pi.single i x = Pi.single i y ↔ x = y
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y),
  CategoryTheory.WithTerminal.prelaxfunctor.map F = (CategoryTheory.WithTerminal.map F.toFunctor).toCatHom
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- If `f` has temperate growth, then its `n`-th iterated derivative is `O((1 + ‖x‖) ^ k)` for
some `k : ℕ` (depending on `n`).

Note that the `O` here is with respect to the `⊤` filter, meaning that the bound holds everywhere.
 -/
Function.HasTemperateGrowth.isBigO : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F},
  Function.HasTemperateGrowth f → ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x => (1 + ‖x‖) ^ k
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- A simplicial object that is isomorphic to a split simplicial object is split.  -/
CategoryTheory.SimplicialObject.Splitting.ofIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : CategoryTheory.SimplicialObject C} → X.Splitting → (X ≅ Y) → Y.Splitting
-- Mathlib.Data.Nat.Factorial.Basic
Nat.pow_succ_le_ascFactorial : ∀ (n k : ℕ), n ^ k ≤ n.ascFactorial k
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.toDigitsCore.eq_2 : ∀ (base x : ℕ) (x_1 : List Char) (fuel : ℕ),
  base.toDigitsCore fuel.succ x x_1 =
    if x / base = 0 then (x % base).digitChar :: x_1
    else base.toDigitsCore fuel (x / base) ((x % base).digitChar :: x_1)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A family of maps with the same target can be turned into one arrow in the category of formal
coproducts. This is used in Čech cohomology.  -/
CategoryTheory.Limits.FormalCoproduct.homOfPiHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      {J : Type w} →
        (f : J → C) →
          ((j : J) → f j ⟶ X) → ({ I := J, obj := f } ⟶ (CategoryTheory.Limits.FormalCoproduct.incl C).obj X)
-- Mathlib.Data.Finset.Basic
Finset.toList_eq_nil : ∀ {α : Type u_1} {s : Finset α}, s.toList = [] ↔ s = ∅
-- Aesop.Forward.State
Aesop.InstMap.instEmptyCollection : EmptyCollection Aesop.InstMap
-- Init.Data.SInt.Bitwise
Int32.not_and_self : ∀ {a : Int32}, ~~~a &&& a = 0
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A normed commutative ring is a seminormed commutative ring.  -/
NormedCommRing.toSeminormedCommRing : {α : Type u_2} → [β : NormedCommRing α] → SeminormedCommRing α
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- If a function `ℤ² → ℂ` is `O (‖n‖ ^ a)⁻¹` for `2 < a`, then the function is summable.  -/
EisensteinSeries.summable_of_isBigO_rpow_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [CompleteSpace E] {f : (Fin 2 → ℤ) → E} {a : ℝ},
  2 < a → (f =O[Filter.cofinite] fun n => (‖n‖ ^ a)⁻¹) → Summable f
-- Init.Data.Nat.Basic
Nat.ne_of_lt' : ∀ {a b : ℕ}, a < b → b ≠ a
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.isDomain : ∀ {R : Type u_3} [inst : Ring R] (I : Ideal R) [inst_1 : I.IsTwoSided] [hI : I.IsPrime], IsDomain (R ⧸ I)
-- Std.Data.Iterators.Combinators.Monadic.Drop
/-- Given an iterator `it` and a natural number `n`, `it.drop n` is an iterator that forwards all of
`it`'s output values except for the first `n`.

**Marble diagram:**

```text
it          ---a----b---c--d-e--⊥
it.drop 3   ---------------d-e--⊥

it          ---a--⊥
it.drop 3   ------⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

**Performance:**

Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator
does not drop any elements anymore.
 -/
Std.IterM.drop : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → ℕ → Std.IterM m β → Std.IterM m β
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.Array.toListLitAux.match_1.eq_1 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → List α → Sort u_2) (x : 0 ≤ xs.size) (acc : List α)
  (h_1 : (x : 0 ≤ xs.size) → (acc : List α) → motive 0 x acc)
  (h_2 : (i : ℕ) → (hi : i + 1 ≤ xs.size) → (acc : List α) → motive i.succ hi acc),
  (match 0, x, acc with
    | 0, x, acc => h_1 x acc
    | i.succ, hi, acc => h_2 i hi acc) =
    h_1 x acc
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_true : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] (f : Filter β) (u : β → α),
  (Filter.bliminf u f fun x => True) = Filter.liminf u f
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffOn.clm_precomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₁ →L[𝕜] F₂}
  {s : Set M},
  ContMDiffOn I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₂)) n f s →
    ContMDiffOn I (modelWithCornersSelf 𝕜 ((F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃)) n
      (fun y => ContinuousLinearMap.precomp F₃ (f y)) s
-- Mathlib.CategoryTheory.Action.Basic
Action.resEquiv_inverse : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G ≃* H), (Action.resEquiv V f).inverse = Action.res V ↑f.symm
-- Mathlib.Order.KrullDimension
Order.coheight_pos_of_lt_top : ∀ {α : Type u_1} [inst : Preorder α] {x : α} [inst_1 : OrderTop α], x < ⊤ → 0 < Order.coheight x
-- Mathlib.Topology.Bornology.BoundedOperation
BoundedAdd.isBounded_add : ∀ {R : Type u_1} {inst : Bornology R} {inst_1 : Add R} [self : BoundedAdd R] {s t : Set R},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)
-- Lean.Data.Position
Lean.String.toFileMap : String → Lean.FileMap
-- Init.Data.Float.Model.Format.Basic
/-- Specification corresponding to the IEEE `binary64` format.  -/
Float.Model.Format.binary64 : Float.Model.Format
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.MapSubtype.orderIso_symm_apply : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (sH' : { H' // H' ≤ H }),
  (Subgroup.MapSubtype.orderIso H).symm sH' = (↑sH').subgroupOf H
-- Mathlib.Data.DFinsupp.Interval
/-- When `t` is supported on `s`, `f ∈ s.dfinsupp t` precisely means that `f` is pointwise in `t`.
 -/
Finset.mem_dfinsupp_iff_of_support_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)] {s : Finset ι}
  {f : Π₀ (i : ι), α i} [inst_2 : (i : ι) → DecidableEq (α i)] {t : Π₀ (i : ι), Finset (α i)},
  t.support ⊆ s → (f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Ici_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioc a b ⊆ Finset.Ici a
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.compl : ∀ {α : Type u_2} {𝒜 : Set (Set α)} (s : Set α),
  MeasureTheory.generateSetAlgebra 𝒜 s → MeasureTheory.generateSetAlgebra 𝒜 sᶜ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.eq.injEq : ∀ (x y p x_1 y_1 p_1 : Lean.Expr),
  (Nat.EqResult.eq✝ x y p = Nat.EqResult.eq✝ x_1 y_1 p_1) = (x = x_1 ∧ y = y_1 ∧ p = p_1)
-- Mathlib.Data.Set.Lattice
Set.biInter_mono : ∀ {α : Type u_1} {β : Type u_2} {s s' : Set α} {t t' : α → Set β},
  s ⊆ s' → (∀ x ∈ s, t x ⊆ t' x) → ⋂ x ∈ s', t x ⊆ ⋂ x ∈ s, t' x
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.complexEmbedding_injective : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ), Function.Injective ⇑(NumberField.Units.complexEmbedding φ)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_const_beq_const : ∀ {w b c : ℕ} {a : BitVec w}, (a + BitVec.ofNat w b == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [CategoryTheory.Limits.HasPullbacks C], P.HasPullbacks
-- Mathlib.Analysis.Calculus.FDeriv.Comp
Differentiable.comp_differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} {g : F → G},
  Differentiable 𝕜 g → DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (g ∘ f) s
-- Mathlib.Algebra.Star.StarAlgHom
/-- Construct a star algebra equivalence from a pair of star algebra homomorphisms.  -/
StarAlgEquiv.ofStarAlgHom : {R : Type u_8} →
  {A : Type u_9} →
    {B : Type u_10} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] →
                [inst_5 : Algebra R B] →
                  [inst_6 : Star B] →
                    (f : A →⋆ₐ[R] B) →
                      (g : B →⋆ₐ[R] A) → g.comp f = StarAlgHom.id R A → f.comp g = StarAlgHom.id R B → A ≃⋆ₐ[R] B
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_zpow : ∀ {ι : Type u_2} {G : Type u_4} [inst : DivisionCommMonoid G] {m : Multiset ι} {f : ι → G} {n : ℤ},
  (Multiset.map (fun i => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
gelfandStarTransform_apply_apply : ∀ (A : Type u_1) [inst : CommCStarAlgebra A] (a : A) (φ : ↑(WeakDual.characterSpace ℂ A)),
  ((gelfandStarTransform A) a) φ = φ a
-- Init.Data.List.Control
List.flatMapM.loop : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (List β)) → List α → List (List β) → m (List β)
-- Mathlib.Order.Filter.Partial
Filter.rcomap_sets : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (f : Filter β),
  (Filter.rcomap r f).sets = SetRel.image {(s, t) | r.core s ⊆ t} f.sets
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_signSet_apply_isReal : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : { w // w.IsReal }),
  ((NumberField.mixedEmbedding.negAt (NumberField.mixedEmbedding.signSet x)) x).1 w = ‖x.1 w‖
-- Mathlib.Algebra.Group.Invertible.Defs
mul_right_inj_of_invertible : ∀ {α : Type u} [inst : Monoid α] {a b : α} (c : α) [Invertible c], c * a = c * b ↔ a = b
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.homObjEquiv_apply_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G A : CategoryTheory.Functor C (Type w)) (a : F.HomObj G A)
  (X : C),
  ((F.homObjEquiv G A) a).app X =
    TypeCat.ofHom fun x =>
      match x with
      | (x, y) => (CategoryTheory.ConcreteCategory.hom (a.app X y)) x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.mk.sizeOf_spec : ∀ (nextDeclIdx : ℕ) (enodeMap : Lean.Meta.Grind.ENodeMap) (exprs : Lean.PArray Lean.Expr)
  (parents : Lean.Meta.Grind.ParentMap) (congrTable : Lean.Meta.Grind.CongrTable enodeMap)
  (appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (indicesFound : Lean.PHashSet Lean.HeadIndex)
  (newFacts : Array Lean.Meta.Grind.NewFact) (inconsistent : Bool) (nextIdx : ℕ)
  (newRawFacts : Std.Queue Lean.Meta.Grind.NewRawFact) (facts : Lean.PArray Lean.Expr)
  (extThms : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem))
  (ematch : Lean.Meta.Grind.EMatch.State) (inj : Lean.Meta.Grind.Injective.State) (split : Lean.Meta.Grind.Split.State)
  (clean : Lean.Meta.Grind.Clean.State) (sstates : Array Lean.Meta.Grind.SolverExtensionState),
  sizeOf
      { nextDeclIdx := nextDeclIdx, enodeMap := enodeMap, exprs := exprs, parents := parents, congrTable := congrTable,
        appMap := appMap, indicesFound := indicesFound, newFacts := newFacts, inconsistent := inconsistent,
        nextIdx := nextIdx, newRawFacts := newRawFacts, facts := facts, extThms := extThms, ematch := ematch,
        inj := inj, split := split, clean := clean, sstates := sstates } =
    1 + sizeOf nextDeclIdx + sizeOf enodeMap + sizeOf exprs + sizeOf parents + sizeOf congrTable + sizeOf appMap +
                            sizeOf indicesFound +
                          sizeOf newFacts +
                        sizeOf inconsistent +
                      sizeOf nextIdx +
                    sizeOf newRawFacts +
                  sizeOf facts +
                sizeOf extThms +
              sizeOf ematch +
            sizeOf inj +
          sizeOf split +
        sizeOf clean +
      sizeOf sstates
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache : Type u → Std.Sat.AIG Std.Tactic.BVDecide.BVBit → Type u
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.Y_eq_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ → W.Equation x₂ y₂ → x₁ = x₂ → y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
-- Std.Time.Zoned.TimeZone
Std.Time.instInhabitedTimeZone : Inhabited Std.Time.TimeZone
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.const_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (b : β) (a : α),
  (ContinuousMap.const α b) a = b
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Pseudofunctor.StrongTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Pseudofunctor.StrongTrans.isoMk app naturality).hom.as.app a = (app a).hom
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.neg_comp_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp (-f) (-g) = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Logic.Equiv.Defs
/-- `ULift α` is equivalent to `α`.  -/
Equiv.ulift : {α : Type v} → ULift.{u, v} α ≃ α
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.foldr : {α : Type u} → {β : α → Type v} → {δ : Type w} → ((a : α) → β a → δ → δ) → δ → Std.DHashMap.Internal.AssocList α β → δ
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instSetLike : {K : Type u} → [inst : DivisionRing K] → SetLike (Subfield K) K
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.id_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (a : E.I₀),
  (CategoryTheory.CategoryStruct.id E).s₀ a = a
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflection is its own inverse.  -/
EuclideanGeometry.reflection_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  (EuclideanGeometry.reflection s).symm = EuclideanGeometry.reflection s
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.functor_obj_obj : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (M : Action V G)
  (x : CategoryTheory.SingleObj G), (Action.FunctorCategoryEquivalence.functor.obj M).obj x = M.V
-- Mathlib.Algebra.Group.Center
/-- The center of a magma.  -/
Set.center : (M : Type u_1) → [Mul M] → Set M
-- Init.Data.ToString.Name
_private.Init.Data.ToString.Name.0.Lean.Name.escape : String → String
-- Mathlib.RepresentationTheory.Invariants
Representation.toInvariants.congr_simp : ∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Group G] {V : Type u_5} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal],
  ρ.toInvariants S = ρ.toInvariants S
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' →
    Std.DHashMap.Const.get? (Std.DHashMap.filterMap f m) k = (Std.DHashMap.Const.get? m k).bind (f k')
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.headerTimeout : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Option Std.Time.Timestamp
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toNontrivial : ∀ {G₀ : Type u} [self : GroupWithZero G₀], Nontrivial G₀
-- Mathlib.Tactic.DefEqAbuse
/-- Collect rendered check strings from `Meta.isDefEq` trace nodes matching a status predicate.
Returns a `HashSet` of header strings.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.collectIsDefEqChecks : (Lean.TraceResult → Bool) → Lean.MessageData → BaseIO (Std.HashSet String)
-- Mathlib.Data.Finset.Prod
Finset.product_subset_product_right : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β}, t ⊆ t' → s ×ˢ t ⊆ s ×ˢ t'
-- Lean.Elab.DocString
Lean.Doc.SuggestionMode.interactive.sizeOf_spec : sizeOf Lean.Doc.SuggestionMode.interactive = 1
-- Mathlib.Order.Notation
Top.ext_iff : ∀ {α : Type u_1} {x y : Top α}, x = y ↔ ⊤ = ⊤
-- Lean.Meta.TransparencyMode
Lean.Meta.TransparencyMode.instHashable_lean : Hashable Lean.Meta.TransparencyMode
-- Mathlib.Order.Sublattice
Sublattice.instPartialOrder : {α : Type u_2} → [inst : Lattice α] → PartialOrder (Sublattice α)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Collects all singleton patterns in the type of the given proof.
We use this function to implement local forall expressions in a `grind` goal.
 -/
Lean.Meta.Grind.mkEMatchTheoremUsingSingletonPatterns : Lean.Meta.Grind.Origin →
  Array Lean.Name →
    Lean.Expr →
      ℕ → Lean.Meta.Grind.SymbolPriorities → optParam Bool false → Lean.MetaM (Array Lean.Meta.Grind.EMatchTheorem)
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.eq_1 : ∀ {α : Type u_1} [inst : LT α] (a : α), Order.IsSuccPrelimit a = ∀ (b : α), ¬b ⋖ a
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Config.mk.injEq : ∀ (maxTransitionDepth maxSteps maxTransitionDepth_1 maxSteps_1 : ℕ),
  ({ maxTransitionDepth := maxTransitionDepth, maxSteps := maxSteps } =
      { maxTransitionDepth := maxTransitionDepth_1, maxSteps := maxSteps_1 }) =
    (maxTransitionDepth = maxTransitionDepth_1 ∧ maxSteps = maxSteps_1)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 0 = 0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_add_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Add Z] [inst_4 : ContinuousAdd Z] (f g : C(X × Y, Z)) (x : X),
  (f + g).curry x = f.curry x + g.curry x
-- Lean.Server.RequestCancellation
Lean.Server.MonadCancellable.checkCancelled : {m : Type → Type v} → [self : Lean.Server.MonadCancellable m] → m PUnit.{1}
-- Mathlib.Algebra.Order.Sub.Basic
tsub_add_cancel_iff_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, b - a + a = b ↔ a ≤ b
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment : BEq Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.monic_minpoly : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  (c : ConjRootClass K L), c.minpoly.Monic
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
 -/
Lean.Elab.Term.TermElabM.parIterGreedy : {α : Type} →
  List (Lean.Elab.TermElabM α) → Lean.Elab.TermElabM (Std.IterM Lean.Elab.TermElabM (Except Lean.Exception α))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff! m₂).getKey! k = default
-- Init.Control.Lawful.Instances
instLawfulMonadStateRefT' : ∀ {m : Type → Type} {ω σ : Type} [inst : Monad m] [LawfulMonad m], LawfulMonad (StateRefT' ω σ m)
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.coordChange : {ι : Type u_5} →
  {B : Type u_6} →
    [inst : TopologicalSpace B] →
      {F : Type u_7} → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → ι → ι → B → F → F
-- Mathlib.Data.Finite.Defs
Set.finite_coe_iff : ∀ {α : Type u} {s : Set α}, Finite ↑s ↔ s.Finite
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulated.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [toContainsZero : P.ContainsZero]
  [toIsStableUnderShift : P.IsStableUnderShift ℤ] [toIsTriangulatedClosed₂ : P.IsTriangulatedClosed₂], P.IsTriangulated
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_injective : Function.Injective ENNReal.toEReal
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict.eq_1 : ∀ {α : Type u_1} (s : Set α),
  MeasureTheory.OuterMeasure.restrict s =
    MeasureTheory.OuterMeasure.map Subtype.val ∘ₗ MeasureTheory.OuterMeasure.comap Subtype.val