mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inr : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g),
  (Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm (0, Algebra.Generators.cMulXSubOneCotangent T g) =
    x
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The image of a comonoid object under an oplax monoidal functor is a comonoid object.  -/
CategoryTheory.Functor.obj.instComonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (A : C) →
              [CategoryTheory.ComonObj A] →
                (F : CategoryTheory.Functor C D) → [F.OplaxMonoidal] → CategoryTheory.ComonObj (F.obj A)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_sum_list_ofFn : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Finset α},
  a ∈ (List.ofFn s).sum ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
-- Mathlib.Topology.Separation.Regular
/-- If the codomain of a closed embedding is a T₄ space, then so is the domain.  -/
Topology.IsClosedEmbedding.t4Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T4Space Y] {f : X → Y},
  Topology.IsClosedEmbedding f → T4Space X
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.instToStringAtomicFact : ToString Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.coe_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Ioc 0 1)), 0 < ↑x
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The finset of vertices in a complete equipartite subgraph as a `biUnion`.  -/
SimpleGraph.CompleteEquipartiteSubgraph.verts_eq_biUnion : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t), K.verts = K.parts.biUnion id
-- Mathlib.Algebra.Algebra.Opposite
/-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`.
This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
AlgEquiv.op : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ
-- Mathlib.Data.Countable.Basic
instCountableInt : Countable ℤ
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.X_subst : ∀ {R : Type u_2} [inst : CommRing R] (f : PowerSeries R), PowerSeries.subst PowerSeries.X f = f
-- Mathlib.Data.Nat.Factors
Nat.mem_primeFactorsList_iff_dvd : ∀ {n p : ℕ}, n ≠ 0 → Nat.Prime p → (p ∈ n.primeFactorsList ↔ p ∣ n)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atBot' : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β} {l : Filter β},
  Filter.Tendsto f Filter.atBot l ↔ ∀ s ∈ l, ∃ a, ∀ b ≤ a, f b ∈ s
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.get.match_1.splitter : (motive : Substring.Raw → String.Pos.Raw → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 : String.Pos.Raw) →
      ((s : String) → (b stopPos p : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := stopPos } p) →
        motive x x_1
-- Mathlib.Data.Set.Restrict
Set.mapsTo_iff_exists_map_subtype : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t ↔ ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
-- Mathlib.Topology.LocallyFinsupp
/-- Functions with locally finite support within `U` are `FunLike`: the coercion to functions is
injective.
 -/
Function.locallyFinsuppWithin.instFunLike : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : Zero Y] → FunLike (Function.locallyFinsuppWithin U Y) X Y
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.def : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, f =o[l] g → 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extensions_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (x : C),
  c.extensions.app x =
    TypeCat.ofHom fun f => CategoryTheory.CategoryStruct.comp c.ι ((CategoryTheory.Functor.const J).map f.down)
-- Mathlib.Data.Int.Bitwise
Int.testBit_lxor : ∀ (m n : ℤ) (k : ℕ), (m.xor n).testBit k = (m.testBit k ^^ n.testBit k)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of `SimpleGraph.IsIsolated.bot`. -/
SimpleGraph.isIsolated_bot : ∀ {V : Type u} {v : V}, ⊥.IsIsolated v
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitInv.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat),
  GrpCat.FilteredColimits.colimitInv F = { inv := fun x => Quot.lift (GrpCat.FilteredColimits.colimitInvAux F) ⋯ x }
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instZero : {R : Type u} → [inst : Semiring R] → Zero (Polynomial R)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_exp_mul_complex : ∀ {a b : ℝ} {c : ℂ}, c ≠ 0 → ∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pushout of `f, g` is also the pullback of `h ≫ f, h ≫ g` for any epi `h`.  -/
CategoryTheory.Limits.pushoutIsPushoutOfEpiComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (h : W ⟶ X) →
            [inst_1 : CategoryTheory.Epi h] →
              [inst_2 : CategoryTheory.Limits.HasPushout f g] →
                CategoryTheory.Limits.IsColimit
                  (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.inl f g)
                    (CategoryTheory.Limits.pushout.inr f g) ⋯)
-- Mathlib.RingTheory.PolynomialAlgebra
instIsScalarTowerPolynomial_1 : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [IsScalarTower R S A],
  IsScalarTower (Polynomial R) (Polynomial S) (Polynomial A)
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_norm_inv_mul_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖(f e)⁻¹ * b‖) a (nhds 0)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.id_apply : ∀ (M : MagmaCat) (x : ↑M), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map_injective_of_surjOn_or_injective : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q},
  Set.SurjOn ⇑g ↑S ↑T ∨ Function.Injective ⇑k → Function.Injective ⇑g → Function.Injective ⇑(f.map hy k)
-- Std.Http.Internal.Encode
Std.Http.Internal.instEncodeV11Version : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Version
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.Indep.isRkFinite_iff_finite : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → (M.IsRkFinite I ↔ I.Finite)
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.instNonemptyChooseBasisIndexOfNontrivial : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [Nontrivial M], Nonempty (Module.Free.ChooseBasisIndex R M)
-- Std.Time.Format.Modifier
Std.Time.instReprDayPeriod.repr : Std.Time.DayPeriod → ℕ → Std.Format
-- Mathlib.NumberTheory.Ostrowski
/-- A natural number not divisible by `p` has absolute value 1.  -/
Rat.AbsoluteValue.eq_one_of_not_dvd : ∀ {f : AbsoluteValue ℚ ℝ},
  (∀ (n : ℕ), f ↑n ≤ 1) →
    ∀ {p : ℕ}, 0 < f ↑p → f ↑p < 1 → (∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m) → ∀ {m : ℕ}, ¬p ∣ m → f ↑m = 1
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.FunInfoEnvCacheKey.mk.sizeOf_spec : ∀ (c : Lean.Name) (ls : List Lean.Level) (maxArgs? : Option ℕ),
  sizeOf { c := c, ls := ls, maxArgs? := maxArgs? } = 1 + sizeOf c + sizeOf ls + sizeOf maxArgs?
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.instFaithfulModuleCatEmbeddingRingFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (CategoryTheory.Abelian.FreydMitchell.functor C).Faithful
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_theta_coe_floor : ∀ (x : ℝ), Chebyshev.theta x = Chebyshev.theta ↑⌊x⌋₊
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.id.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_2 ()
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_5 : ∀ (x : Turing.PartrecToTM2.Cont') (f g : Turing.ToPartrec.Code),
  Turing.PartrecToTM2.codeSupp' (f.comp g) x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal (f.comp g) x) ∪
      (Turing.PartrecToTM2.codeSupp' g (Turing.PartrecToTM2.Cont'.comp f x) ∪
        (Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal f x) ∪ Turing.PartrecToTM2.codeSupp' f x))
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `PolynomialModule R S` is isomorphic to `S[X]` as an `R` module.  -/
PolynomialModule.equivPolynomial : {R : Type u_2} →
  [inst : CommRing R] →
    {S : Type u_6} → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → PolynomialModule R S ≃ₗ[R] Polynomial S
-- Mathlib.Topology.Maps.Strict.Group
/-- The product (in the sense of `AddMonoidHom.prodMap`) of
additive group homomorphisms is strict if and only if both homomorphisms are strict.  -/
AddMonoidHom.isStrictMap_prodMap_iff : ∀ {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [inst : AddGroup G'] [inst_1 : AddGroup H']
  [inst_2 : AddGroup G] [inst_3 : AddGroup H] {f : G →+ H} {g : G' →+ H'} [inst_4 : TopologicalSpace G]
  [inst_5 : TopologicalSpace H] [IsTopologicalAddGroup G] [inst_7 : TopologicalSpace G'] [IsTopologicalAddGroup G']
  [inst_9 : TopologicalSpace H'],
  Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffMul.toIsManifold : ∀ {𝕜 : 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} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : Mul G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G} [self : ContMDiffMul I n G],
  IsManifold I n G
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.toCircle_eq_circleExp : ∀ {N : ℕ} [inst : NeZero N] (j : ZMod N), ZMod.toCircle j = Circle.exp (2 * Real.pi * (↑j.val / ↑N))
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Coercion from `Subgraph G` to `SimpleGraph V`.  If `G'` is a spanning
subgraph, then `G'.spanningCoe` yields an isomorphic graph.
In general, this adds in all vertices from `V` as isolated vertices.  -/
SimpleGraph.Subgraph.spanningCoe : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → SimpleGraph V
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prodAssoc_symm_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsSFiniteKernel η]
  (ξ : ProbabilityTheory.Kernel α δ) [ProbabilityTheory.IsSFiniteKernel ξ],
  (κ.prod (ξ.prod η)).map ⇑MeasurableEquiv.prodAssoc.symm = (κ.prod ξ).prod η
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.times : Std.Internal.UV.System.CPUInfo → Std.Internal.UV.System.CPUTimes
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_image : ∀ {α : Type u} {β : Type v} (s : Set α) (f : α → β) [Finite ↑s], Finite ↑(f '' s)
-- Mathlib.Data.EReal.Inv
EReal.inv_nonpos_of_nonpos : ∀ {a : EReal}, a ≤ 0 → a⁻¹ ≤ 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α} {f : β → β},
  (Std.ExtDHashMap.Const.modify m k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instMonoid.eq_1 : ∀ (M : Type u_4) [inst : MulOne M],
  Monoid.End.instMonoid M =
    { mul := MonoidHom.comp, mul_assoc := ⋯, one := MonoidHom.id M, one_mul := ⋯, mul_one := ⋯,
      npow := fun n f => MonoidHom.copy (npowRec n f) (⇑f)^[n] ⋯, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- Computes `J(a | b)` by reducing `b` to odd by repeated division and then using
`fastJacobiSymAux`.  -/
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastJacobiSym : ℤ → ℕ → ℤ
-- Mathlib.CategoryTheory.ComposableArrows.One
CategoryTheory.ComposableArrows.functorArrows_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (i j n : ℕ)
  (hij : autoParam (i ≤ j) CategoryTheory.ComposableArrows.functorArrows._auto_1)
  (hj : autoParam (j ≤ n) CategoryTheory.ComposableArrows.functorArrows._auto_3)
  {S S' : CategoryTheory.ComposableArrows C n} (φ : S ⟶ S'),
  (CategoryTheory.ComposableArrows.functorArrows C i j n hij hj).map φ =
    CategoryTheory.ComposableArrows.homMk₁ (φ.app ⟨i, ⋯⟩) (φ.app ⟨j, ⋯⟩) ⋯
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarLeft_symm_apply_single : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_4} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_5}
  [inst_3 : DecidableEq ι] (i : ι) (n : N),
  ((TensorProduct.finsuppScalarLeft R N ι).symm fun₀ | i => n) = (fun₀ | i => 1) ⊗ₜ[R] n
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.continuous_iff : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] {B : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {f : α → β}, Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_ε_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (T : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) T)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) T) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) T)
-- Std.Data.HashMap.Basic
/-- Monadically computes a value by folding the given function over the mappings in the hash
map in some order.
 -/
Std.HashMap.foldM : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        {m : Type w → Type w'} → [Monad m] → {γ : Type w} → (γ → α → β → m γ) → γ → Std.HashMap α β → m γ
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.parenthesizerAliasesRef : IO.Ref (Lean.NameMap Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue)
-- Mathlib.Topology.Sheaves.Alexandrov
/-- Given `x : X`, this is the principal open subset of `X` generated by `x`.  -/
Alexandrov.principalOpen : {X : Type v} →
  [inst : TopologicalSpace X] → [inst_1 : Preorder X] → [Topology.IsUpperSet X] → X → TopologicalSpace.Opens X
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_le : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} {a b : Ordinal.{u}},
  (∀ (l : List ι), List.foldr f a l ≤ b) → Ordinal.nfpFamily f a ≤ b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α} [inst_1 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).get! k = m.get! k
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.instInhabitedWithTerminal.default : {C : Type u} → CategoryTheory.WithTerminal C
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalars.congr_simp : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f f_1 : A ≃ₐ[S] B), f = f_1 → AlgEquiv.restrictScalars R f = AlgEquiv.restrictScalars R f_1
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.removeSaveInfoAnnotation : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv_symm_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z : C} [inst_2 : CategoryTheory.ExactPairing Y Y'] (f : X ⟶ X')
  (g : X' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y'),
  (CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
      ((CategoryTheory.tensorRightHomEquiv X' Y Y' Z).symm g)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- A variant of `derivWithin_fun_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
derivWithin_fun_const_smul_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F),
  derivWithin (fun y => c • f y) s x = c • derivWithin f s x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_rightUnitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (self.mapComp f (CategoryTheory.CategoryStruct.id b)))
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.Entry.thmName : Lean.Compiler.CSimp.Entry → Lean.Name
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom_inv_id_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) {Z : C} (h_1 : F.obj i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map φ) (CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv h_1) = h_1
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.evalSyntaxConstantUnsafe : Lean.Environment → Lean.Options → Lean.Name → ExceptT String Id Lean.Syntax
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.wikidata : Mathlib.CrossRef.Database
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.FactorsThrough.same_level : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.FactorsThrough n
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.neg_const : ∀ {l : Lean.Omega.LinearCombo}, (-l).const = -l.const
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instFullGrpCatForget₂MonoidHomCarrierCarrier : (CategoryTheory.forget₂ CommGrpCat GrpCat).Full
-- Mathlib.Order.Defs.PartialOrder
lt_of_le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- As for coproducts, any functor between categories with binary biproducts gives rise to a
morphism `F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)`.  -/
CategoryTheory.Functor.biprodComparison' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              (X Y : C) →
                [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
                  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] →
                    F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)
-- Mathlib.Algebra.Order.Hom.Basic
/-- the image of a product is less or equal than the product of the images.  -/
SubmultiplicativeHomClass.map_mul_le_mul : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Mul α} {inst_1 : Mul β} {inst_2 : LE β}
  {inst_3 : FunLike F α β} [self : SubmultiplicativeHomClass F α β] (f : F) (a b : α), f (a * b) ≤ f a * f b
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (self : P.LeftHomotopy f g) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.i₁ (CategoryTheory.CategoryStruct.comp self.h h) =
    CategoryTheory.CategoryStruct.comp g h
-- Lean.Meta.AppBuilder
/-- Similar to `mkAppOptM`, but takes an `Expr` instead of a constant name.  -/
Lean.Meta.mkAppOptM' : Lean.Expr → Array (Option Lean.Expr) → Lean.MetaM Lean.Expr