mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The equivalence of categories between `TopRep k G` and `Action (TopModuleCat k) G`.  -/
TopRep.TopRepEquivActionTop : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] → [inst_1 : Ring k] → [inst_2 : Monoid G] → TopRep k G ≌ Action (TopModuleCat k) G
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.mk.sizeOf_spec : ∀ (elimExpr elimType : Lean.Expr) (motivePos : ℕ) (targetsPos : Array ℕ) (altsInfo : Array Lean.Meta.ElimAltInfo)
  (numComplexMotiveArgs : ℕ),
  sizeOf
      { elimExpr := elimExpr, elimType := elimType, motivePos := motivePos, targetsPos := targetsPos,
        altsInfo := altsInfo, numComplexMotiveArgs := numComplexMotiveArgs } =
    1 + sizeOf elimExpr + sizeOf elimType + sizeOf motivePos + sizeOf targetsPos + sizeOf altsInfo +
      sizeOf numComplexMotiveArgs
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.hom_ext_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F] {X : C}
  {f g : X ⟶ CategoryTheory.Limits.end_ F},
  f = g ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.end_.π F j) =
        CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.end_.π F j)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.error : Lean.Lsp.DiagnosticSeverity
-- Std.Http.Internal.LowerCase
Std.Http.Internal.IsLowerCase.eq_1 : ∀ (s : String), Std.Http.Internal.IsLowerCase s = (s.toLower = s)
-- Mathlib.Data.Set.PowersetCard
/-- The type of combinations of `n` elements of a type `α`.

See also `Finset.powersetCard`.  -/
Set.powersetCard : (α : Type u_1) → ℕ → Set (Finset α)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
MeasureTheory.VectorMeasure.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Std.Sat.AIG.Basic
_private.Std.Sat.AIG.Basic.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1)
  (h_1 : Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_1 ⋯
-- Mathlib.GroupTheory.Congruence.Defs
/-- There exists an element of the quotient of a monoid by a congruence relation (namely 1).  -/
Con.Quotient.inhabited : {M : Type u_1} → [inst : Mul M] → [One M] → {c : Con M} → Inhabited c.Quotient
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularEpi.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C] (W : C)
  (left right : W ⟶ X)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp left f = CategoryTheory.CategoryStruct.comp right f)
      CategoryTheory.RegularEpi.w._autoParam)
  (isColimit : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f w)),
  sizeOf { W := W, left := left, right := right, w := w, isColimit := isColimit } =
    1 + sizeOf W + sizeOf left + sizeOf right + sizeOf w + sizeOf isColimit
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Raw.Const.insertMany t l).getKey! k = t.getKey! k
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.hasSum_orthogonalProjectionOnto : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [inst_3 : CompleteSpace ↥U] (b : HilbertBasis ι 𝕜 ↥U) (x : E),
  HasSum (fun i => inner 𝕜 (↑(b i)) x • b i) (U.orthogonalProjectionOnto x)
-- Init.Data.Vector.Basic
_private.Init.Data.Vector.Basic.0.Vector.mapM.go : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} → {n : ℕ} → [Monad m] → (α → m β) → Vector α n → (k : ℕ) → k ≤ n → Vector β k → m (Vector β n)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew!_eq_foldl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β},
  ↑(t.insertManyIfNew! l) =
    List.foldl
      (fun acc x_1 =>
        match x_1 with
        | ⟨k, v⟩ => Std.DTreeMap.Internal.Impl.insertIfNew! k v acc)
      t l
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.LaxFunctor.bicategory_whiskerLeft_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (η : x ⟶ x_1) (x_3 x_4 : x_1 ⟶ x_2) (Γ : x_3 ⟶ x_4) (a : B),
  (CategoryTheory.Bicategory.whiskerLeft η Γ).as.app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.Topology.Algebra.Group.Basic
continuousNeg_inf : ∀ {G : Type w} [inst : Neg G] {t₁ t₂ : TopologicalSpace G}, ContinuousNeg G → ContinuousNeg G → ContinuousNeg G
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAddMonoidMorphism.toAddMonoidHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {H' : Type u_5} →
                [inst_4 : TopologicalSpace H'] →
                  {E' : Type u_6} →
                    [inst_5 : NormedAddCommGroup E'] →
                      [inst_6 : NormedSpace 𝕜 E'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {n : WithTop ℕ∞} →
                              {G : Type u_8} →
                                [inst_7 : TopologicalSpace G] →
                                  [inst_8 : ChartedSpace H G] →
                                    [inst_9 : AddMonoid G] →
                                      {G' : Type u_9} →
                                        [inst_10 : TopologicalSpace G'] →
                                          [inst_11 : ChartedSpace H' G'] →
                                            [inst_12 : AddMonoid G'] → ContMDiffAddMonoidMorphism I I' n G G' → G →+ G'
-- Mathlib.RepresentationTheory.Invariants
/-- The subspace of invariants, consisting of the vectors fixed by all elements of `G`.
 -/
Representation.invariants : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] → [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → Representation k G V → Submodule k V
-- Mathlib.Order.Filter.Map
Filter.map_iInf_eq : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → Filter α} {m : α → β},
  Directed (fun x1 x2 => x1 ≥ x2) f → ∀ [Nonempty ι], Filter.map m (iInf f) = ⨅ i, Filter.map m (f i)
-- Std.Http.Data.Request
/-- The main parts of a request containing the HTTP method, version, and request target URI.

Reference: https://httpwg.org/specs/rfc9112.html#request.line
 -/
Std.Http.Request.Head : Type
-- Aesop.Script.Step
Aesop.Script.Step : Type
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
instInhabitedAlgebraNorm : (K : Type u_1) → [inst : NormedField K] → Inhabited (AlgebraNorm K K)
-- Init.Data.Vector.Lemmas
Vector.toList_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α}, (Vector.replicate n a).toList = List.replicate n a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.getThenInsertIfNew? k v).1 = t[k]?
-- Mathlib.Algebra.GradedMonoid
/-- A tactic to for use as an optional value for `GMonoid.gnpow_succ'`.  -/
GradedMonoid.tacticApply_gmonoid_gnpowRec_succ_tac : Lean.ParserDescr
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_mul' : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s : Set α) (f g : α → M),
  s.mulIndicator (f * g) = s.mulIndicator f * s.mulIndicator g
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- **Alias** of `IsLocalization.AtPrime.under_map_of_isMaximal`. -/
IsLocalization.AtPrime.comap_map_of_isMaximal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Sₚ : Type u_5) [inst_4 : CommSemiring Sₚ] [inst_5 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsMaximal] [P.LiesOver p],
  Ideal.under S (Ideal.map (algebraMap S Sₚ) P) = P
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.Monadic.isPlausibleOutput_iff : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {it : Std.IterM Id α}, it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a < it.internalState.upperBound
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAt_eq_self_of_lt : ∀ {N i : ℕ}, N < i → (Polynomial.revAt N) i = i
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_neg_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R (-2) = -1
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.splits_rotateLeft : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃), h.rotateLeft.Splits t₁ (t₂ ++ t₃)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzWith.locallyBoundedVariationOn : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {C : NNReal},
  LipschitzWith C f → ∀ (s : Set ℝ), LocallyBoundedVariationOn f s
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_1.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_limZero_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv) {g : CauSeq β abv},
  g.LimZero → (f * g).LimZero
-- Mathlib.Data.Nat.Dist
Nat.dist_add_add_right : ∀ (n k m : ℕ), (n + k).dist (m + k) = n.dist m
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.unbox.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_23} {fvarId_1 : Lean.FVarId}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_23},
  Lean.Compiler.LCNF.LetValue.unbox fvarId h = Lean.Compiler.LCNF.LetValue.unbox fvarId_1 h_1 → fvarId = fvarId_1
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.setLike : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] → [inst_5 : GradedRing 𝒜] → SetLike (HomogeneousIdeal 𝒜) A
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {G : Type u_2} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G} {u : 𝕜 → F} {u' : F},
  HasDerivAt c c' x → HasDerivAt u u' x → HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.exists_smul_of_last_eq : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ}
  (a : α) (x : Fin n.succ ↪ α), ∃ g y, g • x = SubMulAction.ofStabilizer.snoc y
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_pow : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V) (m : ℕ), ↑(A ^ m) = ↑A ^ m
-- Init.Control.Lawful.MonadAttach.Instances
StateT.run.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ), x.run s = x s
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
  (N : ι) (n : ℕ) (ω : Ω),
  MeasureTheory.lowerCrossingTime a b f N n ω =
    MeasureTheory.hittingBtwn f (Set.Iic a) (MeasureTheory.upperCrossingTime a b f N n ω) N ω
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.unopUnop_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ),
  (CategoryTheory.unopUnop C).obj X = Opposite.unop (Opposite.unop X)
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_sub : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a - b).imJ = a.imJ - b.imJ
-- Init.Grind.Interactive
/-- `grind` is the syntax category for a "grind interactive tactic".
A `grind` tactic is a program which receives a `grind` goal.  -/
Lean.Parser.Category.grind : Lean.Parser.Category
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
aemeasurable_of_tendsto_metrizable_ae' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure α}
  {f : ℕ → α → β} {g : α → β},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) → AEMeasurable g μ
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_le_iff_degree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n ↔ p.degree ≤ ↑n
-- Std.Data.HashSet.Basic
/-- Creates a new empty hash set. The optional parameter `capacity` can be supplied to presize the
set so that it can hold the given number of elements without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash set with the default
capacity.
 -/
Std.HashSet.emptyWithCapacity : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 8 → Std.HashSet α
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The `w`-derivative of the Fourier transform integrand.  -/
VectorFourier.hasFDerivAt_fourierChar_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W),
  HasFDerivAt (fun w' => Real.fourierChar (-(L v) w') • f v)
    (Real.fourierChar (-(L v) w) • VectorFourier.fourierSMulRight L f v) w
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.getRef? : Lean.Elab.Term.Do.Code → Option Lean.Syntax
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, Std.TreeMap.Raw.empty.minKey? = none
-- Mathlib.Algebra.Lie.TensorProduct
/-- The action of the Lie algebra on one of its modules, regarded as a morphism of Lie modules.  -/
LieModule.toModuleHom : (R : Type u) →
  [inst : CommRing R] →
    (L : Type v) →
      (M : Type w) →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → TensorProduct R L M →ₗ⁅R,L⁆ M
-- Mathlib.Data.Rel
/-- Core of a set `S : Set β` w.R.t `R : SetRel α β` is the set of `x : α` that are related *only*
to elements of `S`. Other generalization of `Function.preimage`.  -/
SetRel.core : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set β → Set α
-- Mathlib.Order.RelClasses
instAsymmOfIsWellFounded : ∀ {α : Type u} (r : α → α → Prop) [IsWellFounded α r], Std.Asymm r
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.addEmptyConstants_invLHom : ∀ (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α],
  (FirstOrder.Language.LEquiv.addEmptyConstants L α).invLHom =
    (FirstOrder.Language.LHom.id L).sumElim (FirstOrder.Language.LHom.ofIsEmpty (FirstOrder.Language.constantsOn α) L)
-- Mathlib.Data.List.Zip
List.unzip_revzip : ∀ {α : Type u} (l : List α), l.revzip.unzip = (l, l.reverse)
-- Mathlib.Algebra.Field.ULift
ULift.up_nnratCast : ∀ {α : Type u} [inst : NNRatCast α] (q : ℚ≥0), { down := ↑q } = ↑q
-- Mathlib.NumberTheory.ModularForms.Bounds
_private.Mathlib.NumberTheory.ModularForms.Bounds.0.term𝕢 : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The counit isomorphism of the equivalence `TopRepIsoActionTop`.  -/
TopRep.fromActionToAction : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] →
          (X : Action (TopModuleCat k) G) → TopRep.toActionTopModFunc.obj (TopRep.fromActionTopModFunc.obj X) ≅ X
-- Std.Sat.AIG.Relabel
_private.Std.Sat.AIG.Relabel.0.Std.Sat.AIG.Decl.relabel.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (a : α) (h_1 : Unit → motive Std.Sat.AIG.Decl.false)
  (h_2 : (a : α) → motive (Std.Sat.AIG.Decl.atom a))
  (h_3 : (lhs rhs : Std.Sat.AIG.Fanin) → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match Std.Sat.AIG.Decl.atom a with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | Std.Sat.AIG.Decl.atom a => h_2 a
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs) =
    h_2 a
-- Mathlib.Order.CompleteLattice.Basic
iInf_eq_if : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst_1 : Decidable p] (a : α), ⨅ (_ : p), a = if p then a else ⊤
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.toFunAux : {s : Set ℕ} → [DecidablePred fun x => x ∈ s] → ↑s → ℕ
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.isDiag_diagonal : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [inst_1 : DecidableEq n] (d : n → α), (Matrix.diagonal d).IsDiag
-- Init.Prelude
/-- The value in the underlying type that satisfies the predicate.
 -/
Subtype.val : {α : Sort u} → {p : α → Prop} → Subtype p → α
-- Mathlib.GroupTheory.ResiduallyFinite
/-- `G` is residually finite if for every element `g` not equal to `1` there exists a group
homomorphism `f` to a finite group `H` such that `f g ≠ 1`.  -/
Group.residuallyFinite_of_forall_exists_finite_monoidHom : ∀ {G : Type u_1} [inst : Group G], (∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1) → Group.ResiduallyFinite G
-- Mathlib.Data.List.Perm.Subperm
List.Nodup.subperm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodup → l₁ ⊆ l₂ → l₁.Subperm l₂
-- Lean.Parser.Term
Lean.Parser.Term.haveI.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.ne' : ∀ {V : Type u} {G : SimpleGraph V} {a b : V}, G.Adj a b → b ≠ a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
HomotopyCategory.instIsHomologicalIntUpHomologyFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] (n : ℤ),
  (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).IsHomological
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true →
    Std.DTreeMap.Internal.Impl.contains k m₂ = false → Std.DTreeMap.Internal.Impl.contains k m₁ = true
-- Qq.Typ
Qq.instHashableQuoted : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.multisetProd_map_one : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Multiset α},
  (∀ x ∈ s, f x ≡ 1 [ZMOD n]) → (Multiset.map f s).prod ≡ 1 [ZMOD n]
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightAdjointMate_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : CategoryTheory.HasRightDual X], CategoryTheory.CategoryStruct.id Xᘁ = CategoryTheory.CategoryStruct.id Xᘁ
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.smulTower_leftMulMatrix_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T] {m : Type u_4}
  {n : Type u_5} [inst_7 : Fintype m] [inst_8 : Fintype n] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n]
  (b : Module.Basis m R S) (c : Module.Basis n S T) (x : S),
  (Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) =
    Matrix.blockDiagonal fun x_1 => (Algebra.leftMulMatrix b) x
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀` and its
integral on some finite-measure neighborhood of `x₀` converges to `1`, and `g` is integrable and
has a limit `a` at `x₀`, then `∫ φᵢ • g` converges to `a`.
Auxiliary lemma where one assumes additionally `a = 0`.  -/
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux : ∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E}
  {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → ℝ},
  MeasurableSet s →
    MeasurableSet t →
      t ⊆ s →
        t ∈ nhdsWithin x₀ s →
          (∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x) →
            (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)) →
              Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) →
                (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) →
                  MeasureTheory.IntegrableOn g s μ →
                    Filter.Tendsto g (nhdsWithin x₀ s) (nhds 0) →
                      Filter.Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (nhds 0)
-- Mathlib.Algebra.Group.ULift
ULift.addCommMonoid.eq_1 : ∀ {α : Type u} [inst : AddCommMonoid α], ULift.addCommMonoid = Function.Injective.addCommMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Cfg.mk.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (l : Option Λ) (var : σ) (Tape : Turing.Tape Γ)
  (l_1 : Option Λ) (var_1 : σ) (Tape_1 : Turing.Tape Γ),
  ({ l := l, var := var, Tape := Tape } = { l := l_1, var := var_1, Tape := Tape_1 }) =
    (l = l_1 ∧ var = var_1 ∧ Tape = Tape_1)
-- Mathlib.Order.Filter.Map
Filter.frequently_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop},
  (∃ᶠ (b : β) in Filter.map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_anti : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set V}, s ⊆ s' → G'.deleteVerts s' ≤ G'.deleteVerts s
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.Config.mk.sizeOf_spec : ∀ (distrib : Bool), sizeOf { distrib := distrib } = 1 + sizeOf distrib