mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rootD_lt : ∀ {self : Batteries.UnionFind} {x : ℕ}, self.rootD x < self.size ↔ x < self.size
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_zero_left : ∀ {R : Type u_1} [inst : CommRing R] (a : Polynomial R), Polynomial.wronskian 0 a = 0
-- Mathlib.Order.Filter.Defs
Filter.univ_mem : ∀ {α : Type u_1} {f : Filter α}, Set.univ ∈ f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.ofIso_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (e : M ≅ X),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.comap_map_mk' : ∀ {G : Type u} [inst : AddGroup G] (N H : AddSubgroup G) [inst_1 : N.Normal],
  AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.map (QuotientAddGroup.mk' N) H) = N ⊔ H
-- Mathlib.Algebra.Module.GradedModule
DirectSum.GdistribMulAction.toGMulAction : {ιA : Type u_1} →
  {ιB : Type u_2} →
    {A : ιA → Type u_3} →
      {M : ιB → Type u_4} →
        {inst : AddMonoid ιA} →
          {inst_1 : VAdd ιA ιB} →
            {inst_2 : GradedMonoid.GMonoid A} →
              {inst_3 : (i : ιB) → AddMonoid (M i)} →
                [self : DirectSum.GdistribMulAction A M] → GradedMonoid.GMulAction A M
-- Std.Http.Data.URI.Basic
/-- Attempts to create a normalized domain name from a string.
Returns `none` if the name is empty, longer than 255 characters, or any label violates DNS label
constraints.
 -/
Std.Http.URI.DomainName.ofString? : String → Option Std.Http.URI.DomainName
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x * a) ⁻¹' Set.Iic b = Set.Iic (b / a)
-- Mathlib.RingTheory.AdicCompletion.Basic
isPrecomplete_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsPrecomplete I M ↔
    ∀ (f : ℕ → M), (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- If `e : S₁ ≅ S₂` is an isomorphism of short complexes and `h₁ : RightHomologyData S₁`,
this is the right homology data for `S₂` deduced from the isomorphism.  -/
CategoryTheory.ShortComplex.RightHomologyData.ofIso : {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₂) → S₁.RightHomologyData → S₂.RightHomologyData
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_cpopLayer : ∀ {oldLen k w iterNum : ℕ} {oldLayer : BitVec (oldLen * w)} {newLayer : BitVec (iterNum * w)}
  (hold : 2 * (iterNum - 1) < oldLen),
  (∀ i < iterNum,
      BitVec.extractLsb' (i * w) w newLayer =
        BitVec.extractLsb' (2 * i * w) w oldLayer + BitVec.extractLsb' ((2 * i + 1) * w) w oldLayer) →
    (oldLayer.cpopLayer newLayer hold).getLsbD k =
      (BitVec.extractLsb' (2 * ((k - k % w) / w) * w) w oldLayer +
            BitVec.extractLsb' ((2 * ((k - k % w) / w) + 1) * w) w oldLayer).getLsbD
        (k % w)
-- Mathlib.Topology.Algebra.MulAction
ContinuousSMul.mk : ∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace X],
  (Continuous fun p => p.1 • p.2) → ContinuousSMul M X
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.map_eval_injective : ∀ (K : Type uK) (V : Type uV) [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], Function.Injective (Submodule.map (Module.Dual.eval K V))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertList_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ {m : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true}
        (contains : Std.Internal.List.containsKey k toInsert = true),
        Std.Internal.List.getKey k (Std.Internal.List.insertList l toInsert) m =
          Std.Internal.List.getKey k toInsert contains
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddSemigroup α], Colex.instAddSemigroup = { toAdd := Colex.instAdd, add_assoc := ⋯ }
-- Mathlib.SetTheory.ZFC.Class
ZFSet.choice_mem_aux : ∀ (x : ZFSet.{u}), ∅ ∉ x → ∀ y ∈ x, (Classical.epsilon fun z => z ∈ y) ∈ y
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_inf : ∀ {R : Type u} [inst : NonAssocSemiring R] {p p' : Subsemiring R} {x : R}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelOpUnop_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.kernelOpUnop f).hom =
    (CategoryTheory.Limits.kernel.lift f.op (CategoryTheory.Limits.cokernel.π f).op ⋯).unop
-- Mathlib.NumberTheory.FLT.Basic
/-- Statement of Fermat's Last Theorem over a given semiring with a specific exponent.  -/
FermatLastTheoremWith : (R : Type u_1) → [Semiring R] → ℕ → Prop
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_comp_cotangentComplex : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P'),
  Algebra.Extension.CotangentSpace.map f ∘ₗ P.cotangentComplex =
    ↑S P'.cotangentComplex ∘ₗ Algebra.Extension.Cotangent.map f
-- Mathlib.Data.Finset.Prod
Finset.diag_mono : ∀ {α : Type u_1}, Monotone Finset.diag
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Converts an element of `R` to an element of `WithVal v`.  -/
WithVal.toVal : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → R → WithVal v
-- Lean.Data.PrefixTree
Lean.PrefixTree : (α : Type u) → Type v → (α → α → Ordering) → Type (max u v)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Help the typechecker by converting an arrow in the fundamental groupoid of
a topological space back to a path in that space (i.e., `Path.Homotopic.Quotient`).  -/
FundamentalGroupoid.toPath : {X : TopCat} →
  {x₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj X)} → (x₀ ⟶ x₁) → Path.Homotopic.Quotient x₀.as x₁.as
-- Mathlib.Data.Num.Basic
/-- Subtraction of two `Num`s, producing an `Option Num`.  -/
Num.psub : Num → Num → Option Num
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.trans.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (h1 : M ≃+ N)
  (h2 : N ≃+ P), h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- `HasRankNullity.{u}` is a class of rings satisfying
1. Every `R`-module `M : Type u` has a linear independent subset of cardinality `Module.rank R M`.
2. `rank (M ⧸ N) + rank N = rank M` for every `R`-module `M : Type u` and every `N : Submodule R M`.

Usually such a ring satisfies `HasRankNullity.{w}` for all universes `w`, and the universe
argument is there because of technical limitations to universe polymorphism.

See `DivisionRing.hasRankNullity` and `IsDomain.hasRankNullity`.
 -/
HasRankNullity : (R : Type v) → [inst : Ring R] → Prop
-- Mathlib.Order.IsNormal
/-- A normal function between well-orders is a strictly monotonic continuous function.  -/
Order.IsNormal : {α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [LinearOrder β] → (α → β) → Prop
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
_private.Mathlib.NumberTheory.ModularForms.LevelOne.Basic.0.ModularFormClass.cuspFunction_eqOn_const_of_nonpos_wt : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k],
  k ≤ 0 →
    ∀ (f : F),
      Set.EqOn (UpperHalfPlane.cuspFunction 1 ⇑f) (Function.const ℂ (UpperHalfPlane.cuspFunction 1 (⇑f) 0))
        (Metric.ball 0 1)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit : ∀ {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} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal], CategoryTheory.NatTrans.IsMonoidal adj.unit
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_cramer : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Fintype n] [inst_3 : DecidableEq n] [inst_4 : CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R}
  {B : X → n → R}, Continuous A → Continuous B → Continuous fun x => (A x).cramer (B x)
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.distrib : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C) (f g h k : X ⟶ Y),
  CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y
      (CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y f g)
      (CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y h k) =
    CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y
      (CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y f h)
      (CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd X Y g k)
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_zero : ∀ (a : ℤ), a.tmod 0 = a
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_gc : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  GaloisConnection (⇑OrderDual.toDual ∘ Submodule.dualAnnihilator) (Submodule.dualCoannihilator ∘ ⇑OrderDual.ofDual)
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.t_inv : ∀ (h : TopCat.GlueData.MkCore) (i j : h.J) (x : ↥(h.V j i)),
  (CategoryTheory.ConcreteCategory.hom (h.t i j)) ((CategoryTheory.ConcreteCategory.hom (h.t j i)) x) = x
-- Mathlib.Topology.Compactness.Compact
/-- The indiscrete topology is compact  -/
instCompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [IndiscreteTopology X], CompactSpace X
-- Mathlib.GroupTheory.Torsion
AddEquiv.map_torsion : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] (e : G ≃+ H),
  AddSubgroup.map (↑e) (AddCommGroup.torsion G) = AddCommGroup.torsion H
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Construct a morphism `M ⟶ N` of `Comon C` from a map `f : M ⟶ N` and a `IsComonHom f`
instance.  -/
CategoryTheory.Comon.Hom.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Comon C} →
        (f : M.X ⟶ N.X) →
          autoParam
              (CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
              CategoryTheory.Comon.Hom.mk'._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.comul =
                  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                    (CategoryTheory.MonoidalCategoryStruct.tensorHom f f))
                CategoryTheory.Comon.Hom.mk'._auto_3 →
              M.Hom N
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.FG.finite : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [L.IsRelational] {S : L.Substructure M},
  S.FG → Finite ↥S
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- Given a fibered category `p : 𝒳 ⥤ 𝒫`, a morphism `f : R ⟶ S` and an object `a` lying over `S`,
then `pullbackMap` is a choice of a Cartesian morphism lying over `f` with codomain `a`.  -/
CategoryTheory.Functor.IsPreFibered.pullbackMap : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : p.IsPreFibered] →
            {R S : 𝒮} →
              {a : 𝒳} → (ha : p.obj a = S) → (f : R ⟶ S) → CategoryTheory.Functor.IsPreFibered.pullbackObj ha f ⟶ a
-- Mathlib.Order.Hom.Lattice
SupHom.coe_id : ∀ (α : Type u_2) [inst : Max α], ⇑(SupHom.id α) = id
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The functor `sheafPushforwardContinuous` corresponding to the identity functor
identifies to the identity functor.  -/
CategoryTheory.Functor.sheafPushforwardContinuousId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (A : Type u) →
      [inst_1 : CategoryTheory.Category.{t, u} A] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (CategoryTheory.Functor.id C).sheafPushforwardContinuous A J J ≅
            CategoryTheory.Functor.id (CategoryTheory.Sheaf J A)
-- Init.Data.List.SplitOn.Lemmas
/-- `splitOn x` is the left inverse of `intercalate [x]`, on the domain
consisting of each nonempty list of lists `ls` whose elements do not contain `x`  -/
List.splitOn_intercalate : ∀ {α : Type u_1} {ls : List (List α)} [inst : BEq α] [LawfulBEq α] (x : α),
  (∀ l ∈ ls, x ∉ l) → ls ≠ [] → List.splitOn x ([x].intercalate ls) = ls
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldrM_eq_foldrM_keys' : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((a : α) × β a)} {f : δ → α → m' δ} {init : δ},
  List.foldrM (fun a b => f b a.fst) init l = List.foldrM (fun a b => f b a) init (Std.Internal.List.keys l)
-- Mathlib.Order.Sublattice
Sublattice.supClosed : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α), SupClosed ↑L
-- Mathlib.Order.Interval.Set.ProjIcc
/-- Extend a function `[a, ∞) → β` to a map `α → β`.  -/
Set.IciExtend : {α : Type u_1} → {β : Type u_2} → [inst : LinearOrder α] → {a : α} → (↑(Set.Ici a) → β) → α → β
-- Mathlib.Data.List.Perm.Basic
List.perm_insertIdx_iff_of_le : ∀ {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ},
  m ≤ l₁.length → n ≤ l₂.length → ∀ (a : α), (l₁.insertIdx m a).Perm (l₂.insertIdx n a) ↔ l₁.Perm l₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tendsto_sin_pi_div_two : Filter.Tendsto Real.sin (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2))) (nhds 1)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_pos : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀], 0 < a → ∀ (n : ℕ), 0 < a ^ n
-- Init.Data.Float.Float32
/-- Computes the base-2 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`log2f`.
 -/
Float32.log2 : Float32 → Float32
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_nonpos_iff : ∀ {x : ℝ}, 0 ≤ x → (Real.log x ≤ 0 ↔ x ≤ 1)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.neg_algebraMap : ∀ {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {r t : R},
  -r = t → -(algebraMap R A) r = (algebraMap R A) t
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
discreteUniformity_iff_eq_bot : ∀ (X : Type u_1) [u : UniformSpace X], DiscreteUniformity X ↔ u = ⊥
-- Mathlib.Data.Set.Restrict
/-- If a function `f` is restricted to a set `t`, and `s ⊆ t`, this is the restriction to `s`.  -/
Set.domRestrict₂ : {α : Type u_1} → {π : α → Type u_6} → {s t : Set α} → s ⊆ t → ((a : ↑t) → π ↑a) → (a : ↑s) → π ↑a
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteMulSupport.zpow` -/
Function.HasFiniteMulSupport.fun_zpow : ∀ {α : Type u_1} {M : Type u_3} [inst : DivisionMonoid M] {f : α → M},
  Function.HasFiniteMulSupport f → ∀ (n : ℤ), Function.HasFiniteMulSupport fun i => f i ^ n
-- Mathlib.ModelTheory.Types
/-- **Alias** of `FirstOrder.Language.Theory.CompleteType.iInter_setOfPred_subset`. -/
FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {ι : Type u_1} (S : ι → (L.withConstants α).Theory),
  ⋂ i, {p | S i ⊆ ↑p} = {p | ⋃ i, S i ⊆ ↑p}
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.Integrable.measure_le_integral : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ᵐ[μ] f → ∀ {s : Set X}, (∀ x ∈ s, 1 ≤ f x) → μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.compl : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {G : SimpleGraph V} [inst_2 : DecidableRel G.Adj] {k : ℕ},
  G.IsRegularOfDegree k → Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_cons : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)),
  Std.Internal.List.minKey? (e :: l) =
    some
      (match Std.Internal.List.minKey? l with
      | none => e.fst
      | some w => if (compare e.fst w).isLE = true then e.fst else w)
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_def : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b x : α), (Equiv.swap a b) x = if x = a then b else if x = b then a else x
-- Lean.Meta.Tactic.Grind.EMatch
/-- `EMatchTheorem` being processed.  -/
Lean.Meta.Grind.EMatch.Context.thm : Lean.Meta.Grind.EMatch.Context → Lean.Meta.Grind.EMatchTheorem
-- Init.Data.Iterators.Basic
/-- `Productive α m` asserts that `IterM (α := α) m` terminates or emits a value after finitely many
skips. Technically, this means that the relation of plausible successors during skips is
well-founded.
Given this typeclass, termination proofs for well-founded recursion over an iterator `it` can use
`it.finitelyManySkips` as a termination measure.
 -/
Std.Iterators.Productive : (α : Type u_1) → (m : Type u_1 → Type u_2) → {β : Type u_1} → [Std.Iterator α m β] → Prop
-- Mathlib.Data.ZMod.Basic
ZMod.inv_zero : ∀ (n : ℕ), 0⁻¹ = 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.toDenselyNormedField : {K : semiOutParam (Type u_1)} → [self : RCLike K] → DenselyNormedField K
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toUInt32 = UInt32.ofNat n
-- Mathlib.Order.SuccPred.Archimedean
exists_succ_iterate_iff_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {a b : α},
  (∃ n, Order.succ^[n] a = b) ↔ a ≤ b
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.eq_1 : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] (s : ℝ) (p : ENNReal) [hp : Fact (1 ≤ p)]
  (f : TemperedDistribution E F),
  TemperedDistribution.MemSobolev s p f =
    ∃ f', (TemperedDistribution.besselPotential E F s) f = MeasureTheory.Lp.toTemperedDistribution f'
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.vadd : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → {α : Type u_3} → [VAdd α Y] → VAdd α (LocallyConstant X Y)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift.eq_1 : ∀ {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} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)),
  f.lift hg =
    { toFun := fun z => g (f.sec z).1 + ↑(-(IsAddUnit.liftRight (g.domRestrict S) hg) (f.sec z).2), map_zero' := ⋯,
      map_add' := ⋯ }
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.instInhabitedContext.default : Aesop.Script.DynStructureM.Context
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.iUnion_finset_leftRel_eq_univ_of_leftRel : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {t : Finset (DoubleCoset.Quotient ↑H ↑K)},
  Set.univ ⊆ ⋃ i ∈ t, Quot.mk ⇑(QuotientGroup.leftRel K) '' DoubleCoset.doubleCoset (Quotient.out i) ↑H ↑K →
    ⋃ q ∈ t, DoubleCoset.doubleCoset (Quotient.out q) ↑H ↑K = Set.univ
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_univ : ∀ (M : Type u_1) [inst : AddSemigroup M], Set.univ.addCentralizer = Set.addCenter M
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The morphism in `ShortComplex C` associated to a morphism in `ShortComplex Cᵒᵖ`  -/
CategoryTheory.ShortComplex.unopMap : {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₂) → (S₂.unop ⟶ S₁.unop)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C}
  (h_1 : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h)
      (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h_1) =
    CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i.1 i.2 i₁₂') h_1
-- Init.Data.UInt.Basic
instHModUInt64Nat : HMod UInt64 ℕ UInt64
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.clientInfo? : Lean.Lsp.InitializeParams → Option Lean.Lsp.ClientInfo
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  (α : LieModule.Weight K (↥H) L), IsCompl LieModule.Weight.ker (K ∙ LieAlgebra.IsKilling.coroot α)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertₘ.eq_1 : ∀ {α : 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 h =
    (Std.DTreeMap.Internal.Impl.updateCell k (fun x => Std.DTreeMap.Internal.Cell.of k v) l h).impl
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.ext_iff : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, s = t ↔ ↑s = ↑t
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {S : Set M}, N.colon ↑(Submodule.span R S) = N.colon S
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- **Alias** of `mfderiv_subtypeVal_Icc_one`. -/
mfderiv_subtype_coe_Icc_one : ∀ {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)), (mfderiv% Subtype.val z) 1 = 1
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.summand.eq_1 : ∀ {C : Type u_1} (N : ℕ → C) (Δ : SimplexCategoryᵒᵖ) (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  CategoryTheory.SimplicialObject.Splitting.summand N Δ A = N (Opposite.unop A.fst).len
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_zero_iff_eq : ∀ {α : Type u_2} [inst : Zero α] {s : Set α}, s ⊆ 0 ↔ s = ∅ ∨ s = 0