mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Declaration
/-- Number of motives  -/
Lean.RecursorVal.numMotives : Lean.RecursorVal → ℕ
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.CompatibleSMul.of_algebraMap_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) (N : Type u_6) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {A : Type u_11} [inst_5 : CommSemiring A]
  [inst_6 : Algebra R A] [inst_7 : Module A M] [IsScalarTower R A M] [inst_9 : Module A N] [IsScalarTower R A N],
  Function.Surjective ⇑(algebraMap R A) → TensorProduct.CompatibleSMul R A M N
-- Mathlib.CategoryTheory.Category.Basic
/-- Many classes in Mathlib have universe parameters that do not appear in their
input parameter types. For example:
* `Category.{v} (C : Type u)` — the morphism universe `v` is not determined by `C`
* `HasLimitsOfSize.{v₁, u₁} (C : Type u) [Category.{v} C]` — the shape universes `v₁, u₁`
  are not determined by `C`
* `Small.{w} (α : Type v)` — the target universe `w` is not determined by `α`
  (but `v` is determined by `α`, so `v` *is* an output)
* `Functor.IsContinuous.{t} (F) (J) (K)` — the sheaf type universe `t` is not determined
  by `F`, `J`, `K`
* `UnivLE.{u, v}` — has no input parameters at all

By default (since https://github.com/leanprover/lean4/pull/12286), Lean treats any universe
parameter not occurring in input types as an output parameter, and erases it from typeclass
resolution cache keys. This means that queries differing only in such a universe share a
cache entry — the first result found is reused.

This is correct when the universe truly is determined by the inputs (e.g., `v` in
`Small.{w} (α : Type v)`), but incorrect when the universe is part of the *question*
(e.g., `v` in `Category.{v} C`). Cache collisions cause "stuck at solving universe constraint"
errors or silent misresolution.

The `@[univ_out_params]` attribute
(from https://github.com/leanprover/lean4/pull/12423) overrides the default:
* `@[univ_out_params]` — no universe parameters are output (all kept in cache key)
* `@[univ_out_params v]` — only `v` is output

**Rule of thumb:** if the class is typically used with explicit universe annotations
(e.g., `HasLimitsOfSize.{v₁, u₁} C`) or is marked `@[pp_with_univ]`, its "extra" universe
parameters are likely inputs, not outputs, and the class should be annotated with
`@[univ_out_params]`.
 -/
LibraryNote.universe_output_parameters_and_typeclass_caching : Batteries.Util.LibraryNote
-- Mathlib.Algebra.Field.Rat
Rat.inv_nonneg : ∀ {a : ℚ}, 0 ≤ a → 0 ≤ a⁻¹
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.subst.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_4} (motive : L.Term α → (α → L.Term β) → Sort u_5) (l : ℕ)
  (f : L.Functions l) (ts : Fin l → L.Term α) (tf : α → L.Term β)
  (h_1 : (a : α) → (tf : α → L.Term β) → motive (FirstOrder.Language.var a) tf)
  (h_2 :
    (l : ℕ) →
      (f : L.Functions l) → (ts : Fin l → L.Term α) → (tf : α → L.Term β) → motive (FirstOrder.Language.func f ts) tf),
  (match FirstOrder.Language.func f ts, tf with
    | FirstOrder.Language.var a, tf => h_1 a tf
    | FirstOrder.Language.func f ts, tf => h_2 l f ts tf) =
    h_2 l f ts tf
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
instPseudoMetricSpaceAdditive : {α : Type u} → [PseudoMetricSpace α] → PseudoMetricSpace (Additive α)
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instHashableDeclMod.hash : Lean.Meta.LibrarySearch.DeclMod → UInt64
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.variableLengthEncode : ByteArray → UInt64 → ByteArray
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).get k ⋯ = m₂.get k mem
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.chars.eq_1 : ∀ (s : String), s.chars = s.toSlice.chars
-- Init.Data.List.Lemmas
/-- A reasoning principle for proving propositions about the result of `List.foldr` by establishing an
invariant that is true for the initial data and preserved by the operation being folded.

Because the motive can return a type in any sort, this function may be used to construct data as
well as to prove propositions.

Example:
```lean example
example {xs : List Nat} : xs.foldr (· + ·) 1 > 0 := by
  apply List.foldrRecOn
  . show 0 < 1; trivial
  . show ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < a + b
    intros; omega
```
 -/
List.foldrRecOn : {β : Type u_1} →
  {α : Type u_2} →
    {motive : β → Sort u_3} →
      (l : List α) →
        (op : α → β → β) →
          {b : β} → motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op a b)) → motive (List.foldr op b l)
-- Mathlib.NumberTheory.Real.Irrational
irrational_natCast_sub_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (↑n - x) ↔ Irrational x
-- Lean.Parser.Extra
Lean.Parser.dbgTraceState.formatter : String → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.SizeOf
PUnit.unit.sizeOf_spec : sizeOf PUnit.unit = 1
-- Mathlib.Algebra.Opposites
MulOpposite.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq αᵐᵒᵖ
-- Init.Data.BEq
BEq.comm : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b : α}, (a == b) = (b == a)
-- Mathlib.Topology.ClusterPt
closure_eq_cluster_pts : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure s = {a | ClusterPt a (Filter.principal s)}
-- Mathlib.Order.Monotone.Monovary
monovaryOn_toDual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn (⇑OrderDual.toDual ∘ f) g s ↔ AntivaryOn f g s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} {l : List α} {k : α},
  (t.insertManyIfNewUnit l)[k]! = ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey?.get ⋯ = kmi → (compare k kmi).isLE = true
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.denoteExpr : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- See also `Irreducible.isRelPrime_iff_not_dvd`.  -/
Irreducible.coprime_iff_not_dvd : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] {p n : R}, Irreducible p → (IsCoprime p n ↔ ¬p ∣ n)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.mul_congr : ∀ (w : ℕ) (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' * rhs' = lhs * rhs
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_eq_top_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω}, MeasureTheory.hittingAfter u s n ω = ⊤ ↔ ∀ (j : ι), n ≤ j → u j ω ∉ s
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- the second projection `Y j ⟶ X i₂`  -/
CategoryTheory.PreOneHypercover.p₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (self : CategoryTheory.PreOneHypercover S) → ⦃i₁ i₂ : self.I₀⦄ → (j : self.I₁ i₁ i₂) → self.Y j ⟶ self.X i₂
-- Init.Data.UInt.Lemmas
UInt8.toUSize_inj : ∀ {a b : UInt8}, a.toUSize = b.toUSize ↔ a = b
-- Mathlib.Algebra.Quaternion
Quaternion.instFree : ∀ {R : Type u_3} [inst : CommRing R], Module.Free R (Quaternion R)
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.Raw.valuesIter.eq_1 : ∀ {α β : Type u} (m : Std.DHashMap.Raw α fun x => β), m.valuesIter = Std.Iter.map (fun e => e.snd) m.iter
-- Mathlib.Data.Tree.Traversable
BinaryTree.traverse_eq_map_id : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : BinaryTree α),
  BinaryTree.traverse (pure ∘ f) t = pure (BinaryTree.map f t)
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsGLB.mem_of_nonempty_of_not_isPredLimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {x : α},
  IsGLB s x → s.Nonempty → ¬Order.IsPredLimit x → x ∈ s
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**. Let `f : E → F` be a complex analytic function
on an open ball with center `c` and positive radius `R₁`.
If `f` sends this ball to a closed ball with center `f c` and radius `R₂`,
then the norm of the Fréchet derivative of `f` at `c` is at most `R₂ / R₁`.
 -/
Complex.norm_fderiv_le_div_of_mapsTo_ball : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {R₁ R₂ : ℝ} {f : E → F} {c : E},
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) → 0 < R₁ → ‖fderiv ℂ f c‖ ≤ R₂ / R₁
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
_private.Mathlib.MeasureTheory.Integral.FinMeasAdditive.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Goal.getEqc.go : Lean.Meta.Grind.Goal → Lean.Expr → Lean.Expr → Array Lean.Expr → Array Lean.Expr
-- Plausible.Arbitrary
Plausible.Prod.Arbitrary : {α : Type u} → {β : Type v} → [Plausible.Arbitrary α] → [Plausible.Arbitrary β] → Plausible.Arbitrary (α × β)
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_iInf_of_u_l_eq_self : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → α), (∀ (i : ι), u (l (f i)) = f i) → l (⨅ i, f i) = ⨅ i, l (f i)
-- Mathlib.Order.Filter.Defs
Filter.mem_copy : ∀ {α : Type u_1} {f : Filter α} {s : Set α} {S : Set (Set α)} {hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f},
  s ∈ f.copy S hmem ↔ s ∈ S
-- Mathlib.Order.Heyting.Hom
HeytingHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : HeytingAlgebra α] → [inst_1 : HeytingAlgebra β] → FunLike (HeytingHom α β) α β
-- Mathlib.Data.Sign.Basic
SignType.coe_mul : ∀ {α : Type u_1} [inst : MulZeroOneClass α] [inst_1 : HasDistribNeg α] (a b : SignType), ↑(a * b) = ↑a * ↑b
-- Mathlib.CategoryTheory.ObjectProperty.Retract
/-- The closure by retracts of a predicate on objects in a category.  -/
CategoryTheory.ObjectProperty.retractClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} [inst_3 : SizeOf N] [inst_4 : SizeOf E] [inst_5 : SizeOf G] (toFun : G → E)
  (rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom),
  sizeOf { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } = 1
-- Lean.ProjFns
Lean.instReprProjectionFunctionInfo.repr : Lean.ProjectionFunctionInfo → ℕ → Std.Format
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.registerSymExtension.unsafe_impl_2 : {σ : Type} → Lean.Meta.Sym.SymExtension σ → Lean.Meta.Sym.SymExtension Lean.Meta.Sym.SymExtensionState
-- Mathlib.Geometry.Manifold.ChartedSpace
OpenPartialHomeomorph.const.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a a_1 : X} (e_a : a = a_1)
  {b b_1 : Y} (e_b : b = b_1) (ha : IsOpen {a}) (hb : IsOpen {b}),
  OpenPartialHomeomorph.const ha hb = OpenPartialHomeomorph.const ⋯ ⋯
-- Mathlib.Data.Num.ZNum
ZNum.cast_bit0 : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ZNum), ↑n.bit0 = ↑n + ↑n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keys_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.TreeMap.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x t[x])
        t.keys.attach).unattach
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_ext : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys l' →
      (∀ (a : α), Std.Internal.List.getEntry? a l = Std.Internal.List.getEntry? a l') → l.Perm l'
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(α ≫ (f ◁ η) ≫ ηs) ▷ g`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightConsWhisker : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Mathlib.Tactic.BicategoryLike.NormalExpr →
                            Lean.Expr →
                              Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.zoom_del.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (t : RBTree.RBNode α) →
      ((c : RBTree.RBColor) →
          (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)) →
        ((x : RBTree.RBNode α) →
            (∀ (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
                x = RBTree.RBNode.node c l v r → False) →
              motive x) →
          motive t
-- Mathlib.Topology.Connected.LocallyConnected
Topology.IsOpenEmbedding.locallyConnectedSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [LocallyConnectedSpace α] [inst_2 : TopologicalSpace β]
  {f : β → α}, Topology.IsOpenEmbedding f → LocallyConnectedSpace β
-- Init.Prelude
/-- The notation typeclass for heterogeneous addition.
This enables the notation `a + b : γ` where `a : α`, `b : β`.
 -/
HAdd : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Control.ULiftable
/-- convenient shortcut to avoid manipulating `ULift`  -/
ULiftable.adaptDown : {F : Type (max u₀ v₀) → Type u₁} →
  {G : Type v₀ → Type v₁} →
    [L : ULiftable G F] → [Monad F] → {α : Type (max u₀ v₀)} → {β : Type v₀} → F α → (α → G β) → G β
-- Mathlib.CategoryTheory.Limits.Filtered
/-- For all filtered types of size `w`, we have limits  -/
CategoryTheory.Limits.HasCofilteredLimitsOfSize.HasLimitsOfShape : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C] (I : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsCofiltered I],
  CategoryTheory.Limits.HasLimitsOfShape I C
-- Lean.Message
Lean.TraceData.mk.sizeOf_spec : ∀ (cls : Lean.Name) (result? : Option Lean.TraceResult) (startTime stopTime : Float) (collapsed : Bool) (tag : String),
  sizeOf
      { cls := cls, result? := result?, startTime := startTime, stopTime := stopTime, collapsed := collapsed,
        tag := tag } =
    1 + sizeOf cls + sizeOf result? + sizeOf startTime + sizeOf stopTime + sizeOf collapsed + sizeOf tag
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_3) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'], (FractionalIdeal.canonicalEquiv S P P').symm = FractionalIdeal.canonicalEquiv S P' P
-- Mathlib.ModelTheory.Definability
Set.definable_iff_finitely_definable : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s : Set (α → M)},
  A.Definable L s ↔ ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s
-- Mathlib.Computability.DFA
/-- A regular language is a language that is defined by a DFA with finite states.  -/
Language.IsRegular : {T : Type u} → Language T → Prop
-- Mathlib.MeasureTheory.Measure.MutuallySingular
/-- A set such that `μ h.nullSet = 0` and `ν h.nullSetᶜ = 0`.  -/
MeasureTheory.Measure.MutuallySingular.nullSet : {α : Type u_1} → {m0 : MeasurableSpace α} → {μ ν : MeasureTheory.Measure α} → μ.MutuallySingular ν → Set α
-- Lean.Meta.Tactic.Grind.EqResolution
/-- A basic "equality resolution" procedure: Given a proposition `prop` with a proof `proof`, it attempts to resolve equality hypotheses using `isDefEq`. For example, it reduces `∀ x y, f x = f (g y y) → g x y = y` to `∀ y, g (g y y) y = y`, and `∀ (x : Nat), f x ≠ f a` to `False`.
If successful, the result is a pair `(prop', proof)`, where `prop'` is the simplified proposition,
and `proof : prop → prop'`
 -/
Lean.Meta.Grind.eqResolution : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Given proofs
- that `a` is a natural number `na`;
- that `b` is a nonnegative rational number `nb / db`;

returns a tuple of
- a natural number `r` (result);
- the same number, as an expression;
- a proof that `a ^ b = r`.

Fails if `na` is not a `db`th power of a natural number.
 -/
Mathlib.Meta.NormNum.proveIsNatNNRealRPowIsNNRat : (a : Q(NNReal)) →
  (na : Q(ℕ)) →
    Q(Mathlib.Meta.NormNum.IsNat «$a» «$na») →
      (b : Q(ℝ)) →
        (nb db : Q(ℕ)) →
          Q(Mathlib.Meta.NormNum.IsNNRat «$b» «$nb» «$db») →
            Lean.MetaM (ℕ × (r : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$a» ^ «$b») «$r»))
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s : NonemptyInterval α), (-s).toProd.2 = -s.toProd.1
-- Lean.Data.PersistentArray
Lean.PersistentArray : Type u → Type u
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.return.inj : ∀ {ref val ref_1 val_1 : Lean.Syntax},
  Lean.Elab.Term.Do.Code.return ref val = Lean.Elab.Term.Do.Code.return ref_1 val_1 → ref = ref_1 ∧ val = val_1
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_map : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B]
  [inst_7 : StarRing B] [inst_8 : Algebra R B] [inst_9 : StarModule R B] [inst_10 : Semiring C] [inst_11 : StarRing C]
  [inst_12 : Algebra R C] [inst_13 : StarModule R C] (S : StarSubalgebra R A) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B),
  StarSubalgebra.map g (StarSubalgebra.map f S) = StarSubalgebra.map (g.comp f) S
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_sumElim : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid M]
  (f : α₁ → M) (g : α₂ → M), ∏ x, Sum.elim f g x = (∏ a₁, f a₁) * ∏ a₂, g a₂
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comp.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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N O : CategoryTheory.Mod D A} (f : M.Hom N) (g : N.Hom O),
  CategoryTheory.Mod.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isModHom := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_apply : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (i : l × n) (j : m × p),
  Matrix.kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Composition of an `L^p` function with a measure-preserving function is an `L^p` function.  -/
MeasureTheory.Lp.compMeasurePreserving : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] →
            {β : Type u_7} →
              [inst_1 : MeasurableSpace β] →
                {μb : MeasureTheory.Measure β} →
                  (f : α → β) →
                    MeasureTheory.MeasurePreserving f μ μb → ↥(MeasureTheory.Lp E p μb) →+ ↥(MeasureTheory.Lp E p μ)
-- Mathlib.CategoryTheory.Linear.FunctorCategory
CategoryTheory.NatTrans.appLinearMap_apply : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G),
  (CategoryTheory.NatTrans.appLinearMap X) α = α.app X
-- Init.Data.String.Basic
String.Pos.Raw.isValid_singleton : ∀ {c : Char} {p : String.Pos.Raw}, String.Pos.Raw.IsValid (String.singleton c) p ↔ p = 0 ∨ p.byteIdx = c.utf8Size
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.rightAdjointCommShift_commShiftIso : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (a : A),
  CategoryTheory.Functor.commShiftIso G a = CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a
-- Mathlib.Data.Set.Function
Set.prod_surjOn_snd_iff : ∀ {β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂}, Set.SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ↔ t₁.Nonempty ∨ t₂ = ∅
-- Mathlib.Order.RelClasses
WellFoundedGT.toWellFoundedRelation.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedGT α],
  WellFoundedGT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun x1 x2 => x2 < x1
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
Prove a degree bound for `cosPoly n` by induction. Note this is where we find the value in an
explicit description of `cosPoly`.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.cosPoly_natDegree_le : ∀ (n : ℕ), (cosPoly✝ n).natDegree ≤ n
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pushout of `f` and `g` in `Cᵒᵖ` is isomorphic to the pullback of
`f.unop` and `g.unop` in `C`.  -/
CategoryTheory.Limits.pushoutIsoOpPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      (f : X ⟶ Z) →
        (g : X ⟶ Y) →
          [h : CategoryTheory.Limits.HasPushout f g] →
            CategoryTheory.Limits.pushout f g ≅ Opposite.op (CategoryTheory.Limits.pullback f.unop g.unop)
-- Mathlib.Data.List.Sort
/-- Inserting then erasing an element that is absent is the identity.  -/
List.erase_orderedInsert_of_notMem : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [inst_1 : DecidableEq α] {x : α} {xs : List α},
  x ∉ xs → (List.orderedInsert r x xs).erase x = xs
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The subtype of `X × X` corresponding to a relation `φ : X → X → Prop`.  -/
TypeCat.ROfRel : {X : Type w} → (X → X → Prop) → Type (max 0 w)
-- Mathlib.Topology.UniformSpace.Basic
closure_ball_subset : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {V : SetRel α α},
  closure (UniformSpace.ball x V) ⊆ UniformSpace.ball x (closure V)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.mem_cons_iff : ∀ {α : Type u} {a b : α} {s : Stream'.Seq α}, a ∈ Stream'.Seq.cons b s ↔ a = b ∨ a ∈ s
-- Mathlib.Data.Ordmap.Ordset
Ordnode.valid'_nil : ∀ {α : Type u_1} [inst : Preorder α] {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.nil.Bounded o₁ o₂ → Ordnode.Valid' o₁ Ordnode.nil o₂