mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.IsPrimitive.mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Fintype n] [inst_3 : DecidableEq n]
  {A : Matrix n n R}, (∀ (i j : n), 0 ≤ A i j) → (∃ k > 0, ∀ (i j : n), 0 < (A ^ k) i j) → A.IsPrimitive
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.instBoundedSpaceSeq : ∀ {α : Type u_1}, BoundedSpace (Stream'.Seq α)
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.AlternatingMap.ext : ∀ {R : Type u} [inst : CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {φ φ' : M.AlternatingMap N n},
  (∀ (x : Fin n → ↑M), φ x = φ' x) → φ = φ'
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.toJordanDecomposition_smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : NNReal),
  (r • s).toJordanDecomposition = r • s.toJordanDecomposition
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, a ∉ t → Std.DTreeMap.Raw.Const.getD t a fallback = fallback
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_add_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ ν : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → ν.Integrable f → ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
-- Mathlib.Data.Finset.Insert
Finset.eq_singleton_or_nontrivial : ∀ {α : Type u_1} {s : Finset α} {a : α}, a ∈ s → s = {a} ∨ s.Nontrivial
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborate structure constructor applications using structure instance notation or anonymous constructor notation.
 -/
Lean.PrettyPrinter.Delaborator.delabStructureInstance : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.FieldTheory.RatFunc.Valuation
/-- The valued field `F(t)` with the valuation at infinity.  -/
RatFunc.inftyValued : (F : Type u_1) → [inst : Field F] → [DecidableEq (RatFunc F)] → Valued (RatFunc F) (WithZero (Multiplicative ℤ))
-- Mathlib.Analysis.Calculus.Deriv.Shift
deriv_comp_const_sub : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜), deriv (fun x => f (a - x)) x = -deriv f (a - x)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.le_objs : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S T : CategoryTheory.Subgroupoid C}, S ≤ T → S.objs ⊆ T.objs
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.good.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.smul.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x : α), Mathlib.Tactic.Abel.smul n x = n • x
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.extensionValuation_toFun : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  (x : UniformSpace.Completion K),
  Valued.extensionValuation x = MonoidWithZeroHom.ValueGroup₀.embedding (Valued.extension x)
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.zero_at_cusps' : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (self : CuspForm Γ k) {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt self.toFun k
-- Mathlib.RingTheory.Perfection
PerfectionMap.comp_symm_equiv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π)
  (f : Perfection R p), π (m.equiv.symm f) = (Perfection.coeff R p 0) f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited α] {f : α → β → Option γ} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m).getKey! k = ((m.getKey? k).pfilter fun x h' => (f x m[x]).isSome).get!
-- Lean.MetavarContext
Lean.MetavarContext.findUserName? : Lean.MetavarContext → Lean.Name → Option Lean.MVarId
-- Mathlib.Order.Hom.Basic
/-- Surjective order embeddings are equivalent to order isomorphisms.  -/
OrderIso.equivEmbeddingSurjective : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → α ≃o β ≃ { f // Function.Surjective ⇑f }
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_neighborFinset : ∀ {n : ℕ} {v : Fin (n + 2)}, (SimpleGraph.cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1}
-- Mathlib.Order.Bounds.Basic
IsLUB.insert : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] (a : γ) {b : γ} {s : Set γ}, IsLUB s b → IsLUB (insert a s) (a ⊔ b)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Methods.mk.injEq : ∀ (initLB initUB : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr))
  (proveLE proveLT : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)
  (roundUp roundDown : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)
  (eval : Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)) (mkNumeral : ℤ → Lean.MetaM Lean.Expr)
  (initLB_1 initUB_1 : Lean.Expr → Lean.MetaM (Mathlib.Tactic.IntervalCases.Bound × Lean.Expr × Lean.Expr))
  (proveLE_1 proveLT_1 : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)
  (roundUp_1 roundDown_1 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr)
  (eval_1 : Lean.Expr → Lean.MetaM (ℤ × Lean.Expr × Lean.Expr)) (mkNumeral_1 : ℤ → Lean.MetaM Lean.Expr),
  ({ initLB := initLB, initUB := initUB, proveLE := proveLE, proveLT := proveLT, roundUp := roundUp,
        roundDown := roundDown, eval := eval, mkNumeral := mkNumeral } =
      { initLB := initLB_1, initUB := initUB_1, proveLE := proveLE_1, proveLT := proveLT_1, roundUp := roundUp_1,
        roundDown := roundDown_1, eval := eval_1, mkNumeral := mkNumeral_1 }) =
    (initLB = initLB_1 ∧
      initUB = initUB_1 ∧
        proveLE = proveLE_1 ∧
          proveLT = proveLT_1 ∧ roundUp = roundUp_1 ∧ roundDown = roundDown_1 ∧ eval = eval_1 ∧ mkNumeral = mkNumeral_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.maxEntryD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntryD fallback = t₂.maxEntryD fallback
-- Mathlib.Topology.Algebra.ConstMulAction
isClosedMap_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G), IsClosedMap fun x => c • x
-- Mathlib.Data.Int.Order.Basic
Int.lt.elim : ∀ {a b : ℤ}, a < b → ∀ {P : Prop}, (∀ (n : ℕ), a + ↑n.succ = b → P) → P
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkToSMatch.mkAlts : Lean.Elab.Deriving.Context →
  Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.inter m₂).getKey? k = m₁.getKey? k
-- Mathlib.Algebra.BigOperators.Pi
MonoidHom.functions_ext'_iff : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → CommMonoid (M i)] [Finite I]
  {N : Type u_9} [inst_3 : CommMonoid N] {g h : ((i : I) → M i) →* N},
  g = h ↔ ∀ (i : I), g.comp (MonoidHom.mulSingle M i) = h.comp (MonoidHom.mulSingle M i)
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.ensureNotBuiltinCases : Lean.Name → Lean.CoreM Unit
-- Mathlib.Analysis.Normed.Operator.Mul
/-- Multiplication in a normed algebra as a linear isometry to the space of
continuous linear maps.  -/
ContinuousLinearMap.mulₗᵢ : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (R : Type u_3) →
      [inst_1 : NonUnitalSeminormedRing R] →
        [inst_2 : NormedSpace 𝕜 R] →
          [inst_3 : IsScalarTower 𝕜 R R] →
            [inst_4 : SMulCommClass 𝕜 R R] → [RegularNormedAlgebra 𝕜 R] → R →ₗᵢ[𝕜] R →L[𝕜] R
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.not_tendsto_pow_atTop_atBot : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ},
  ¬Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atBot
-- Lean.Widget.UserWidget
/-- Use this structure and the `@[widget]` attribute to define your own widgets.

```lean
@[widget]
def rubiks : UserWidgetDefinition :=
  { name := "Rubiks cube app"
    javascript := include_str ...
  }
```
 -/
Lean.Widget.UserWidgetDefinition : Type
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_le_iff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
  p ≠ 0 → ∀ (a : R) (n : ℕ), Polynomial.rootMultiplicity a p ≤ n ↔ ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The repr uses the notation from the `OnePoint` locale.  -/
instReprOnePoint : {X : Type u_1} → [Repr X] → Repr (OnePoint X)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.not_isLoop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.not_isLoop_iff._auto_1 → (¬M.IsLoop e ↔ M.IsNonloop e)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instDivisionRing : (K : Type u) →
  [inst : Field K] → (p : ℕ) → [inst_1 : Fact (Nat.Prime p)] → [inst_2 : CharP K p] → DivisionRing (PerfectClosure K p)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasureSMulNNReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {r : NNReal},
  MeasureTheory.IsFiniteMeasure (r • μ)
-- Mathlib.Topology.Category.TopPair
/-- The homotopy on the first space.  -/
TopPair.Homotopy.fst : {X Y : TopPair} → {f g : X ⟶ Y} → TopPair.Homotopy f g → TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g)
-- Aesop.Frontend.Attribute
Aesop.Frontend.Parser.aesop : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.Q_is_eventually_constant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {q n : ℕ},
  n ≤ q → (AlgebraicTopology.DoldKan.Q (q + 1)).f n = (AlgebraicTopology.DoldKan.Q q).f n
-- Mathlib.Algebra.Lie.Basic
/-- A morphism of Lie algebra modules (denoted as `M →ₗ⁅R,L⁆ N`) is a linear map
which commutes with the action of the Lie algebra.  -/
«term_→ₗ⁅_,_⁆_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A countable intersection of analytic sets is analytic.  -/
MeasureTheory.AnalyticSet.iInter : ∀ {α : Type u_1} {ι : Type u_2} [inst : TopologicalSpace α] [hι : Nonempty ι] [Countable ι] [T2Space α] {s : ι → Set α},
  (∀ (n : ι), MeasureTheory.AnalyticSet (s n)) → MeasureTheory.AnalyticSet (⋂ n, s n)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
_private.Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn.0.ApproximatesLinearOn.termN : Lean.ParserDescr
-- Mathlib.Tactic.FunProp.FunctionData
/-- The result of `FunctionData.decomposition` and `FunctionData.peeloffArgDecomposition`.  -/
Mathlib.Meta.FunProp.DecompositionResult : Type
-- Mathlib.Analysis.SpecialFunctions.Bernstein
_private.Mathlib.Analysis.SpecialFunctions.Bernstein.0.bernstein.«term_/ₙ» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Convex.Function
ConcaveOn.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E]
  [inst_6 : Module 𝕜 β] [PosSMulMono 𝕜 β] {s : Set E} {f : E → β} {c : 𝕜},
  0 ≤ c → ConcaveOn 𝕜 s f → ConcaveOn 𝕜 s fun x => c • f x
-- Mathlib.Data.Set.Card
Set.one_le_encard_insert : ∀ {α : Type u_1} {a : α} (s : Set α), 1 ≤ (insert a s).encard
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.orderBot : {α : Type u_1} → [inst : LE α] → [OrderBot α] → OrderBot (Multiplicative α)
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_succ_right_eq_insert_Ico : ∀ {a b : ℕ}, a ≤ b → Finset.Ico a b.succ = insert b (Finset.Ico a b)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (k' : α) (v' : β k')
  (h_1 : Unit → motive none) (h_2 : (k' : α) → (v' : β k') → motive (some ⟨k', v'⟩)),
  (match some ⟨k', v'⟩ with
    | none => h_1 ()
    | some ⟨k', v'⟩ => h_2 k' v') =
    h_2 k' v'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.distinct_keys_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) (Std.DTreeMap.Raw.Const.toList t)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
Ideal.instLiesOverFiberOfIsPrime : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime], q.LiesOver p
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.pow_apply_mem_toList_iff_mem_support : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {p : Equiv.Perm α} {x : α} {n : ℕ},
  (p ^ n) x ∈ p.toList x ↔ x ∈ p.support
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.card_filter_unsortedEigenvalues_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (μ : 𝕜),
  {i | ↑(LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn i) = μ}.card = Module.finrank 𝕜 ↥(Module.End.eigenspace T μ)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.mul_snd : ∀ {q : ℕ} (x y : LucasLehmer.X q), (x * y).2 = x.1 * y.2 + x.2 * y.1
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_monomial_subset : ∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R], ((MvPolynomial.monomial s) a).support ⊆ {s}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
`2 * cos θ` to the value `2 * cos (n * θ)`.  -/
Polynomial.Chebyshev.C_two_mul_complex_cos : ∀ (θ : ℂ) (n : ℤ), Polynomial.eval (2 * Complex.cos θ) (Polynomial.Chebyshev.C ℂ n) = 2 * Complex.cos (↑n * θ)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_le_iff_le_rpow : ∀ {b x y : ℝ}, 1 < b → 0 < x → (Real.logb b x ≤ y ↔ x ≤ b ^ y)
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.instHasFiniteColimits : ∀ (R : Type w) [inst : Ring R], CategoryTheory.Limits.HasFiniteColimits (ModuleCat R)
-- Init.Core
Prod.lexLtDec : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LT α] →
      [inst_1 : LT β] →
        [DecidableEq α] →
          [(a b : α) → Decidable (a < b)] → [(a b : β) → Decidable (a < b)] → (s t : α × β) → Decidable (s.lexLt t)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- A sequence of functions `f` is said to converge in measure to some function `g` if for all
`ε > 0`, the measure of the set `{x | ε ≤ dist (f i x) (g x)}` tends to 0 as `i` converges along
some given filter `l`.  -/
MeasureTheory.TendstoInMeasure : {α : Type u_1} →
  {ι : Type u_2} →
    {E : Type u_4} →
      [EDist E] → {x : MeasurableSpace α} → MeasureTheory.Measure α → (ι → α → E) → Filter ι → (α → E) → Prop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mkIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (e e_1 : M.X ≅ N.X) (e_e : e = e_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Mon.mkIso e one_f mul_f = CategoryTheory.Mon.mkIso e_1 ⋯ ⋯
-- Mathlib.Topology.ShrinkingLemma
ShrinkingLemma.PartialRefinement.mk.sizeOf_spec : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  [inst_1 : SizeOf ι] [inst_2 : SizeOf X] [inst_3 : (a : ι) → (a_1 : X) → SizeOf (u a a_1)]
  [inst_4 : (a : X) → SizeOf (s a)] [inst_5 : (a : Set X) → SizeOf (p a)] (toFun : ι → Set X) (carrier : Set ι)
  (isOpen : ∀ (i : ι), IsOpen (toFun i)) (subset_iUnion : s ⊆ ⋃ i, toFun i)
  (closure_subset : ∀ {i : ι}, i ∈ carrier → closure (toFun i) ⊆ u i)
  (pred_of_mem : ∀ {i : ι}, i ∈ carrier → p (toFun i)) (apply_eq : ∀ {i : ι}, i ∉ carrier → toFun i = u i),
  sizeOf
      { toFun := toFun, carrier := carrier, isOpen := isOpen, subset_iUnion := subset_iUnion,
        closure_subset := closure_subset, pred_of_mem := pred_of_mem, apply_eq := apply_eq } =
    1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.left_inv : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α}, x ∈ e.source → ↑e.symm (↑e x) = x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- Subtraction of morphisms in a `NonPreadditiveAbelian` category.  -/
CategoryTheory.NonPreadditiveAbelian.hasSub : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.NonPreadditiveAbelian C] → {X Y : C} → Sub (X ⟶ Y)
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- `CoalgEquivClass F R A B` asserts `F` is a type of bundled coalgebra equivalences
from `A` to `B`.  -/
CoalgEquivClass : (F : Type u_5) →
  (R : outParam (Type u_6)) →
    (A : outParam (Type u_7)) →
      (B : outParam (Type u_8)) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : AddCommMonoid B] →
              [inst_3 : Module R A] →
                [inst_4 : Module R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → [EquivLike F A B] → Prop
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.two_mul_semilength_eq_length : ∀ {p : DyckWord}, 2 * p.semilength = (↑p).length
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castSuccEmb_Ioi : ∀ {n : ℕ} (i : Fin n), Finset.map Fin.castSuccEmb (Finset.Ioi i) = Finset.Ioo i.castSucc (Fin.last n)
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.valid.inj : ∀ {escaped : Bool} {acc : String} {escaped_1 : Bool} {acc_1 : String},
  Std.Http.Internal.UnquoteState.valid✝ escaped acc = Std.Http.Internal.UnquoteState.valid✝ escaped_1 acc_1 →
    escaped = escaped_1 ∧ acc = acc_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_eq_get_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : a ∈ t}, t[a] = t[a]?.get ⋯
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given `AddCommMonoid`s `M, P` and `AddSubmonoid`s `S ⊆ M, T ⊆ P`, if `f : M →* N` is a
Localization map for `S` and `k : P ≃+ M` is an isomorphism of `AddCommMonoid`s such that
`k(T) = S`, `f ∘ k` is a Localization map for `T`.  -/
AddSubmonoid.LocalizationMap.ofAddEquivOfDom : {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] →
              S.LocalizationMap N →
                {T : AddSubmonoid P} → {k : P ≃+ M} → AddSubmonoid.map k.toAddMonoidHom T = S → T.LocalizationMap N
-- Mathlib.Order.Minimal
MaximalFor.anti : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] {P Q : ι → Prop} {f : ι → α} {i : ι},
  MaximalFor P f i → Q ≤ P → Q i → MaximalFor Q f i
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.reindexₗ_apply : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} {l : Type u_7} {o : Type u_8} [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {eₘ : m ≃ l} {eₙ : n ≃ o} {M : CStarMatrix m n A} {i : l} {j : o},
  (CStarMatrix.reindexₗ R A eₘ eₙ) M i j = (Matrix.reindex eₘ eₙ) M i j
-- Init.Data.SInt.Lemmas
Int16.not_maxValue_lt : ∀ {a : Int16}, ¬Int16.maxValue < a
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_apply : ∀ {n : ℕ}, ArithmeticFunction.vonMangoldt n = if IsPrimePow n then Real.log ↑n.minFac else 0
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_units_zsmul : ∀ {E : Type u_8} [inst : SeminormedAddGroup E] (n : ℤˣ) (a : E), ‖n • a‖₊ = ‖a‖₊
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.yonedaPresheaf_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C TopCat) (Y : Type w')
  [inst_1 : TopologicalSpace Y] (X : Cᵒᵖ), (ContinuousMap.yonedaPresheaf F Y).obj X = C(↑(F.obj (Opposite.unop X)), Y)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.preimage_unionProd : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {X' Y' : SSet} (f : X' ⟶ X) (g : Y' ⟶ Y),
  (S.unionProd T).preimage (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    (S.preimage f).unionProd (T.preimage g)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.mono' : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} {g : α → ℝ},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) → MeasureTheory.MemLp f p μ
-- Mathlib.Topology.Order.IsLUB
IsLUB.isLUB_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  MonotoneOn f s → IsLUB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsLUB (f '' s) b
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
/-- The finite set of monic irreducible factors of `minpoly ℤ θ` modulo `p`.
 -/
RingOfIntegers.monicFactorsMod : {K : Type u_1} →
  [inst : Field K] → NumberField.RingOfIntegers K → (p : ℕ) → [inst : Fact (Nat.Prime p)] → Finset (Polynomial (ZMod p))
-- Mathlib.Data.Nat.PrimeFin
Nat.Primes.infinite : Infinite Nat.Primes
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.minKeyD fallback = t.keys.headD fallback
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.exists_inv_mem : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α} {p : α → Prop}, (∃ x, x⁻¹ ∈ s ∧ p x) ↔ ∃ x ∈ s, p x⁻¹
-- Mathlib.Algebra.Lie.Solvable
LieHom.isSolvable_range : ∀ {R : Type u} {L : Type v} {L' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (f : L' →ₗ⁅R⁆ L) [LieAlgebra.IsSolvable L'],
  LieAlgebra.IsSolvable ↥f.range
-- Mathlib.Data.Rel
SetRel.inv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β), R.inv = Prod.swap ⁻¹' R
-- Lean.Level
Lean.Level.beq : Lean.Level → Lean.Level → Bool
-- Std.Async.Timer
Std.Async.Interval.native : Std.Async.Interval → Std.Internal.UV.Timer