mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C)
  (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H),
  (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso c).inv.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F c).comp X))
-- Init.Prelude
/-- Create syntax node with 7 children  -/
Lean.Syntax.node7 : Lean.SourceInfo →
  Lean.SyntaxNodeKind →
    Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.represents_iff' : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] {A : Matrix ι ι R} {f : Module.End R M},
  Matrix.Represents b A f ↔ ∀ (j : ι), ∑ i, A i j • b i = f (b j)
-- Std.Http.Data.Status
Std.Http.Status.unprocessableEntity.sizeOf_spec : sizeOf Std.Http.Status.unprocessableEntity = 1
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with eventually summable sup norm is the uniform limit of its
partial sums. Version with general index set.  -/
tendstoUniformly_tsum_of_cofinite_eventually : ∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {ι : Type u_4} {f : ι → β → F}
  {u : ι → ℝ},
  Summable u →
    (∀ᶠ (n : ι) in Filter.cofinite, ∀ (x : β), ‖f n x‖ ≤ u n) →
      TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : ι), f n x) Filter.atTop
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The root number of the unique Dirichlet character modulo 1 is 1.  -/
DirichletCharacter.rootNumber_modOne : ∀ (χ : DirichletCharacter ℂ 1), χ.rootNumber = 1
-- Mathlib.Data.EReal.Operations
EReal.add_eq_bot_iff : ∀ {x y : EReal}, x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
-- Mathlib.Algebra.GroupWithZero.Defs
noZeroDivisors_iff_right_eq_zero_of_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.induction_mk : ∀ {X : SSet} {motive : X.N → Sort u_1} (mk : (n : ℕ) → (x : ↑(X.nonDegenerate n)) → motive (SSet.N.mk ↑x ⋯)) {n : ℕ}
  (s : ↑(X.nonDegenerate n)), SSet.N.induction mk (SSet.N.mk ↑s ⋯) = mk n s
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The size of the replacement when printed  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.stringLength : Mathlib.Tactic.LibraryRewrite.Rewrite → ℕ
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_eq_one_iff_unique : ∀ {α : Type u_3}, ENat.card α = 1 ↔ Nonempty (Unique α)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isMulLeftInvariant_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  (c : ENNReal), (c • μ).IsMulLeftInvariant
-- Mathlib.Data.Nat.Choose.Sum
Finset.prod_pow_choose_succ : ∀ {M : Type u_2} [inst : CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∏ i ∈ Finset.range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ Finset.range (n + 1), f i (n + 1 - i) ^ n.choose i) *
      ∏ i ∈ Finset.range (n + 1), f (i + 1) (n - i) ^ n.choose i
-- LeanSearchClient.Syntax
/-- Search from within Lean, depending on the option `leansearchclient.backend` (currently only leansearch).
Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

```lean
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.
```
  -/
LeanSearchClient.search_cmd : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.circulantGraph.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  SimpleGraph.circulantGraph s = SimpleGraph.fromRel fun x1 x2 => x1 - x2 ∈ s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_smul_right : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (a : R) (x y : M),
  QuadraticMap.polar (⇑Q) x (a • y) = a • QuadraticMap.polar (⇑Q) x y
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The preimage of a `Submonoid` along a `MonoidHom` is a `Submonoid`.  -/
Submonoid.comap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : MonoidHomClass F M N] → F → Submonoid N → Submonoid M
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportData.mk.sizeOf_spec : ∀ (errors : IO.Ref (Array Lean.Meta.LazyDiscrTree.ImportFailure)), sizeOf { errors := errors } = 1 + sizeOf errors
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).base =
    CategoryTheory.CategoryStruct.id X.base
-- Init.Grind.AC
/-- Given `lhs₁ = rhs₁` and `lhs₂ = rhs₂` where `lhs₁ := union c r₁` and `lhs₂ := union c r₂`,
`lhs = rhs` where `lhs := union r₂ rhs₁` and `rhs := union r₁ rhs₂`
 -/
Lean.Grind.AC.superpose_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_ac_cert r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs = Lean.Grind.AC.Seq.denote ctx rhs
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.eq_def : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (i : ℕ) (a : i ≤ n),
  Nat.allLTTR.loop✝ n f i a =
    match i, a with
    | 0, x => true
    | i.succ, h => f (n - (i + 1)) ⋯ && Nat.allLTTR.loop✝ n f i ⋯
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.any_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Monad m] [inst_4 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m β'} {p : β' → Bool},
  Std.IterM.any p (Std.Iter.mapM f it) =
    Std.IterM.anyM (fun x => (fun x => { down := p x }) <$> f x) (Std.Iter.mapM pure it)
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_ofObj : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1} (X : ι → Cᵒᵖ),
  (CategoryTheory.ObjectProperty.ofObj X).unop = CategoryTheory.ObjectProperty.ofObj fun i => Opposite.unop (X i)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_blsub_iff : ∀ {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}} {a : Ordinal.{max u v}},
  a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.instIsCorepresentableIdType : (CategoryTheory.Functor.id (Type v)).IsCorepresentable
-- Mathlib.CategoryTheory.Types.Basic
/-- The identity function as a `Fun`.  -/
TypeCat.Fun.id : (X : Type u_1) → TypeCat.Fun X X
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.WellFounded.eq_1 : ∀ (α : Type w) (m : Type w → Type w') {β : Type w} [inst : Std.Iterator α m β] {γ : Type x}
  (plausible_forInStep : β → γ → ForInStep γ → Prop),
  Std.IteratorLoop.WellFounded α m plausible_forInStep = WellFounded (Std.IteratorLoop.rel α m plausible_forInStep)
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {a b c : CategoryTheory.LocallyDiscrete Cᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c)
  (X : CategoryTheory.Sheaf (J.over (Opposite.unop a.as)) A) (X_1 : (CategoryTheory.Over (Opposite.unop c.as))ᵒᵖ),
  (((J.pseudofunctorOver A).mapComp x x_1).inv.toNatTrans.app X).hom.app X_1 =
    X.obj.map ((CategoryTheory.Over.mapComp x_1.as.unop x.as.unop).hom.app (Opposite.unop X_1)).op
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.instConcreteCategorySubtypeForallCarrierMeasurable : CategoryTheory.ConcreteCategory MeasCat fun x1 x2 => { f // Measurable f }
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_fst_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 φ] {K : CochainComplex C ℤ}
  {d e : ℤ} (γ : CochainComplex.HomComplex.Cochain F K d) (he : 1 + d = e),
  (CochainComplex.mappingCone.inl φ).comp ((↑(CochainComplex.mappingCone.fst φ)).comp γ he) ⋯ = γ
-- Lean.DocString.Add
/-- Reports parse errors from a Verso docstring parse failure.

When Verso docstring parsing fails at parse time, a `parseFailure` node is created containing the
raw text, because emitting an error at that stage could lead to unwanted parser backtracking. This
function reports the actual error messages with proper source positions.
 -/
Lean.reportVersoParseFailure : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadFileMap m] →
      [Lean.MonadError m] →
        [Lean.MonadEnv m] → [Lean.MonadOptions m] → [Lean.MonadLog m] → [Lean.MonadResolveName m] → Lean.Syntax → m Unit
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
instIsMeasurablyGeneratedCocompactOfR1Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [R1Space α],
  (Filter.cocompact α).IsMeasurablyGenerated
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {x y : F.Elements}
  (f g : x ⟶ y), ↑f = ↑g → f = g
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.of_Lawson_symm_eq : ∀ {α : Type u_1}, Topology.WithLawson.ofLawson.symm = Topology.WithLawson.toLawson
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : AddZeroClass β],
  WithZero.lift =
    { toFun := fun f => { toFun := fun n => WithZero.recZeroCoe 0 (⇑f) n, map_zero' := ⋯, map_add' := ⋯ },
      invFun := fun F => (↑F).comp WithZero.coeAddHom, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceSub : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_div_iff_left : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] [MulRightStrictMono α] {b c : α} (a : α),
  a / b < a / c ↔ c < b
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C}
  (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)))
      (CategoryTheory.CategoryStruct.comp (X.cokernelIsoCycles f g fg h n).hom
        (CategoryTheory.CategoryStruct.comp (X.iCycles f g n) h_1)) =
    CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h_1
-- Mathlib.Algebra.Order.Hom.Basic
abs_sub_map_le_div : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommGroup β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] (f : F) (x y : α), |f x - f y| ≤ f (x / y)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.fieldRange_val : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  S.val.fieldRange = S
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Prime.not_pseudoperfect : ∀ {p : ℕ}, Nat.Prime p → ¬p.Pseudoperfect
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k k' : α}, t.getKey? k = some k' → (Std.TreeMap.filterMap f t)[k]? = t[k]?.bind (f k')
-- Std.Time.Date.Unit.Week
/-- Convert `Nanosecond.Offset` into `Week.Offset`.
 -/
Std.Time.Week.Offset.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Week.Offset
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.comp_memLp : ∀ {p : ENNReal} {α : Type u_6} {E : Type u_7} {F : Type u_8} {K : NNReal} [inst : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] {f : α → E} {g : E → F},
  LipschitzWith K g → g 0 = 0 → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (g ∘ f) p μ
-- Std.Do.SPred.SPred
/-- Entailment in `SPred`.

One predicate `P` entails another predicate `Q` if `Q` is true in every state in which `P` is true.
Unlike implication (`SPred.imp`), entailment is not itself an `SPred`, but is instead an ordinary
proposition.
 -/
Std.Do.SPred.entails : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → Prop
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₄.eq_def : ∀ (w x y z : UInt8),
  ByteArray.utf8DecodeChar?.assemble₄ w x y z =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
              ByteArray.utf8DecodeChar?.isInvalidContinuationByte y ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte z) =
          true then
      none
    else
      let r := ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z;
      if h₁ : r < 65536 then none else if h₂ : 1114111 < r then none else some { val := r, valid := ⋯ }
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.sub : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f g : α → β} {a : α}, IsLocalMin f a → IsLocalMax g a → IsLocalMin (fun x => f x - g x) a
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Cauchy–Schwarz inequality with norm  -/
real_inner_le_norm : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F), inner ℝ x y ≤ ‖x‖ * ‖y‖
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLeftExtension_unit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  (CategoryTheory.Bicategory.lanLeftExtension f g).unit = CategoryTheory.Bicategory.lanUnit f g
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α], Set.Ioi ⊥ = {⊥}ᶜ
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mkCommaObject_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (x : C),
  (CategoryTheory.WithInitial.mkCommaObject F).hom.app x =
    F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
-- Mathlib.RepresentationTheory.Rep.Basic
ModuleCat.endRingEquiv.eq_1 : ∀ {R : Type u} [inst : Ring R] (M : ModuleCat R),
  M.endRingEquiv =
    { toFun := ModuleCat.Hom.hom, invFun := ModuleCat.ofHom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
      map_add' := ⋯ }
-- Init.Data.List.Lemmas
List.getElem_set_ne : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i ≠ j → ∀ {a : α} (hj : j < (l.set i a).length), (l.set i a)[j] = l[j]
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_top_of_isLocalized'_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Rₚ : ↑s → Type u_4) [inst_3 : (r : ↑s) → CommSemiring (Rₚ r)] [inst_4 : (r : ↑s) → Algebra R (Rₚ r)]
      [inst_5 : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5)
      [inst_6 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_7 : (r : ↑s) → Module R (Mₚ r)]
      [inst_8 : (r : ↑s) → Module (Rₚ r) (Mₚ r)] [inst_9 : ∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_10 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M},
      (∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊤) → N = ⊤
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instInhabited : {M : Type u_1} → [inst : MulOneClass M] → Inhabited (Submonoid M)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.contentChange.sizeOf_spec : sizeOf Lean.Lsp.SignatureHelpTriggerKind.contentChange = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
/-- `horn n i` (or `Λ[n, i]`) is the `i`-th horn of the `n`-th standard simplex,
where `i : n`. It consists of all `m`-simplices `α` of `Δ[n]`
for which the union of `{i}` and the range of `α` is not all of `n`
(when viewing `α` as monotone function `m → n`).  -/
SSet.horn : (n : ℕ) → Fin (n + 1) → (SSet.stdSimplex.obj { len := n }).Subcomplex
-- Init.Data.Iterators.Lemmas.Producers.List
List.step_iter_nil : ∀ {β : Type w}, [].iter.step = ⟨Std.IterStep.done, ⋯⟩
-- Plausible.Gen
Plausible.Gen.down : {α : Type u_1} → Plausible.Gen (ULift.{v, u_1} α) → Plausible.Gen α
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDivInvMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : DivInvMonoid G],
  Filter.Germ.instDivInvMonoid =
    { toMonoid := Filter.Germ.instMonoid, toInv := Filter.Germ.instInv, toDiv := Filter.Germ.instDiv,
      zpow := fun z f => f ^ z, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
SchwartzMap.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
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instNeg : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : NegZeroClass R] → Neg (HahnSeries Γ R)
-- Std.Data.DTreeMap.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings.  -/
Std.DTreeMap.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} → {cmp : α → α → Ordering} → ((a : α) → β a → γ a) → Std.DTreeMap α β cmp → Std.DTreeMap α γ cmp
-- Lean.Message
/-- `composePreservingKind msg msg'` appends the contents of `msg'` to the end of `msg` but ensures that
the resulting message preserves the kind (as given by `MessageData.kind`) of `msg`.
 -/
Lean.MessageData.composePreservingKind : Lean.MessageData → Lean.MessageData → Lean.MessageData
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.toList.eq_2 : ∀ {V : Type u} [inst : Quiver V] {a : V} (x b : V) (p : Quiver.Path a b) (a_1 : b ⟶ x),
  (p.cons a_1).toList = b :: p.toList
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.span_univ : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], LieSubmodule.lieSpan R L Set.univ = ⊤
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_le_essSup : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (f : α → ENNReal),
  ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Negadd-negadd-negadd version.  -/
Finset.ruzsa_triangle_inequality_negAdd_negAdd_negAdd : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  B.card * (-A + C).card ≤ (-B + A).card * (-B + C).card
-- Std.Http.Protocol.H1.Reader
/-- Manages the reading state of the HTTP parsing and processing machine.
 -/
Std.Http.Protocol.H1.Reader : Std.Http.Protocol.H1.Direction → Type
-- Mathlib.NumberTheory.FermatPsp
/-- `n` is a probable prime to base `b` if `n` passes the Fermat primality test; that is, `n` divides
`b ^ (n - 1) - 1`.
This definition implies that all numbers are probable primes to base 0 or 1, and that 0 and 1 are
probable primes to any base.
 -/
Nat.ProbablePrime : ℕ → ℕ → Prop
-- Mathlib.Data.NNReal.Defs
NNReal.instIsStrictOrderedRing_1 : IsStrictOrderedRing NNReal
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsEulerian.edgeSet_eq : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsEulerian → p.edgeSet = G.edgeSet
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.V.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i i_1 : self.J)
  (e_i : i = i_1) (j j_1 : self.J) (e_j : j = j_1) (a : i ≠ j), self.V i j a = self.V i_1 j_1 ⋯
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_eq_closure_mul_set : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] (M N : AddSubmonoid R), M * N = AddSubmonoid.closure (↑M * ↑N)
-- Lean.Message
Lean.instInhabitedMessageLog.default : Lean.MessageLog
-- Lean.Meta.CoeAttr
/-- The number of arguments to the coercion function  -/
Lean.Meta.CoeFnInfo.numArgs : Lean.Meta.CoeFnInfo → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomologyMapData.neg_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂), γ.neg.left = γ.left.neg
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.whiskerRight_def : ∀ {R : Type u} [inst : CommSemiring R] {X₁ X₂ : SemimoduleCat R} (f : X₁ ⟶ X₂) (N : SemimoduleCat R),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f N = SemimoduleCat.MonoidalCategory.whiskerRight f N
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_div : ∀ {K : Type u_1} [inst : RCLike K] (z w : K), RCLike.normSq (z / w) = RCLike.normSq z / RCLike.normSq w
-- Mathlib.Topology.Order.LiminfLimsup
exists_seq_tendsto_limsSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [FirstCountableTopology α] {f : Filter α} [f.NeBot] [f.IsCountablyGenerated],
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) exists_seq_tendsto_limsSup._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f) exists_seq_tendsto_limsSup._auto_3 →
      ∃ x, Filter.Tendsto x Filter.atTop (nhds f.limsSup) ∧ Filter.Tendsto x Filter.atTop f
-- Lean.DeclarationRange
Lean.addBuiltinDeclarationRanges : Lean.Name → Lean.DeclarationRanges → IO Unit
-- Mathlib.GroupTheory.Congruence.Defs
/-- The complete lattice of additive congruence relations on a given type with
an addition.  -/
AddCon.instCompleteLattice : {M : Type u_1} → [inst : Add M] → CompleteLattice (AddCon M)