mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.Const.alter!.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((sz : ℕ) →
              (k' : α) →
                (v' : β) →
                  (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')) →
            motive t
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulatedClosed₂],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₃ → P.isoClosure T.obj₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_filter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.filter f t).size ≤ t.size
-- Lean.Parser.Command
/-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type`  -/
Lean.Parser.Command.declSig : Lean.Parser.Parser
-- Init.Data.Int.Lemmas
Int.subNatNat_add_right : ∀ {m n : ℕ}, Int.subNatNat m (m + n + 1) = Int.negSucc n
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_div_bot : ∀ {M : Type u_4} (f : ℕ → M) {m n : ℕ} [inst : CommGroup M],
  m < n → (∏ i ∈ Finset.Ico m n, f i) / f m = ∏ i ∈ Finset.Ico (m + 1) n, f i
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.fst_comp_inl : ∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β],
  (LinearOrderedCommGroupWithZero.fst α β).comp (LinearOrderedCommGroupWithZero.inl α β) = OrderMonoidWithZeroHom.id α
-- Init.Data.Int.Compare
Int.lt_or_eq_of_le : ∀ {n m : ℤ}, n ≤ m → n < m ∨ n = m
-- Aesop.Tree.Data
Aesop.Iteration.instDecidableRelLe : DecidableRel fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Algebra.Hom
AlgHom.End_toOne_one : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], 1 = AlgHom.id R A
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.isThetaTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x → Topology.IsInducing ⇑f' → (fun x_1 => f x_1 - f x) =Θ[𝕜; nhds x] fun x_1 => x_1 - x
-- Lean.Language.Basic
/-- `MessageLog` with interactive diagnostics.

Can be created using `Diagnostics.empty` or `Diagnostics.ofMessageLog`.
 -/
Lean.Language.Snapshot.Diagnostics : Type
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommRingObjCat C),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (toDerivation :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤))
  (left_invariant'' :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation) = (Derivation.evalAt g) toDerivation)
  (toDerivation_1 :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤))
  (left_invariant''_1 :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation_1) = (Derivation.evalAt g) toDerivation_1),
  ({ toDerivation := toDerivation, left_invariant'' := left_invariant'' } =
      { toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 }) =
    (toDerivation = toDerivation_1)
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_unique : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ⊓ y ⊔ z = x → x ⊓ y ⊓ z = ⊥ → x \ y = z
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.abs : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a₀ : (MvQPF.P F).A)
  (f'₀ : ((MvQPF.P F).drop.B a₀).Arrow α) (f₀ : (MvQPF.P F).last.B a₀ → (MvQPF.P F).W α) (a₁ : (MvQPF.P F).A)
  (f'₁ : ((MvQPF.P F).drop.B a₁).Arrow α) (f₁ : (MvQPF.P F).last.B a₁ → (MvQPF.P F).W α),
  MvQPF.abs ⟨a₀, (MvQPF.P F).appendContents f'₀ f₀⟩ = MvQPF.abs ⟨a₁, (MvQPF.P F).appendContents f'₁ f₁⟩ →
    MvQPF.WEquiv ((MvQPF.P F).wMk a₀ f'₀ f₀) ((MvQPF.P F).wMk a₁ f'₁ f₁)
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.of_dvd_right : ∀ {a b₁ b₂ : ℕ}, b₁ ∣ b₂ → a.Coprime b₂ → a.Coprime b₁
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.mk.inj : ∀ {name url cmd : String} {query : String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult)}
  {queryNum : Lean.CoreM ℕ} {name_1 url_1 cmd_1 : String}
  {query_1 : String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult)} {queryNum_1 : Lean.CoreM ℕ},
  { name := name, url := url, cmd := cmd, query := query, queryNum := queryNum } =
      { name := name_1, url := url_1, cmd := cmd_1, query := query_1, queryNum := queryNum_1 } →
    name = name_1 ∧ url = url_1 ∧ cmd = cmd_1 ∧ query = query_1 ∧ queryNum = queryNum_1
-- Lean.DocString.Types
Lean.Doc.Inline.text.injEq : ∀ {i : Type u} (string string_1 : String),
  (Lean.Doc.Inline.text string = Lean.Doc.Inline.text string_1) = (string = string_1)
-- Init.Internal.Order.Basic
Lean.Order.instPartialOrderReaderT : {m : Type u_1 → Type u_2} →
  {ρ α : Type u_1} → [inst : Lean.Order.PartialOrder (m α)] → Lean.Order.PartialOrder (ReaderT ρ m α)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (x : M), (IsLocalizedModule.lift S f g h) (f x) = g x
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instInhabited.eq_1 : ∀ {α : Type u} [inst : Group α], GroupTopology.instInhabited = { default := ⊤ }
-- Mathlib.Order.Category.PartOrd
/-- Typecheck a `OrderHom` as a morphism in `PartOrd`.  -/
PartOrd.ofHom : {X Y : Type u} →
  [inst : PartialOrder X] →
    [inst_1 : PartialOrder Y] → (X →o Y) → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Aesop.Util.Basic
/-- Register a "Try this" suggestion for a tactic sequence.

It works when the tactic to replace appears on its own line:

```lean
by
  aesop?
```

It doesn't work (i.e., the suggestion will appear but in the wrong place) when
the tactic to replace is preceded by other text on the same line:

```lean
have x := by aesop?
```

The `Try this:` suggestion in the infoview is not correctly formatted, but
there's nothing we can do about this at the moment.
 -/
Aesop.addTryThisTacticSeqSuggestion : Lean.Syntax → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → optParam (Option Lean.Syntax) none → Lean.MetaM Unit
-- Mathlib.RingTheory.Polynomial.Hermite.Gaussian
Polynomial.hermite_eq_deriv_gaussian : ∀ (n : ℕ) (x : ℝ),
  (Polynomial.aeval x) (Polynomial.hermite n) =
    (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  (hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto_77✝) (hf0 : autoParam (f 0 = 0) _auto_79✝)
  (ha : autoParam (p a) _auto_85✝),
  cfcₙ f a = (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯, map_zero' := hf0 }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceOfNatLT : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Set.Basic
SetCoe.exists : ∀ {α : Type u} {s : Set α} {p : ↑s → Prop}, (∃ x, p x) ↔ ∃ x, ∃ (h : x ∈ s), p ⟨x, h⟩
-- Mathlib.Data.Num.Lemmas
Num.cast_le : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {m n : Num}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.LinearAlgebra.Ray
sameRay_neg_smul_right_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M} {r : R},
  SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
-- Init.Data.UInt.Lemmas
UInt16.toUInt16_toUInt32 : ∀ (n : UInt16), n.toUInt32.toUInt16 = n
-- Mathlib.Algebra.Group.Prod
Prod.instSemigroup : {M : Type u_3} → {N : Type u_4} → [Semigroup M] → [Semigroup N] → Semigroup (M × N)
-- Init.Data.Order.Lemmas
Std.instAssociativeMinOfIsLinearOrderOfLawfulOrderMin : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α], Std.Associative min
-- Init.Data.List.Attach
/-- “Attaches” the proof that the elements of `l` are in fact elements of `l`, producing a new list with
the same elements but in the subtype `{ x // x ∈ l }`.

`O(1)`.

This function is primarily used to allow definitions by [well-founded
recursion](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=well-founded-recursion) that use higher-order functions (such as
`List.map`) to prove that an value taken from a list is smaller than the list. This allows the
well-founded recursion mechanism to prove that the function terminates.
 -/
List.attach : {α : Type u_1} → (l : List α) → List { x // x ∈ l }
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  CategoryTheory.CategoryStruct.comp (L.map φ.s) (φ.map L hL) = L.map φ.f
-- Mathlib.GroupTheory.OrderOfElement
powCoprime_symm_apply : ∀ {n : ℕ} {G : Type u_6} [inst : Group G] (h : (Nat.card G).Coprime n) (g : G),
  (powCoprime h).symm g = g ^ (Nat.card G).gcdB n
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The `n`-cocycles `Zⁿ(G, A)` of a `k`-linear `G`-representation `A`, i.e. the kernel of the
`n`th differential in the complex of inhomogeneous cochains.  -/
groupCohomology.cocycles : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ℕ → ModuleCat k
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.obj.match_1.splitter : (motive : Fin 2 → Sort u_1) →
  (x : Fin 2) → ((isLt : 0 < 2) → motive ⟨0, isLt⟩) → ((isLt : 1 < 2) → motive ⟨1, isLt⟩) → motive x
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This typeclass ensures that an `UpwardEnumerable α` instance is well-behaved.
 -/
Std.PRange.LawfulUpwardEnumerable : (α : Type u) → [Std.PRange.UpwardEnumerable α] → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `sum_apply`. -/
QuadraticMap.sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.Logic.Function.Basic
/-- The property of a binary function `f : α → β → γ` being injective.
Mathematically this should be thought of as the corresponding function `α × β → γ` being injective.
 -/
Function.Injective2 : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α → β → γ) → Prop
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iio_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n),
  ∑ i < a.castSucc, f i = ∑ i < a, f i.castSucc
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` creates limits if it creates limits of shape `J` for any `J`.  -/
CategoryTheory.CreatesLimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
-- Mathlib.CategoryTheory.EpiMono
/-- There is a splitting  -/
CategoryTheory.IsSplitMono.exists_splitMono : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsSplitMono f],
  Nonempty (CategoryTheory.SplitMono f)
-- Mathlib.Topology.Algebra.ConstMulAction
Specializes.const_smul : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α] {x y : α},
  x ⤳ y → ∀ (c : M), (c • x) ⤳ (c • y)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.comp 1 = Polynomial.C (Polynomial.eval 1 p)
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift for commutative additive groups is additive.
 -/
AddCommGrpCat.uliftFunctor_additive : AddCommGrpCat.uliftFunctor.Additive
-- Mathlib.GroupTheory.DivisibleHull
/-- Forward direction of `archimedeanClassOrderIso`.  -/
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.archimedeanClassOrderHom : (M : Type u_2) →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] → ArchimedeanClass M →o ArchimedeanClass (DivisibleHull M)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.inv_nhdsNE : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {a : G},
  (nhdsWithin a {a}ᶜ)⁻¹ = nhdsWithin a⁻¹ {a⁻¹}ᶜ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.image_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β),
  ⇑e '' ⇑e ⁻¹' s = s
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instUniformSpace : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : UniformSpace F] → [IsUniformAddGroup F] → UniformSpace (E [⋀^ι]→L[𝕜] F)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C)
  (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
      CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m)
  {U X : C} (m : U ⟶ X) (x : CategoryTheory.Mono m),
  (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ m = χ m
-- Mathlib.Lean.Json
Lean.instToJsonPUnit_mathlib.toJson : PUnit.{u_1} → Lean.Json
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.toList_iter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.iter.toList = m.toList
-- Std.Time.Date.PlainDate
/-- Returns the week of the month for the given `PlainDate`, where weeks start on `firstDay`.
The first partial week containing day 1 is week 1, so weeks may span fewer than 7 days.
 -/
Std.Time.PlainDate.weekOfMonth : Std.Time.PlainDate → optParam Std.Time.Weekday Std.Time.Weekday.monday → Std.Time.Week.Ordinal
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_smul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {S : Type u_5}
  [inst_8 : DistribSMul S F] [inst_9 : SMulCommClass 𝕜₂ S F] [inst_10 : ContinuousConstSMul S F] {c : S}
  {f : E →SL[σ] F}, ContinuousLinearMapWOT.ofCLM (c • f) = c • ContinuousLinearMapWOT.ofCLM f
-- Mathlib.Combinatorics.Derangements.Basic
/-- Derangements on a subtype are equivalent to permutations on the original type where points are
fixed iff they are not in the subtype.  -/
derangements.subtypeEquiv : {α : Type u_1} →
  (p : α → Prop) →
    [DecidablePred p] → ↑(derangements (Subtype p)) ≃ { f // ∀ (a : α), ¬p a ↔ a ∈ Function.fixedPoints ⇑f }
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_prodAssoc : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : TopologicalSpace M₁] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃],
  ⇑(ContinuousLinearEquiv.prodAssoc R M₁ M₂ M₃) = ⇑(Equiv.prodAssoc M₁ M₂ M₃)
-- Mathlib.NumberTheory.Divisors
Nat.self_notMem_properDivisors : ∀ {n : ℕ}, n ∉ n.properDivisors
-- Batteries.Data.Random.MersenneTwister
/-- Tempering shift parameters (`u`, `s`, `t`, `l`).  -/
Batteries.Random.MersenneTwister.Config.temperingShifts : Batteries.Random.MersenneTwister.Config → ℕ × ℕ × ℕ × ℕ
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.incl_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (x : ↥I), I.incl x = ↑x
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.map_rangeS : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (g : S →+* T) (f : R →+* S), Subsemiring.map g f.rangeS = (g.comp f).rangeS
-- Init.Data.Array.Extract
Array.extract_append_extract : ∀ {α : Type u_1} {as : Array α} {i j k : ℕ}, as.extract i j ++ as.extract j k = as.extract (min i j) (max j k)
-- Init.Data.List.Lemmas
List.head?_eq_none_iff : ∀ {α : Type u_1} {l : List α}, l.head? = none ↔ l = []
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.symm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Mathlib.Analysis.Calculus.VectorField
/-- Variant of `lieBracketWithin_eventually_congr_set` where one requires the sets to coincide only
in the complement of a point.  -/
VectorField.lieBracketWithin_eventually_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → VectorField.lieBracketWithin 𝕜 V W s =ᶠ[nhds x] VectorField.lieBracketWithin 𝕜 V W t
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.val_step_takeWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  ↑(Std.Iter.takeWhile P it).step =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      match P out with
      | true => Std.IterStep.yield (Std.Iter.takeWhile P it') out
      | false => Std.IterStep.done
    | Std.IterStep.skip it' => Std.IterStep.skip (Std.Iter.takeWhile P it')
    | Std.IterStep.done => Std.IterStep.done
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie subalgebra inherits module structures from `L`.  -/
LieSubalgebra.instModuleSubtypeMemOfIsScalarTower : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {R₁ : Type u_1} →
            [inst_3 : Semiring R₁] →
              [inst_4 : SMul R₁ R] →
                [inst_5 : Module R₁ L] → [IsScalarTower R₁ R L] → (L' : LieSubalgebra R L) → Module R₁ ↥L'
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.η_ε_assoc : ∀ {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) [self : F.Monoidal] {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) h) =
    h
-- Init.Data.SInt.Basic
instToStringInt8 : ToString Int8
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- A square matrix over a `*`-semiring whose entries are unitary and whose rows and columns are
orthogonal with respect to the conjugate transpose:
`A * Aᴴ = n • 1` and `Aᴴ * A = n • 1`.

Over a commutative ring in which the order is regular, the one-sided condition from
[Definition 2.3.1][deLauneyFlannery2011] implies this predicate by
`IsHadamard.of_mul_conjTranspose`; over a ring with trivial star (e.g. `ℝ`, `ℤ`), the entry
condition becomes `A i j = 1 ∨ A i j = -1`. Over `ℂ`, the entry condition becomes `‖A i j‖ = 1`,
generalizing the fourth-root complex Hadamard matrices of
[Definition 2.7.1][deLauneyFlannery2011].  -/
Matrix.IsHadamard : {n : Type u_2} →
  {R : Type u_3} → [Fintype n] → [DecidableEq n] → [inst : Semiring R] → [StarRing R] → Matrix n n R → Prop
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biprodIsoProd_inv_comp_snd : ∀ (G H : AddCommGrpCat),
  CategoryTheory.CategoryStruct.comp (G.biprodIsoProd H).inv CategoryTheory.Limits.biprod.snd =
    AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H)
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- `AdicCauchySequence I R` is a subring of `ℕ → R`.  -/
AdicCompletion.AdicCauchySequence.subring : {R : Type u_1} → [inst : CommRing R] → Ideal R → Subring (ℕ → R)
-- Init.Core
not_eq_of_beq_eq_false : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {a b : α}, (a == b) = false → ¬a = b
-- Mathlib.GroupTheory.Nilpotent
/-- A group `G` is virtually nilpotent if it has a nilpotent cofinite subgroup `N`.  -/
Group.IsVirtuallyNilpotent : (G : Type u_1) → [Group G] → Prop
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.uliftFunctor.eq_1 : GrpCat.uliftFunctor =
  { obj := fun X => GrpCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      GrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((GrpCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.dualEquiv_functor : FinBoolAlg.dualEquiv.functor = FinBoolAlg.dual
-- Mathlib.Data.Fin.Tuple.Sort
/-- If a permutation `f ∘ σ` of the tuple `f` is not the same as `f ∘ sort f`, then `f ∘ σ`
has a pair of strictly decreasing entries.  -/
Tuple.antitone_pair_of_not_sorted' : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
  f ∘ ⇑σ ≠ f ∘ ⇑(Tuple.sort f) → ∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i