mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- Let `K` be a field with an admissible family of absolute values (giving rise
to a logarithmic height).
Let `p` be a family (indexed by `ι'`) of homogeneous polynomials in variables indexed by
the finite type `ι` and of the same degree `N`. Then for any `x : ι →  K`,
the logarithmic height of `fun j : ι' ↦ eval x (p j)` is bounded by a constant
(which is made explicit) plus `N * logHeight x`.  -/
Height.logHeight_eval_le : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K},
  (∀ (i : ι'), (p i).IsHomogeneous N) →
    ∀ (x : ι → K),
      (Height.logHeight fun j => (MvPolynomial.eval x) (p j)) ≤
        Real.log (max (Height.mulHeightBound p) 1) + ↑N * Height.logHeight x
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_toBilin`. -/
BilinForm.toMatrix_toBilin : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁) (M : Matrix n n R₁),
  (LinearMap.BilinForm.toMatrix b) ((Matrix.toBilin b) M) = M
-- Mathlib.Combinatorics.Matroid.Basic
/-- A `Finitary` matroid is one where a set is independent if and only if it all
its finite subsets are independent, or equivalently a matroid whose circuits are finite.  -/
Matroid.Finitary : {α : Type u_1} → Matroid α → Prop
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMin.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.Tree α β (1 + l'.size) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.Tree α β (1 + l'.size)) →
          ((l'' : Std.DTreeMap.Internal.Impl α β) →
              (hl''₁ : l''.Balanced) →
                (hl''₂ : l''.size = 1 + l'.size) → motive { impl := l'', balanced_impl := hl''₁, size_impl := hl''₂ }) →
            motive x
-- Batteries.Data.BinomialHeap.Basic
/-- `next` is a binomial heap with ranks above `rank + 1`.  -/
Batteries.BinomialHeap.Imp.FindMin.WF.next : ∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α}
  (self : Batteries.BinomialHeap.Imp.FindMin.WF le res), Batteries.BinomialHeap.Imp.Heap.WF le (self.rank + 1) res.next
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.coeq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {j j' : C},
  CategoryTheory.IsFiltered.filteredClosure f j →
    CategoryTheory.IsFiltered.filteredClosure f j' →
      ∀ (f_1 f' : j ⟶ j'), CategoryTheory.IsFiltered.filteredClosure f (CategoryTheory.IsFiltered.coeq f_1 f')
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- Two arrows `f : X ⟶ P` and `g : Y ⟶ P` are called pseudo-equal if there is some object
`R` and epimorphisms `p : R ⟶ X` and `q : R ⟶ Y` such that `p ≫ f = q ≫ g`.  -/
CategoryTheory.Abelian.PseudoEqual : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (P : C) → CategoryTheory.Over P → CategoryTheory.Over P → Prop
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Icc' : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, c ≤ b → Set.Iic b ∪ Set.Icc c d = Set.Iic (max b d)
-- Mathlib.Algebra.Ring.Commute
/-- **Alias** of `sq_sub_sq`. -/
pow_two_sub_pow_two : ∀ {R : Type u} [inst : CommRing R] (a b : R), a ^ 2 - b ^ 2 = (a + b) * (a - b)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_op : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  {δ' : α → Sort u_8} (h : (i : α) → δ i → δ' i),
  (s.piecewise (fun x => h x (f x)) fun x => h x (g x)) = fun x => h x (s.piecewise f g x)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_pow : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (φ : A →ₐ[R] A)
  (n : ℕ), ⇑(φ ^ n) = (⇑φ)^[n]
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addU.eq_1 : ∀ {F : Type u} [inst : Field F] (P Q : Fin 3 → F),
  WeierstrassCurve.Jacobian.addU P Q = -((P 1 * Q 2 ^ 3 - Q 1 * P 2 ^ 3) / (P 2 * Q 2))
-- Std.Do.SPred.SPred
_private.Std.Do.SPred.SPred.0.Std.Do.SPred.conjunction.match_1.splitter : {σs : List (Type u_1)} →
  (motive : List (Std.Do.SPred σs) → Sort u_2) →
    (env : List (Std.Do.SPred σs)) →
      (Unit → motive []) → ((P : Std.Do.SPred σs) → (env : List (Std.Do.SPred σs)) → motive (P :: env)) → motive env
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- Conversion from `SSet.Edge.CompStruct` to `SSet.Truncated.Edge.CompStruct`.  -/
SSet.Edge.CompStruct.toTruncated : {X : SSet} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { len := 0 })} →
    {e₀₁ : SSet.Edge x₀ x₁} →
      {e₁₂ : SSet.Edge x₁ x₂} →
        {e₀₂ : SSet.Edge x₀ x₂} → e₀₁.CompStruct e₁₂ e₀₂ → e₀₁.toTruncated.CompStruct e₁₂.toTruncated e₀₂.toTruncated
-- Mathlib.Topology.WithTopology
WithTopology.instSemilatticeInf : {X : Type u_1} → (t : TopologicalSpace X) → [SemilatticeInf X] → SemilatticeInf (WithTopology X t)
-- Mathlib.Control.Random
/-- A monad to generate random objects using the generator type `StdGen`.  -/
Rand : Type u_1 → Type u_1
-- Mathlib.Order.Directed
/-- If `f` is monotone and antitone on a directed order, then `f` is constant.  -/
constant_of_monotone_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : Preorder α] {f : α → β} [IsDirectedOrder α],
  Monotone f → Antitone f → ∀ (a b : α), f a = f b
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_apply_le : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedMul M] {a : α}
  {s : Set α} {f g : α → M}, (a ∈ s → f a ≤ g a) → s.mulIndicator f a ≤ g a
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.instUniqueEdgeLabeling : {V : Type u_1} → {G : SimpleGraph V} → {K : Type u_3} → [Unique K] → Unique (G.EdgeLabeling K)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- A coefficient of a product of truncated power series equals the coefficient of the untruncated
product, with the two truncation levels `n₁` and `n₂` allowed to differ.  -/
MvPowerSeries.coeff_trunc_mul_trunc_eq_coeff_mul₂ : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n₁ n₂ : σ →₀ ℕ)
  (f g : MvPowerSeries σ R) {m : σ →₀ ℕ},
  m < n₁ →
    m < n₂ →
      MvPolynomial.coeff m ((MvPowerSeries.trunc R n₁) f * (MvPowerSeries.trunc R n₂) g) =
        (MvPowerSeries.coeff m) (f * g)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm_apply_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) {x : α} {y : β}, e.symm y < x ↔ y < e x
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
zero_le_padicValRat_of_nat : ∀ {p : ℕ} (n : ℕ), 0 ≤ padicValRat p ↑n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonNatIso.eq_1 : ∀ {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 F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e : F ≅ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  CategoryTheory.Functor.mapAddMonNatIso e =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.AddMon.mkIso (e.app X.X) ⋯ ⋯) ⋯
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.IterM.size : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → [Monad m] → Std.IterM m β → m (ULift.{u_1, 0} ℕ)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instProductive : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [Std.PRange.LawfulUpwardEnumerable α], Std.Iterators.Productive (Std.Rxc.Iterator α) Id
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_3.splitter : {α : Type u_1} →
  (xs : List α) →
    (motive : Ordnode α × { l' // l'.length ≤ xs.length } → Sort u_2) →
      (x : Ordnode α × { l' // l'.length ≤ xs.length }) →
        ((t : Ordnode α) → (property : [].length ≤ xs.length) → motive (t, ⟨[], property⟩)) →
          ((l : Ordnode α) → (y : α) → (ys : List α) → (h : (y :: ys).length ≤ xs.length) → motive (l, ⟨y :: ys, h⟩)) →
            motive x
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_eq_filter_Ioc_one : ∀ (n : ℕ), n.primesLE = Finset.filter Nat.Prime (Finset.Ioc 1 n)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.hasColimit_parallelPair_comp_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f.hom],
  CategoryTheory.Limits.HasColimit ((CategoryTheory.Limits.parallelPair f 0).comp P.ι)
-- Mathlib.Topology.Baire.Lemmas
/-- If `p : Y → X` is an open embedding and `X` is a Baire space, then `Y` is a Baire space.  -/
Topology.IsOpenEmbedding.baireSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {Y : Type u_4} [inst_2 : TopologicalSpace Y] {p : Y → X},
  Topology.IsOpenEmbedding p → BaireSpace Y
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_id_comp : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X) (X ⟶[V] Y))
        (CategoryTheory.eComp V X X Y)) =
    CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.bicone_ι_π_ne : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J},
  j ≠ j' → CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j') = 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getLE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getLE? k = t₂.getLE? k
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_lintegral_div' : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : α → ENNReal},
  Measurable f →
    ∫⁻ (y : α), f y ∂μ ≠ ⊤ →
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (nhds (f x))
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.ext_iff : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {x y : F.Grothendieck},
  x = y ↔ x.base = y.base ∧ x.fiber ≍ y.fiber
-- Init.Data.Array.Subarray
/-- The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the subarray is
empty.
 -/
Subarray.start_le_stop : ∀ {α : Type u_1} (xs : Subarray α), xs.start ≤ xs.stop
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.finsetSup : ∀ {X : Type u_1} {R : Type u_2} {Y : Type u_3} [inst : AddCommMonoid R] [inst_1 : LinearOrder R]
  [inst_2 : AddLeftStrictMono R] [inst_3 : IsOrderedAddMonoid R] {f : Y → PseudoMetric X R} {s : Finset Y},
  (∀ d ∈ s, (f d).IsUltra) → (s.sup f).IsUltra
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_associator : ∀ {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 Z : D),
  CategoryTheory.MonoidalCategoryStruct.associator X Y Z =
    e.functor.mapIso
      (CategoryTheory.MonoidalCategory.whiskerRightIso
          (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y))).symm
          (e.inverse.obj Z) ≪≫
        CategoryTheory.MonoidalCategoryStruct.associator (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫
          CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X)
            (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj Y) (e.inverse.obj Z))))
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_extend : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  (P : Finpartition a) (b c : α) {hb : b ≠ ⊥} {hab : Disjoint a b} {hc : a ⊔ b = c},
  (P.extend hb hab hc).parts.card = P.parts.card + 1
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul_nc.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (pw : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit))
  (h_3 :
    (pw : Lean.Grind.CommRing.Power) → (m₁ : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult pw m₁)),
  (m₁ = Lean.Grind.CommRing.Mon.unit → False) →
    (match Lean.Grind.CommRing.Mon.mult pw m₁ with
      | Lean.Grind.CommRing.Mon.unit => h_1 ()
      | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => h_2 pw
      | Lean.Grind.CommRing.Mon.mult pw m₁ => h_3 pw m₁) =
      h_3 pw m₁
-- Mathlib.RingTheory.FreeRing
FreeRing.zero_ne_of : ∀ {α : Type u} (x : α), 0 ≠ FreeRing.of x
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommSemiring.mk : Lean.Meta.Sym.Arith.Semiring →
  ℕ → Lean.Expr → Option (Option Lean.Expr) → Option Lean.Expr → Lean.Meta.Sym.Arith.CommSemiring
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getKey_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁.getKey k hk = m₂.getKey k ⋯
-- Mathlib.Order.KrullDimension
/-- The height of an element in a series is larger or equal to its index in the series.
 -/
Order.index_le_height : ∀ {α : Type u_1} [inst : Preorder α] (p : LTSeries α) (i : Fin (p.length + 1)), ↑↑i ≤ Order.height (p.toFun i)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → β},
  (Std.Internal.List.Option.dmap✝ x fun a x => f a) = Option.map f x
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
_private.Init.Data.Float.Model.Unpacked.Pack.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_2 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (s : Float.Model.UnpackedFloat.Sign)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.infinity s with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_2 s
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_Ico_ae_eq_pi_Icc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {s : Set ι}
  {f g : (i : ι) → α i},
  (s.pi fun i => Set.Ico (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Icc (f i) (g i)
-- Mathlib.Algebra.Category.Ring.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
CommRingCat.Hom.Simps.hom : (R S : CommRingCat) → R.Hom S → ↑R →+* ↑S
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.exists_minimal : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsPWO → s.Nonempty → ∃ a, Minimal (fun x => x ∈ s) a
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.size.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → Sort u_2) (h_1 : Unit → motive Ordnode.nil)
  (h_2 : (sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)),
  (match Ordnode.nil with
    | Ordnode.nil => h_1 ()
    | Ordnode.node sz l x r => h_2 sz l x r) =
    h_1 ()
-- Mathlib.Data.Nat.Digits.Div
Nat.eleven_dvd_iff : ∀ {n : ℕ}, 11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (Nat.digits 10 n)).alternatingSum
-- Mathlib.Topology.MetricSpace.Thickening
IsClopen.of_thickening_subset_self : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {δ : ℝ}, 0 < δ → Metric.thickening δ s ⊆ s → IsClopen s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α} {b : β a}, (m.insert a b).getKey! a = a
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
/-- **Alias** of `Rat.num_lt_denom_iff`. -/
Rat.lt_one_iff_num_lt_denom : ∀ {q : ℚ}, q.num < ↑q.den ↔ q < 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (mem : k ∈ t₂), (t₁ ∪ t₂)[k] = t₂[k]
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- If there is no `j` so `c.Rel i j`, then `C.xNext i` is isomorphic to `C.X i`.  -/
HomologicalComplex.xNextIsoSelf : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (C : HomologicalComplex V c) → {i : ι} → ¬c.Rel i (c.next i) → (C.xNext i ≅ C.X i)
-- Init.Data.List.Sublist
List.infix_append_of_infix_right : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+: l₃ → l₁ <:+: l₂ ++ l₃
-- Mathlib.Topology.Instances.Nat
Nat.dist_eq : ∀ (x y : ℕ), dist x y = |↑x - ↑y|
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig.elab : Lean.Syntax → Lean.Elab.TermElabM Aesop.Frontend.AttrConfig
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.refl : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a : ℝ}
  {μ : MeasureTheory.Measure ℝ}, IntervalIntegrable f μ a a
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.iInter₂ : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [inst : LE α] [Nonempty ι] [∀ (i : ι), Nonempty (κ i)]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsRelLowerSet (f i j) P) → IsRelLowerSet (⋂ i, ⋂ j, f i j) P
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.card_le_aleph : ∀ (o : Ordinal.{u_1}), o.card ≤ Cardinal.aleph o
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2.congr_simp : ∀ {α : Type u_1} (E : Type u_2) (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0), MeasureTheory.condExpL2 E 𝕜 hm = MeasureTheory.condExpL2 E 𝕜 hm
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.precomp_apply : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {𝕜₃ : Type u_6} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_7} {F : Type u_8} (G : Type u_10) [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : AddCommGroup F] [inst_7 : TopologicalSpace F] [inst_8 : AddCommGroup G] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup G] [inst_11 : Module 𝕜₁ E] [inst_12 : Module 𝕜₂ F] [inst_13 : Module 𝕜₃ G]
  [inst_14 : ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (f : F →SLₚₜ[τ] G),
  (PointwiseConvergenceCLM.precomp G L) f = f ∘SL L
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.instNonemptyCostructuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] (d : D), Nonempty (CategoryTheory.CostructuredArrow F d)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.const_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable ((fun x => c) * f) μ
-- Lean.Elab.ConfigEval.Basic
/-- Like `foldConfigM` but takes an array of configurations or configuration items.
 -/
Lean.Elab.ConfigEval.foldConfigsM : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadRef m] →
        α → Array Lean.Syntax → (α → Lean.Elab.ConfigEval.ConfigItem → m α) → (α → Lean.Syntax → m α) → m α
-- Mathlib.Analysis.Calculus.Deriv.Slope
hasDerivAt_iff_tendsto_slope_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x ↔ Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds f')
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Filter.totallyBounded_map_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {F : Filter α},
  IsUniformInducing f → ((Filter.map f F).TotallyBounded ↔ F.TotallyBounded)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The identity strong natural transformation.  -/
CategoryTheory.Lax.StrongTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → (F : CategoryTheory.LaxFunctor B C) → CategoryTheory.Lax.StrongTrans F F
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.opNorm_le_of_re_inner_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {T : E →L[𝕜] F}
  {C : ℝ}, 0 ≤ C → (∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → RCLike.re (inner 𝕜 (T x) y) ≤ C) → ‖T‖ ≤ C
-- Init.Data.UInt.Lemmas
UInt64.mod_lt : ∀ (a : UInt64) {b : UInt64}, 0 < b → a % b < b
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_support_multiset_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {s : Multiset (α →₀ M)},
  ∀ a ∈ s.sum.support, ∃ f ∈ s, a ∈ f.support
-- Init.Data.Fin.Lemmas
Fin.castAdd_mk : ∀ {n : ℕ} (m i : ℕ) (h : i < n), Fin.castAdd m ⟨i, h⟩ = ⟨i, ⋯⟩
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_closure_of_mem : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {x : G}, x ∈ s → x ∈ Subgroup.closure s
-- Init.Data.Array.MapIdx
Array.back?_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β},
  (Array.mapIdx f xs).back? = Option.map (f (xs.size - 1)) xs.back?
-- Mathlib.Topology.Order.IsLUB
IsGLB.nhdsWithin_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsGLB s a → s.Nonempty → (nhdsWithin a s).NeBot