mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.getElem_toArray_eq : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? i r.lower).get ⋯
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} [inst : (a : L.Sentence) → SizeOf (T a)] [inst_1 : SizeOf α]
  (toTheory : (L.withConstants α).Theory) (subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory)
  (isMaximal' : toTheory.IsMaximal),
  sizeOf { toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' } = 1 + sizeOf isMaximal'
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg_apply : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G)
  (s : Set G), μ.neg s = μ (-s)
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
`lp G 2`, an "elementary basis vector" in `lp G 2` supported at `i : ι` is the image of the
associated element in `E`.  -/
IsHilbertSum.linearIsometryEquiv_symm_apply_single : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  [inst_6 : DecidableEq ι] (hV : IsHilbertSum 𝕜 G V) {i : ι} (x : G i),
  hV.linearIsometryEquiv.symm (lp.single 2 i x) = (V i) x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.leFn? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
/-- The cardinality of the subgroup of Dirichlet characters of level `n` associated to an
intermediate field `F` of `ℚ(ζₙ)/ℚ` equals the degree `[F : ℚ]`.  -/
IsCyclotomicExtension.Rat.card_intermediateFieldEquivSubgroupChar : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [inst_5 : IsAbelianGalois ℚ K]
  (F : IntermediateField ℚ K),
  Nat.card ↥((IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R) F) = Module.finrank ℚ ↥F
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_conjTranspose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α),
  ‖A.conjTranspose‖₊ = ‖A‖₊
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommGroupWithOneOfAddMonoidHomClass : {ι : 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 ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddCommGroupWithOne (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] →
                      AddCommGroupWithOne (DirectLimit G f)
-- Mathlib.Topology.Separation.AlexandrovDiscrete
instDiscreteTopologyOfAlexandrovDiscreteOfT1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [AlexandrovDiscrete X] [T1Space X], DiscreteTopology X
-- Mathlib.Analysis.Meromorphic.Divisor
MeromorphicOn.AnalyticOnNhd.divisor_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U → z ∈ U → (MeromorphicOn.divisor f U) z = (ENat.map Nat.cast (analyticOrderAt f z)).untop₀
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {k : α} {v : β}, m.WF → ((k, v) ∈ Std.DHashMap.Raw.Const.toArray m ↔ Std.DHashMap.Raw.Const.get? m k = some v)
-- Init.Data.Vector.Range
Vector.range'_1_concat : ∀ {s n : ℕ}, Vector.range' s (n + 1) = Vector.range' s n ++ #v[s + n]
-- Mathlib.Algebra.Group.Defs
add_right_inj : ∀ {G : Type u_1} [inst : Add G] [IsLeftCancelAdd G] (a : G) {b c : G}, a + b = a + c ↔ b = c
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- **Structure theorem of finitely generated abelian groups** : Any finitely generated abelian
group is the product of a power of `ℤ` and a direct sum of some `ZMod (p i ^ e i)` for some
prime powers `p i ^ e i`.  -/
AddCommGroup.equiv_free_prod_directSum_zmod : ∀ (G : Type u) [inst : AddCommGroup G] [hG : AddGroup.FG G],
  ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ (Fin n →₀ ℤ) × DirectSum ι fun i => ZMod (p i ^ e i))
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddZeroClassOfContinuousAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddZeroClass β]
  [inst_3 : ContinuousAdd β],
  ContinuousMap.instAddZeroClassOfContinuousAdd =
    { toZero := ContinuousMap.instZero, toAdd := ContinuousMap.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getValueCast? a (Std.Internal.List.insertEntry k v l) =
    if h : (k == a) = true then some (cast ⋯ v) else Std.Internal.List.getValueCast? a l
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.range_eq_ofSection' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type (max v w))} {X : C}
  (f : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v} ⟶ F),
  CategoryTheory.Subfunctor.range f = CategoryTheory.Subfunctor.ofSection (CategoryTheory.uliftYonedaEquiv f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.continuous : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β), Continuous ⇑h
-- Mathlib.Data.Part
Part.to_ofOption : ∀ {α : Type u_1} (o : Option α), (↑o).toOption = o
-- Mathlib.CategoryTheory.Localization.Predicate
/-- This universal property states that a functor `L : C ⥤ D` inverts the morphisms
in `W` and every functor `F : C ⥤ E` (for a fixed category `E`) inverting `W` admits
a unique factorisation through `L`.  -/
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.MorphismProperty C →
            (E : Type u_3) →
              [CategoryTheory.Category.{v_3, u_3} E] → Type (max (max (max (max (max u_1 u_2) u_3) v_1) v_2) v_3)
-- Std.Sat.AIG.CNF
/-- Add a `Decl.atom` to a cache.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.addAtom : {aig : Std.Sat.AIG ℕ} →
  {cnf : Std.Sat.CNF ℕ} →
    {a : ℕ} →
      (cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf) →
        (idx : ℕ) →
          (h : idx < aig.decls.size) →
            aig.decls[idx] = Std.Sat.AIG.Decl.atom a → { out // Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache out idx h }
-- Mathlib.Data.Finset.Insert
Finset.mem_insert_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ s → a ∈ insert b s
-- Mathlib.Algebra.Module.Equiv.Basic
/-- The product `Π t : α, f t` of a family of modules is linearly isomorphic to the module
`f ⬝` when `α` only contains `⬝`.

This is `Equiv.piUnique` as a `LinearEquiv`.
 -/
LinearEquiv.piUnique : {α : Type u_9} →
  [inst : Unique α] →
    (R : Type u_10) →
      [inst_1 : Semiring R] →
        (f : α → Type u_11) →
          [inst_2 : (x : α) → AddCommMonoid (f x)] →
            [inst_3 : (x : α) → Module R (f x)] → ((t : α) → f t) ≃ₗ[R] f default
-- Mathlib.Order.Minimal
minimal_subset_iff : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, Minimal P s ↔ P s ∧ ∀ ⦃t : Set α⦄, P t → t ⊆ s → s = t
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.rfl : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, x.entails x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a
colimit cocone.  -/
CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)) →
          CategoryTheory.Limits.IsColimit b.toBinaryBicone.toCocone ≃ CategoryTheory.Limits.IsColimit b.toCocone
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.Const.entryAtIdx! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → ℕ → α × β
-- Mathlib.Data.List.AList
AList.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (entries : List (Sigma β))
  (nodupKeys : entries.NodupKeys),
  sizeOf { entries := entries, nodupKeys := nodupKeys } = 1 + sizeOf entries + sizeOf nodupKeys
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.add_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Add R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R] (f g : BoundedContinuousFunction α R) (x : α),
  (f + g) x = f x + g x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofHasKernel_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : CategoryTheory.Limits.HasKernel S.g],
  (CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_lt_iff_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → (a - b < c ↔ a < b + c)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceContext.mk.sizeOf_spec : ∀ (includeDeclaration : Bool), sizeOf { includeDeclaration := includeDeclaration } = 1 + sizeOf includeDeclaration
-- Mathlib.Data.Finset.Insert
Finset.insert_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, insert a s = s ↔ a ∈ s
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.instFinitePresentationUniversalFactorizationRing : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Algebra.FinitePresentation R (Polynomial.UniversalFactorizationRing m k hn p)
-- Lean.Meta.Tactic.Simp.Main
/-- Adapter for `Meta.simpHaveTelescope`  -/
Lean.Meta.Simp.simpHaveTelescope : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Order.Hom.Set
StrictMono.orderIsoOfSurjective_self_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (h_surj : Function.Surjective f) (b : β), f ((StrictMono.orderIsoOfSurjective f h_mono h_surj).symm b) = b
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabCoeFunNotation : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- To give an isomorphism between cocones, it suffices to give an
isomorphism between their vertices which commutes with the cocone
maps.  -/
CategoryTheory.Limits.Bicones.ext : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} →
          {c c' : CategoryTheory.Limits.Bicone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j)
                  CategoryTheory.Limits.Bicones.ext._auto_1 →
                autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j)
                    CategoryTheory.Limits.Bicones.ext._auto_3 →
                  (c ≅ c')
-- Mathlib.Topology.Order.Basic
/-- **Alias** of `countable_setOfPred_covBy_left`.

---

The set of points which are isolated on the left is countable when the space is
second-countable.  -/
countable_setOf_covBy_left : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | ∃ y, y ⋖ x}.Countable
-- Mathlib.Order.Hom.Lattice
/-- A `SupHom` preserves suprema.

Do not use this directly. Use `map_sup` instead.  -/
SupHom.map_sup' : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] (self : SupHom α β) (a b : α),
  self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- This is the precoverage on `C` where covering presieves are those where every
morphism satisfies `P`.  -/
CategoryTheory.MorphismProperty.precoverage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → CategoryTheory.Precoverage C
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mk.sizeOf_spec : ∀ {α : Type u_5} {β : Type u_6} [inst : SizeOf α] [inst_1 : SizeOf β] (toFun : α → β) (invFun : β → α) (source : Set α)
  (target : Set β) (map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target)
  (map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source) (left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x)
  (right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x),
  sizeOf
      { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
        map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' } =
    1
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The free functor `Type u ⥤ ModuleCat R` sending a type `X` to the
free `R`-module with generators `x : X`, implemented as the monoid algebra `R[X]`.
 -/
ModuleCat.monoidAlgebraFree : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (Type u) (ModuleCat R)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If `S` is an exact short complex and `f : P ⟶ S.X₂` is a morphism from a projective object `P`
such that `f ≫ S.g = 0`, this is a morphism `φ : P ⟶ S.X₁` such that `φ ≫ S.f = f`.  -/
CategoryTheory.ShortComplex.Exact.liftFromProjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          {P : C} →
            (f : P ⟶ S.X₂) → [CategoryTheory.Projective P] → CategoryTheory.CategoryStruct.comp f S.g = 0 → (P ⟶ S.X₁)
-- Mathlib.Data.Sum.Interval
Sum.Ico_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ a₂ : α),
  Finset.Ico (Sum.inl a₁) (Sum.inl a₂) = Finset.map Function.Embedding.inl (Finset.Ico a₁ a₂)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.adjustWith.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (sz : ℕ) (l : Ordnode α) (y : α) (r : Ordnode α)
  (h_1 : Unit → motive Ordnode.nil)
  (h_2 :
    (_t : Ordnode α) →
      (sz : ℕ) →
        (l : Ordnode α) → (y : α) → (r : Ordnode α) → _t = Ordnode.node sz l y r → motive (Ordnode.node sz l y r)),
  (match Ordnode.node sz l y r with
    | Ordnode.nil => h_1 ()
    | _t@h:(Ordnode.node sz l y r) => h_2 _t sz l y r h) =
    h_2 (Ordnode.node sz l y r) sz l y r ⋯
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- `C ⥤ₗ D` denotes left exact functors `C ⥤ D`  -/
CategoryTheory.«term_⥤ₗ_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Edges of the subgraph  -/
SimpleGraph.Subgraph.Adj : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → V → V → Prop
-- Init.Data.Array.Lemmas
Array.back_append : ∀ {α : Type u_1} {ys xs : Array α} (h : 0 < (xs ++ ys).size),
  (xs ++ ys).back h = if h' : ys.isEmpty = true then xs.back ⋯ else ys.back ⋯
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.ofHom_comp : ∀ {R S T : Type u} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Ring T] (f : R →+* S) (g : S →+* T),
  RingCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (RingCat.ofHom f) (RingCat.ofHom g)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isSome_get?_eq_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, (m.get? a).isSome = m.contains a
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.d_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (self : M.Derivation φ) {X : Dᵒᵖ} (a b : ↑(R.obj X)), self.d (a * b) = a • self.d b + b • self.d a
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_ciInf : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompletePartialOrderInf α] [InfConvergenceClass α] {f : ι → α},
  Monotone f → BddBelow (Set.range f) → Filter.Tendsto f Filter.atBot (nhds (⨅ i, f i))
-- Mathlib.Topology.MetricSpace.Completion
LipschitzWith.completion_extension : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : MetricSpace β] [CompleteSpace β] {f : α → β}
  {K : NNReal}, LipschitzWith K f → LipschitzWith K (UniformSpace.Completion.extension f)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The push-forward of a finite measure by a continuous function between Borel spaces as
a continuous linear map.  -/
MeasureTheory.FiniteMeasure.mapCLM : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] →
        [inst_2 : TopologicalSpace Ω] →
          [inst_3 : OpensMeasurableSpace Ω] →
            [inst_4 : TopologicalSpace Ω'] →
              [inst_5 : BorelSpace Ω'] →
                {f : Ω → Ω'} → Continuous f → MeasureTheory.FiniteMeasure Ω →L[NNReal] MeasureTheory.FiniteMeasure Ω'
-- Mathlib.GroupTheory.PushoutI
/-- A constructor that multiplies a `NormalWord` by an element, with condition to make
sure the underlying list does get longer.  -/
Monoid.PushoutI.NormalWord.cons : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              {i : ι} →
                (g : G i) →
                  (w : Monoid.PushoutI.NormalWord d) →
                    w.fstIdx ≠ some i → g ∉ (φ i).range → Monoid.PushoutI.NormalWord d
-- Plausible.Gen
/-- Raised when a fueled generator fails due to insufficient fuel.  -/
Plausible.Gen.outOfFuel : Plausible.GenError
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.alter_eq_empty_iff_erase_eq_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  t.alter k f = ∅ ↔ t.erase k = ∅ ∧ f (t.get? k) = none
-- Lean.Elab.Tactic.Omega.MinNatAbs
_private.Lean.Elab.Tactic.Omega.MinNatAbs.0.Lean.Elab.Tactic.Omega.List.nonzeroMinimum.eq_1 : ∀ (xs : List ℕ), Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = (List.filter (fun x => decide (x ≠ 0)) xs).min?.getD 0
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The bicategory of algebras (monoids) and bimodules, all internal to some monoidal category.  -/
Bimod.monBicategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.Limits.HasCoequalizers C] →
        [∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            CategoryTheory.Bicategory (CategoryTheory.Mon C)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- For `1 < s`, the topological sum of `ZetaAsymptotics.term (n + 1) s` over all `n : ℕ` is
`1 / (s - 1) - ζ s / s`.
 -/
ZetaAsymptotics.termTSum_of_lt : ∀ {s : ℝ}, 1 < s → ZetaAsymptotics.termTSum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposingCat_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) (f : b ⟶ c),
  (CategoryTheory.Bicategory.postcomposingCat a b c).obj f = (CategoryTheory.Bicategory.postcomp a f).toCatHom
-- Mathlib.Data.Nat.Multiplicity
/-- A prime power divides `n!` iff it is at most the sum of the quotients `n / p ^ i`.
This sum is expressed over the set `Ico 1 b` where `b` is any bound greater than `log p n`  -/
Nat.Prime.pow_dvd_factorial_iff : ∀ {p n r b : ℕ}, Nat.Prime p → Nat.log p n < b → (p ^ r ∣ n.factorial ↔ r ≤ ∑ i ∈ Finset.Ico 1 b, n / p ^ i)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.LE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → LE (CategoryTheory.Pretopology C)
-- Mathlib.FieldTheory.Fixed
finrank_algHom : ∀ (K : Type u) (V : Type v) [inst : Field K] [inst_1 : Field V] [inst_2 : Algebra K V] [inst_3 : FiniteDimensional K V],
  Fintype.card (V →ₐ[K] V) ≤ Module.finrank V (V →ₗ[K] V)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Entries for the `grw` discrimination tree.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.grw : Mathlib.Tactic.ClickSuggestions.Entries✝ →
  Array
    (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- The type of closed submodules of a topological module.  -/
ClosedSubmodule : (R : Type u_2) →
  (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [TopologicalSpace M] → [Module R M] → Type u_3
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- If the image of morphism `M' ⟶ M` lands in a submonoid functor `S`,
then the morphism factors through it.  -/
CategoryTheory.SubmonoidFunctor.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M M' : CategoryTheory.Functor C MonCat} →
      (p : M ⟶ M') →
        (S' : CategoryTheory.SubmonoidFunctor M') → CategoryTheory.SubmonoidFunctor.image p ⊤ ≤ S' → (M ⟶ S'.toFunctor)
-- Lean.Elab.MatchAltView
Lean.Elab.Term.instInhabitedMatchAltView : {a : Lean.SyntaxNodeKinds} → Inhabited (Lean.Elab.Term.MatchAltView a)
-- Mathlib.LinearAlgebra.Projection
Submodule.isIdempotentElemEquiv_symm_apply_coe : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p : Submodule R E)
  (f : { f // ∀ (x : ↥p), f ↑x = x }), ↑(p.isIdempotentElemEquiv.symm f) = p.subtype ∘ₗ ↑f