mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.filter : {α : Type u_1} → [inst : BEq α] → (α → Bool) → Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.aleph_mul_aleph0 : ∀ (o : Ordinal.{u_1}), Cardinal.aleph o * Cardinal.aleph0 = Cardinal.aleph o
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves the kernel of `h.g' : h.Q ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g' : ∀ {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} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {S : CategoryTheory.ShortComplex C} {h : S.RightHomologyData}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms} [self : h.IsPreservedBy F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair h.g' 0) F
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∈ t₂ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    e.functor.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.inverse.map f) (e.inverse.map g))
-- Mathlib.RingTheory.KrullDimension.Regular
Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] {x : R},
  IsSMulRegular M x →
    x ∈ (Module.annihilator R M).jacobson → Module.supportDim R (QuotSMulTop x M) + 1 = Module.supportDim R M
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.top_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X), ⊤.arrows f
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk.inj : ∀ {Γ : Type u_1} {inst : Inhabited Γ} {head : Γ} {left right : Turing.ListBlank Γ} {head_1 : Γ}
  {left_1 right_1 : Turing.ListBlank Γ},
  { head := head, left := left, right := right } = { head := head_1, left := left_1, right := right_1 } →
    head = head_1 ∧ left = left_1 ∧ right = right_1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g), c.op.pt = Opposite.op c.pt
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instLawfulUpwardEnumerableLTInt : Std.PRange.LawfulUpwardEnumerableLT ℤ
-- Mathlib.Analysis.Convex.AmpleSet
/-- Pre-images of ample sets under continuous affine equivalences are ample.  -/
AmpleSet.preimage : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] {E : Type u_2}
  [inst_3 : AddCommGroup E] [inst_4 : Module ℝ E] [inst_5 : TopologicalSpace E] {s : Set F},
  AmpleSet s → ∀ (L : E ≃ᴬ[ℝ] F), AmpleSet (⇑L ⁻¹' s)
-- Mathlib.Data.Set.Functor
/-- The `Set` functor is a monad.

This is not a global instance because it does not have computational content,
so it does not make much sense using `do` notation in general.

Moreover, this would cause monad-related coercions and monad lifting logic to become activated.
Either use `attribute [local instance] Set.monad` to make it be a local instance
or use `SetM.run do ...` when `do` notation is wanted.  -/
Set.monad : AlternativeMonad Set
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Icc_sdiff_Ioc_self`. -/
Finset.Icc_diff_Ioc_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → Finset.Icc a b \ Finset.Ioc a b = {a}
-- Mathlib.RingTheory.Spectrum.Prime.LTSeries
PrimeSpectrum.exist_mem_one_of_mem_two : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {p₁ p₀ p₂ : PrimeSpectrum R},
  p₀ < p₁ → p₁ < p₂ → ∀ {x : R}, x ∈ p₂.asIdeal → ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `tsub_add_tsub_comm` for the equality.  -/
add_tsub_add_le_tsub_add_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c d : α}
  [AddLeftMono α], a + b - (c + d) ≤ a - c + (b - d)
-- Mathlib.Data.Fintype.Card
Finset.card_univ_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α),
  (Finset.univ \ s).card = Fintype.card α - s.card
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.edges_subset : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₂.IsSubwalk p₁ → p₂.edges ⊆ p₁.edges
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- `Set.powersetCard α n` as a `SubMulAction` of `Finset α`.  -/
Set.powersetCard.subMulAction : (G : Type u_1) →
  [inst : Group G] →
    (α : Type u_2) → [inst_1 : MulAction G α] → ℕ → [inst_2 : DecidableEq α] → SubMulAction G (Finset α)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.instUnique.eq_1 : ∀ {M : Type u_16} {N : Type u_17} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Mul M] [inst_3 : Mul N],
  MulEquiv.instUnique = { default := MulEquiv.ofUnique, uniq := ⋯ }
-- Mathlib.Data.Int.Init
/-- Induction on integers: prove a proposition `p i` by proving the base case `p 0`,
the upwards induction step `p i → p (i + 1)` and the downwards induction step `p (-i) → p (-i - 1)`.

It is used as the default induction principle for the `induction` tactic.
 -/
Int.induction_on : ∀ {motive : ℤ → Prop} (i : ℤ),
  motive 0 → (∀ (i : ℕ), motive ↑i → motive (↑i + 1)) → (∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)) → motive i
-- Mathlib.Data.Rat.Floor
Rat.floor_cast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : ℚ),
  ⌊↑x⌋ = ⌊x⌋
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.map_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : Ring S] {Λ₀ : Type u_4} [inst_3 : LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀)
  (f : R →+* S) (x : WithVal v), (WithVal.map v w f) x = WithVal.toVal w (f x.ofVal)
-- Mathlib.Topology.DiscreteQuotient
/-- The (locally constant) function from the discrete quotient associated to a locally constant
function.  -/
LocallyConstant.lift : {α : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] → (f : LocallyConstant X α) → LocallyConstant (Quotient f.discreteQuotient.toSetoid) α
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.kind : Lean.SyntaxNodeKind → Lean.Parser.ParserExtension.OLeanEntry
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapId_hom_app_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T) (X : CategoryTheory.Under Y),
  ((CategoryTheory.Under.mapId Y).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Lean.Data.Lsp.Basic
Lean.Lsp.Command.mk.sizeOf_spec : ∀ (title command : String) (arguments? : Option (Array Lean.Json)),
  sizeOf { title := title, command := command, arguments? := arguments? } =
    1 + sizeOf title + sizeOf command + sizeOf arguments?
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_genEigenspace_zero : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, x ∈ (f.genEigenspace μ) 0 ↔ x = 0
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.apply_eq_zero_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) [Nontrivial R] (a : ℤ),
  χ ↑a = 0 ↔ ¬IsCoprime a ↑n
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeAddGroup α), x.norm = x.toWord.length
-- Mathlib.Topology.Algebra.Group.Torsor
/-- The map `v ↦ v +ᵥ p` as a homeomorphism between `V` and `P`.  -/
Homeomorph.vaddConst : {V : Type u_1} →
  {P : Type u_2} →
    [inst : AddGroup V] →
      [inst_1 : TopologicalSpace V] →
        [inst_2 : AddTorsor V P] → [inst_3 : TopologicalSpace P] → [IsTopologicalAddTorsor P] → P → V ≃ₜ P
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffAt.clm_postcomp : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {f : M → F₂ →L[𝕜] F₃}
  {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n
      (fun y => ContinuousLinearMap.postcomp F₁ (f y)) x
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv
      (CategoryTheory.Limits.pullback.snd f g) =
    TypeCat.ofHom fun p => (↑p).2
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den.eq_1 : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype m] [inst_1 : Fintype n] (A : Matrix m n ℚ),
  A.den = Finset.univ.lcm fun P => (A P.1 P.2).den
-- Mathlib.Topology.UniformSpace.Path
Path.uniformContinuous : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X} (γ : Path x y), UniformContinuous ⇑γ
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma.eq_1 : ∀ (s : ℝ), Real.Gamma s = (Complex.Gamma ↑s).re
-- Mathlib.Algebra.Regular.SMul
/-- Any power of an `M`-regular element is `M`-regular.  -/
IsSMulRegular.pow : ∀ {R : Type u_1} {M : Type u_3} {a : R} [inst : Monoid R] [inst_1 : MulAction R M] (n : ℕ),
  IsSMulRegular M a → IsSMulRegular M (a ^ n)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Forward direction of the unit.  -/
CategoryTheory.OverPresheafAux.unitForward : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (η : F ⟶ A) →
        (X : C) →
          CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X →
            F.obj (Opposite.op X)
-- Mathlib.Data.Sum.Interval
Sum.Icc_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ : α) (b₂ : β), Finset.Icc (Sum.inl a₁) (Sum.inr b₂) = ∅
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_eq' : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Fintype σ]
  (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R),
  MvPolynomial.eval₂ g X f = ∑ d ∈ f.support, g (MvPolynomial.coeff d f) * ∏ i, X i ^ d i
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A left homology map data for a morphism of short complexes in the opposite category
induces a right homology map data in the original category.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} →
              CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.ShortComplex.unopMap φ) h₂.unop h₁.unop
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
CategoryTheory.Precoverage.subsheafify_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C)
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))) (U : Cᵒᵖ),
  (K.subsheafify 𝒮).obj U = {x | K.SubsheafClosure 𝒮 (Opposite.unop U) x}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_minKey!_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, compare (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey! t.minKey! = Ordering.eq
-- Mathlib.Algebra.Group.PUnit
PUnit.instMul_mathlib : Mul PUnit.{u_1 + 1}
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The space of tempered distribution is the space of continuous linear maps from the Schwartz to
a normed space, equipped with the topology of pointwise convergence.  -/
SchwartzMap.«term𝓢'(_,_)» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
mapClusterPt_one_atTop_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x : G),
  MapClusterPt 1 Filter.atTop fun x_1 => x ^ x_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter m₂ ⋯) k =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then Std.DTreeMap.Internal.Impl.Const.get! m₁ k else default
-- Mathlib.Topology.Category.TopPair
/-- The functor from topological spaces to topological pairs that sends a space X to the identity
morphism on X.  -/
TopPair.diag : CategoryTheory.Functor TopCat TopPair
-- Mathlib.Analysis.Asymptotics.Defs
/-- The Landau notation `f =o[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by an arbitrarily small constant
multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` tends to `0` along `l`, modulo division by zero
issues that are avoided by this definition.  -/
Asymptotics.«term_=o[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.ContDiff.Operations
OpenPartialHomeomorph.contDiffOn_restrContDiff_target : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ↑⊤),
  ContDiffOn 𝕜 n (↑f.symm) (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).target
-- Mathlib.RingTheory.Derivation.Basic
Derivation.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  {D1 D2 : Derivation R A M}, D1 = D2 ↔ ∀ (a : A), D1 a = D2 a
-- Mathlib.Order.Filter.Basic
Filter.biInf_sets_eq : ∀ {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β},
  DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) s → s.Nonempty → (⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α},
  (Std.TreeMap.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x t[x]).isSome
-- Init.GrindInstances.ToInt
Int32.size.eq_1 : Int32.size = 4294967296
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.whiskerRight_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : CategoryTheory.Bicategory.Pith B} {f g : a ⟶ b}
  (f_1 : f ⟶ g) (y : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRight f_1 y).iso.hom = CategoryTheory.Bicategory.whiskerRight f_1.iso.hom y.of
-- Mathlib.Algebra.Order.Hom.Basic
AddGroupSeminormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : AddGroup α] [inst_1 : AddCommMonoid β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [toSubadditiveHomClass : SubadditiveHomClass F α β],
  (∀ (f : F), f 0 = 0) → (∀ (f : F) (a : α), f (-a) = f a) → AddGroupSeminormClass F α β
-- Mathlib.Order.RelIso.Basic
/-- A `RelHom` sends related elements to related elements  -/
RelHom.map_rel' : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (self : r →r s) {a b : α},
  r a b → s (self.toFun a) (self.toFun b)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Data.Multiset.AddSub
Multiset.zero_sub : ∀ {α : Type u_1} [inst : DecidableEq α] (t : Multiset α), 0 - t = 0
-- Mathlib.Data.String.Lemmas
String.leftpad_prefix : ∀ (n : ℕ) (c : Char) (s : String), (String.replicate (n - s.length) c).IsPrefix (String.leftpad n c s)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X Y : C) (f : J → C),
  (CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X))
        (CategoryTheory.leftDistributor Y f) ≪≫
      CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj Y (f j)) =
    (CategoryTheory.MonoidalCategoryStruct.associator X Y (⨁ f)).symm ≪≫
      CategoryTheory.leftDistributor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f ≪≫
        CategoryTheory.Limits.biproduct.mapIso fun x => CategoryTheory.MonoidalCategoryStruct.associator X Y (f x)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_ciSup_eq_left : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {b : β} {f : (x : β) → x = b → α},
  ⨆ x, ⨆ (h : x = b), f x h = f b ⋯
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instIsSMulApplyForall : ∀ {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : DistribSMul S M₂] [inst_6 : SMulCommClass R S M₂],
  IsSMulApply S (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
/-- The type of absolutely convex open sets.  -/
AbsConvexOpenSets : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [TopologicalSpace E] → [AddCommMonoid E] → [SeminormedRing 𝕜] → [SMul 𝕜 E] → [PartialOrder 𝕜] → Type (max 0 u_2)
-- Lean.Parser.Term
Lean.Parser.Term.letOptPostponeValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Logic.Equiv.Basic
Function.Involutive.coe_toPerm : ∀ {α : Sort u_1} {f : α → α} (h : Function.Involutive f), ⇑(Function.Involutive.toPerm f h) = f
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Polynomial.Monic.quotient_isIntegral : ∀ {S : Type u_4} [inst : CommRing S] {g : Polynomial S},
  g.Monic →
    ∀ {I : Ideal (Polynomial S)}, g ∈ I → ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S (Polynomial S))).IsIntegral
-- Mathlib.Data.List.AList
_private.Mathlib.Data.List.AList.0.AList.insertRec.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : AList β → Sort u_3) (c : Sigma β) (l : List (Sigma β))
  (h : (c :: l).NodupKeys) (h_1 : (nodupKeys : [].NodupKeys) → motive { entries := [], nodupKeys := nodupKeys })
  (h_2 :
    (c : Sigma β) → (l : List (Sigma β)) → (h : (c :: l).NodupKeys) → motive { entries := c :: l, nodupKeys := h }),
  (match { entries := c :: l, nodupKeys := h } with
    | { entries := [], nodupKeys := nodupKeys } => h_1 nodupKeys
    | { entries := c :: l, nodupKeys := h } => h_2 c l h) =
    h_2 c l h
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.RwKind.valid.inj : ∀ {motiveTypeCorrect : Bool} {occ : Option ℕ} {motiveTypeCorrect_1 : Bool} {occ_1 : Option ℕ},
  Mathlib.Tactic.ClickSuggestions.RwKind.valid motiveTypeCorrect occ =
      Mathlib.Tactic.ClickSuggestions.RwKind.valid motiveTypeCorrect_1 occ_1 →
    motiveTypeCorrect = motiveTypeCorrect_1 ∧ occ = occ_1
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq : ∀ {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.IsEventuallyConstantTo i₀) [inst_2 : CategoryTheory.IsCofiltered J] (j j' : J) (α : j' ⟶ i₀) (β : j' ⟶ j),
  h.coneπApp j = CategoryTheory.CategoryStruct.comp (h.isoMap α ⋯).inv (F.map β)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope.eq_1 : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b : k), slope f a b = (b - a)⁻¹ • (f b -ᵥ f a)
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.reciprocalFactors_zero : DihedralGroup.reciprocalFactors 0 = [0]
-- Mathlib.CategoryTheory.Square
/-- the top-left morphism  -/
CategoryTheory.Square.Hom.τ₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {sq₁ sq₂ : CategoryTheory.Square C} → sq₁.Hom sq₂ → (sq₁.X₁ ⟶ sq₂.X₁)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_some_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.min? = some (t.minD fallback)
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.diagonal : ∀ {B : Type u_1} (self : CoxeterMatrix B) (i : B), self.M i i = 1
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the multiplicativity
of a multilinear map along the first variable.  -/
MultilinearMap.cons_smul : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
  (m : (i : Fin n) → M i.succ) (c : R) (x : M 0), f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_inj : ∀ {α : Type u_1} {s t : Set α} [inst : Fintype ↑s] [inst_1 : Fintype ↑t], s.toFinset = t.toFinset ↔ s = t
-- Batteries.Data.AssocList
Batteries.AssocList.forM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : α → β → m PUnit.{u_1 + 1}),
  Batteries.AssocList.forM f Batteries.AssocList.nil = pure PUnit.unit
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasSubgroup.eq_1 : ∀ {α : Type u_1} (F : Type u_2) [inst : NormedAddCommGroup F] (m : MeasurableSpace α) [inst_1 : MeasurableSpace α]
  (p : ENNReal) (μ : MeasureTheory.Measure α),
  MeasureTheory.lpMeasSubgroup F m p μ =
    { carrier := {f | MeasureTheory.AEStronglyMeasurable (↑↑f) μ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter_of_pairwise_eq_zero : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {f : κ → ι} {g : ι → M}
  {n : κ} {I : Finset κ},
  n ∈ I → ((↑I).Pairwise fun i j => f i = f j → g (f i) = 0) → ∑ j ∈ I with f j = f n, g (f j) = g (f n)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.recvSelector : {α : Type} → Std.CloseableChannel.Bounded✝ α → Std.Async.Selector (Option α)