mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusFun.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R),
  x.frobeniusFun = WittVector.mk p fun n => (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
-- Mathlib.Tactic.DeriveCountable
_private.Mathlib.Tactic.DeriveCountable.0.Mathlib.Deriving.Countable.mkToNatMatch : Lean.Elab.Deriving.Context →
  Lean.Elab.Deriving.Header → Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM Lean.Term
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eraseKey_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    (k == a) = true → Std.Internal.List.getEntry? a (Std.Internal.List.eraseKey k l) = none
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one_sorted : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.one.Sorted
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_intro' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (Q ∧ P ⊢ₛ R) → P ⊢ₛ Q → R
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {c : ℕ}, (Std.HashMap.Raw.emptyWithCapacity c).toList = []
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_two_pi : Real.cos (2 * Real.pi) = 1
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.unopFunctor_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op),
  (CategoryTheory.Comma.unopFunctor L R).obj X =
    Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_ofNatLT : ∀ (n : ℕ) (hn : n < 2 ^ 64), Int64.ofBitVec n#'hn = Int64.ofNat n
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.trans_isLittleO : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {l : Filter α} {f : α → E} {g : α → F'} {k : α → G},
  f =O[l] g → g =o[l] k → f =o[l] k
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
  Function.Injective f → ∀ (x : α →₀ M) (a : α), (Finsupp.mapDomain f x) (f a) = x a
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.mem_closure_iff_exists_finset_subset : ∀ {M : Type u_1} [inst : AddCommMonoid M] {x : M} {s : Set M},
  x ∈ AddSubmonoid.closure s ↔ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedSlowInsertionInto : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `s` is an antitone family of sets and `f` tends to `atTop` along a nontrivial filter,
then the indexed intersection of `s ∘ f` is equal to the indexed intersection of `s`.  -/
Antitone.iInter_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ},
  Antitone s → ∀ {f : α → β}, Filter.Tendsto f l Filter.atTop → ⋂ a, s (f a) = ⋂ b, s b
-- Mathlib.Data.Num.ZNum
ZNum.isStrictOrderedRing : IsStrictOrderedRing ZNum
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.uncurry_uncurry_ihomCurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  CategoryTheory.MonoidalClosed.uncurry
      (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.MonoidalClosed.ihomCurry x y z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator x y
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z)).inv
      ((CategoryTheory.ihom.ev (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)).app z)
-- Mathlib.Order.Filter.Basic
Filter.eventually_top : ∀ {α : Type u} {p : α → Prop}, (∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x
-- Init.Data.SInt.Lemmas
Int16.lt_asymm : ∀ {a b : Int16}, a < b → ¬b < a
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The additive character on `ZMod n` defined using `ζ` sends `a` to `ζ^a`.  -/
AddChar.zmodChar_apply : ∀ {C : Type v} [inst : CommMonoid C] {n : ℕ} [inst_1 : NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ZMod n),
  (AddChar.zmodChar n hζ) a = ζ ^ a.val
-- Mathlib.Data.Matrix.Mul
Matrix.single_one_vecMul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonAssocSemiring R]
  (i : m) (M : Matrix m n R), Matrix.vecMul (Pi.single i 1) M = M.row i
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedMon.default : Lean.Grind.CommRing.Mon
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_unitIso_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (X : CategoryTheory.MonoidalCategory.DayFunctor C V),
  (CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.map` as a `RingHom`.  -/
LocallyConstant.mapRingHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        [inst_1 : Semiring Y] → [inst_2 : Semiring Z] → (Y →+* Z) → LocallyConstant X Y →+* LocallyConstant X Z
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.domChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), h.domChart ∈ IsManifold.maximalAtlas I n M
-- Mathlib.Algebra.Ring.SumsOfSquares
Subsemiring.mem_sumSq : ∀ {T : Type u_2} [inst : CommSemiring T] {s : T}, s ∈ Subsemiring.sumSq T ↔ IsSumSq s
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isUniformEmbedding_toUniformOnFun : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F],
  IsUniformEmbedding fun f => (UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s}) ⇑f
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddCommSemigroup : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddCommSemigroup A] → AddCommSemigroup (CStarMatrix m n A)
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.lastTaskMutex : Lean.Server.StatefulRequestHandler → Std.Mutex (Lean.Server.ServerTask Unit)
-- Init.System.IOError
IO.Error.interrupted.sizeOf_spec : ∀ (filename : String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.interrupted filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Mathlib.RingTheory.QuasiFinite.Polynomial
Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S) (P : Ideal S) [inst_3 : P.IsPrime] [Algebra.WeaklyQuasiFiniteAt R P],
  Ideal.map Polynomial.C (Ideal.under R P) < Ideal.comap (↑f) P
-- Mathlib.Data.Sym.Sym2
/-- `ToRel` induces an order embedding from `Sym2` sets to relations  -/
Sym2.toRelOrderEmbedding : (α : Type u_1) → Set (Sym2 α) ↪o (α → α → Prop)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.UniversallyEffectiveEquivalenceRelation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R A : C} {p₁ p₂ : R ⟶ A}
  {toEffectiveEquivalenceRelation : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂}
  {universally_effectiveEpi_π :
    CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f)
      toEffectiveEquivalenceRelation.π}
  {toEffectiveEquivalenceRelation_1 : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂}
  {universally_effectiveEpi_π_1 :
    CategoryTheory.MorphismProperty.universally (fun x x_1 f => CategoryTheory.EffectiveEpi f)
      toEffectiveEquivalenceRelation_1.π},
  { toEffectiveEquivalenceRelation := toEffectiveEquivalenceRelation,
        universally_effectiveEpi_π := universally_effectiveEpi_π } =
      { toEffectiveEquivalenceRelation := toEffectiveEquivalenceRelation_1,
        universally_effectiveEpi_π := universally_effectiveEpi_π_1 } →
    toEffectiveEquivalenceRelation = toEffectiveEquivalenceRelation_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp) (a : α),
  t.contains a = Std.DTreeMap.Internal.Impl.contains a t.inner
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.nonuniformWitnesses_spec : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t →
    ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|
-- Mathlib.RingTheory.WittVector.Defs
WittVector.coeff_surjective : ∀ {p : ℕ} {R : Type u_1} (n : ℕ), Function.Surjective fun x => x.coeff n
-- Mathlib.Data.Multiset.FinsetOps
Multiset.disjoint_ndinsert_left : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Multiset α},
  Disjoint (Multiset.ndinsert a s) t ↔ a ∉ t ∧ Disjoint s t
-- Batteries.Data.Nat.Lemmas
Nat.recDiag_zero_zero : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1)),
  Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toList.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  t.toList = Std.DTreeMap.Internal.Impl.foldr (fun k v l => ⟨k, v⟩ :: l) [] t
-- Lean.Elab.SetOption
_private.Lean.Elab.SetOption.0.Lean.Elab.throwUnconfigurable : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → {α : Type} → Lean.Name → m α
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  ↑e.toOpenPartialHomeomorph.symm = ⇑e.symm
-- Init.System.IO
_private.Init.System.IO.0.IO.FS.Handle.lines.read : IO.FS.Handle → Array String → IO (Array String)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_toArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toArray.isEmpty = m.isEmpty
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sshiftRight'_of_msb_true : ∀ {w : ℕ} {x y : BitVec w}, x.msb = true → (x.sshiftRight' y).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : MulZeroOneClass α] →
          [inst_3 : MulZeroOneClass β] →
            (toMonoidWithZeroHom : α →*₀ β) → Monotone (↑toMonoidWithZeroHom).toFun → α →*₀o β
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.union : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsLowerSet s → IsLowerSet t → IsLowerSet (s ∪ t)
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
/-- `f` has superpolynomial decay in parameter `k` along filter `l` if
`k ^ n * f` tends to zero at `l` for all naturals `n`  -/
Asymptotics.SuperpolynomialDecay : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace β] → [CommSemiring β] → Filter α → (α → β) → (α → β) → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is polynomial on a set `s`, so is its Fréchet derivative.  -/
CPolynomialOn.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, CPolynomialOn 𝕜 f s → CPolynomialOn 𝕜 (fderiv 𝕜 f) s
-- Lean.Meta.TransparencyMode
Lean.Meta.TransparencyMode.hash : Lean.Meta.TransparencyMode → UInt64
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sum_comap_seq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ]
  (hg : Measurable g), (ProbabilityTheory.Kernel.sum fun n => (κ.seq n).comap g hg) = κ.comap g hg
-- Mathlib.Topology.Algebra.GroupWithZero
/-- `h x (f x / g x)` is continuous under certain conditions, even if the denominator is sometimes
`0`. See docstring of `ContinuousAt.comp_div_cases`.  -/
Continuous.comp_div_cases : ∀ {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
  [ContinuousInv₀ G₀] [ContinuousMul G₀] [inst_4 : TopologicalSpace α] [inst_5 : TopologicalSpace β] {f g : α → G₀}
  (h : α → G₀ → β),
  Continuous f →
    Continuous g →
      (∀ (a : α), g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)) →
        (∀ (a : α), g a = 0 → Filter.Tendsto (↿h) (nhds a ×ˢ ⊤) (nhds (h a 0))) → Continuous fun x => h x (f x / g x)
-- Mathlib.ModelTheory.Semantics
/-- A sentence can be evaluated as true or false in a structure.  -/
FirstOrder.Language.Sentence.Realize : {L : FirstOrder.Language} → (M : Type w) → [L.Structure M] → L.Sentence → Prop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.cones_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (X : Cᵒᵖ),
  F.cones.obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_set_nonempty_of_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n → {n | G.Colorable n}.Nonempty
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.mul_left : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] (b : σ → MvPowerSeries τ S)
  {a : σ → MvPowerSeries τ S}, MvPowerSeries.HasSubst a → MvPowerSeries.HasSubst (b * a)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDedekindDomain A] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A),
  IsPrincipalIdealRing ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Init.Data.Array.Basic
List.getElem!_toArray : ∀ {α : Type u} [inst : Inhabited α] {xs : List α} {i : ℕ}, xs.toArray[i]! = xs[i]!
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Iic_iff_integrableOn_Iio : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Iic_iff_integrableOn_Iio._auto_1 →
    (MeasureTheory.IntegrableOn f (Set.Iic b) μ ↔ MeasureTheory.IntegrableOn f (Set.Iio b) μ)
-- Init.Data.Format.Basic
Std.instToFormatString : Std.ToFormat String
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Given functors `F₁ : C₁ ⥤ D₁`, `F₂ : C₂ ⥤ D₂`, `F₃ : C₃ ⥤ D₃`
and `G : D₁ × D₂ × D₃ ⥤ E`, this is the isomorphism between
`curry₃.obj (F₁.prod (F₂.prod F₃) ⋙ G) : C₁ ⥤ C₂ ⥤ C₃ ⥤ E`
and `F₁ ⋙ curry₃.obj G ⋙ ((whiskeringLeft₂ E).obj F₂).obj F₃`.  -/
CategoryTheory.Functor.curry₃ObjProdComp : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_9} →
              [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
                [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
                    [inst_3 : CategoryTheory.Category.{v_6, u_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_7, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_8, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_9, u_9} E] →
                            (F₁ : CategoryTheory.Functor C₁ D₁) →
                              (F₂ : CategoryTheory.Functor C₂ D₂) →
                                (F₃ : CategoryTheory.Functor C₃ D₃) →
                                  (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E) →
                                    CategoryTheory.Functor.curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G) ≅
                                      F₁.comp
                                        ((CategoryTheory.Functor.curry₃.obj G).comp
                                          (((CategoryTheory.Functor.whiskeringLeft₂ E).obj F₂).obj F₃))
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- If the normalized versions of finite measures converge weakly and their total masses
also converge, then the finite measures themselves converge weakly.  -/
MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.FiniteMeasure Ω}
  [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto (fun i => (μs i).normalize) F (nhds μ.normalize) →
    Filter.Tendsto (fun i => (μs i).mass) F (nhds μ.mass) → Filter.Tendsto μs F (nhds μ)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.lift_mk' : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ M} (HN : N ≤ φ.ker) (g : G), (QuotientAddGroup.lift N φ HN) ↑g = φ g
-- Lean.Elab.Tactic.LibrarySearch
Lean.Elab.LibrarySearch.elabExact?Term : Lean.Elab.Term.TermElab
-- Mathlib.SetTheory.ZFC.Class
Class.mem_irrefl : ∀ (x : Class.{u_1}), x ∉ x
-- Lean.Server.CodeActions.Basic
/-- Get a `CodeActionProvider` from a declaration name.  -/
_private.Lean.Server.CodeActions.Basic.0.Lean.Server.evalCodeActionProvider : {M : Type → Type} →
  [Lean.MonadEnv M] →
    [Lean.MonadOptions M] → [Lean.MonadError M] → [Monad M] → Lean.Name → M Lean.Server.CodeActionProvider
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.congr_simp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommSemiring R] (A A_1 : Matrix n n R), A = A_1 → A.Nonsingular = A_1.Nonsingular
-- Init.System.Platform
/-- Checks whether the current platform is macOS.
 -/
System.Platform.getIsOSX : Unit → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.arithShiftRight.sizeOf_spec : ∀ {m n : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n),
  sizeOf (lhs.arithShiftRight rhs) = 1 + sizeOf m + sizeOf n + sizeOf lhs + sizeOf rhs
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- `HasPointwiseRightKanExtensionAt` is invariant when we replace `L` and `F` by isomorphic
functors.  -/
CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_natIso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} {Y : D} (e₁ : L ≅ L') (e₂ : F ≅ F'),
  L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F' Y
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
/-- A property of objects satisfies `P.IsClosedUnderKernels` if whenever `X` and `Y`
satisfy `P`, all kernels of morphisms from `X` to `Y` satisfy `P`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderKernels : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A convenience class similar to `UpgradedPolishSpace`. No instance should be registered.
Instead one should use `letI := upgradeStandardBorel α`.  -/
UpgradedStandardBorel : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `c` is a pullback cone for `p₁` and `p₂`  -/
CategoryTheory.EquivalenceRelation.c : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → CategoryTheory.EquivalenceRelation p₁ p₂ → CategoryTheory.Limits.PullbackCone p₂ p₁
-- Init.Data.String.Termination
String.Slice.Pos.next?.eq_1 : ∀ {s : String.Slice} (pos : s.Pos), pos.next? = if h : pos = s.endPos then none else some (pos.next h)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The Fourier transform of line derivative in direction `m` is given by multiplication of
`(2 * π * Complex.I) • (inner ℝ · m)` with the Fourier transform.  -/
TemperedDistribution.fourier_lineDerivOp_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : TemperedDistribution E F) (m : E),
  FourierTransform.fourier (LineDeriv.lineDerivOp m f) =
    (2 * ↑Real.pi * Complex.I) •
      (TemperedDistribution.smulLeftCLM F fun x => ↑(inner ℝ x m)) (FourierTransform.fourier f)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toDualProd_mono : ∀ {α : Type u_1} [inst : Preorder α], Monotone NonemptyInterval.toDualProd
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert!_eq_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} (h : l.Balanced),
  Std.DTreeMap.Internal.Impl.insert! k v l = Std.DTreeMap.Internal.Impl.insertₘ k v l h
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_fromOpenSubsetsGlue_apply : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : J)
  (x : ↑((TopCat.GlueData.ofOpenSubsets U).U i)),
  (CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U))
      ((CategoryTheory.ConcreteCategory.hom ((TopCat.GlueData.ofOpenSubsets U).ι i)) x) =
    (CategoryTheory.ConcreteCategory.hom (U i).inclusion') x
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocMod hp (a + m • p) b = toIocMod hp a b + m • p