mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_eq_getLastD_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.maxD fallback = t.toList.getLastD fallback
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.splitter : (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) →
  (x : Lean.Level) →
    (x_1 : ℕ) →
      (x_2 : Lean.Level) →
        (x_3 : ℕ) →
          ((l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂) →
            ((l₁ : Lean.Level) →
                (k₁ : ℕ) →
                  (l₂ : Lean.Level) →
                    (k₂ : ℕ) → (∀ (l₁_1 : Lean.Level), l₁ = l₁_1.succ → False) → motive l₁ k₁ l₂.succ k₂) →
              ((l₁₁ l₁₂ : Lean.Level) →
                  (k₁ : ℕ) → (l₂₁ l₂₂ : Lean.Level) → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂) →
                ((l₁₁ l₁₂ : Lean.Level) →
                    (k₁ : ℕ) → (l₂₁ l₂₂ : Lean.Level) → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂) →
                  ((n₁ : Lean.Name) →
                      (k₁ : ℕ) →
                        (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂) →
                    ((n₁ : Lean.LMVarId) →
                        (k₁ : ℕ) →
                          (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂) →
                      ((l₁ : Lean.Level) →
                          (k₁ : ℕ) →
                            (l₂ : Lean.Level) →
                              (k₂ : ℕ) →
                                (∀ (l₁_1 : Lean.Level), l₁ = l₁_1.succ → False) →
                                  (∀ (l₂_1 : Lean.Level), l₂ = l₂_1.succ → False) →
                                    (∀ (l₁₁ l₁₂ l₂₁ l₂₂ : Lean.Level), l₁ = l₁₁.max l₁₂ → l₂ = l₂₁.max l₂₂ → False) →
                                      (∀ (l₁₁ l₁₂ l₂₁ l₂₂ : Lean.Level),
                                          l₁ = l₁₁.imax l₁₂ → l₂ = l₂₁.imax l₂₂ → False) →
                                        (∀ (n₁ n₂ : Lean.Name),
                                            l₁ = Lean.Level.param n₁ → l₂ = Lean.Level.param n₂ → False) →
                                          (∀ (n₁ n₂ : Lean.LMVarId),
                                              l₁ = Lean.Level.mvar n₁ → l₂ = Lean.Level.mvar n₂ → False) →
                                            motive l₁ k₁ l₂ k₂) →
                        motive x x_1 x_2 x_3
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] {n m n' : ℕ},
  n = n' + 1 → P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_sum : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {ι : Type u_6} (s : Finset ι) (f : ι → AdicCompletion I M), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.appendEquiv_apply : ∀ {α : Type u_1} (m n : ℕ) (fg : (Fin m → α) × (Fin n → α)) (a : Fin (m + n)),
  (Fin.appendEquiv m n) fg a = Fin.append fg.1 fg.2 a
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.instHasEqualizers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C],
  CategoryTheory.Limits.HasEqualizers C
-- Mathlib.Order.Filter.Basic
/-- `generate g` is the largest filter containing the sets `g`.  -/
Filter.generate : {α : Type u} → Set (Set α) → Filter α
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.of_comp_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] {f : α → X} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν],
  MeasureTheory.AEStronglyMeasurable (fun x => f x.1) (μ.prod ν) → ν ≠ 0 → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instInhabited : {E : Type u_3} → [inst : AddGroup E] → Inhabited (NonarchAddGroupSeminorm E)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Summable.hasSum_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {a : α} [T2Space α] [L.NeBot], Summable f L → (HasSum f a L ↔ ∑'[L] (b : β), f b = a)
-- Mathlib.Data.Stream.Init
Stream'.drop_tail' : ∀ {α : Type u} {i : ℕ} {s : Stream' α}, Stream'.drop i s.tail = Stream'.drop (i + 1) s
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAddMonoid.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S],
  AddOreLocalization.instAddMonoid =
    { toAdd := AddOreLocalization.instAdd, add_assoc := ⋯, toZero := AddOreLocalization.instZero, zero_add := ⋯,
      add_zero := ⋯, nsmul := AddOreLocalization.nsmul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Order.Atoms.Finite
Finite.to_isCoatomic : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] [Finite α], IsCoatomic α
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- A precoverage is a collection of *covering* presieves on every object `X : C`.
See `CategoryTheory.Coverage` and `CategoryTheory.Pretopology` for common extensions of this.  -/
CategoryTheory.Precoverage : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.disjoint_closedBall_of_lt_infDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ},
  r < Metric.infDist x s → Disjoint (Metric.closedBall x r) s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult.0.Std.Tactic.BVDecide.BVPred.mkUlt.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : aig.BinaryRefVec w → Sort u_1) (lhsRefs rhsRefs : aig.RefVec w)
  (h_1 : (lhsRefs rhsRefs : aig.RefVec w) → motive { lhs := lhsRefs, rhs := rhsRefs }),
  (match { lhs := lhsRefs, rhs := rhsRefs } with
    | { lhs := lhsRefs, rhs := rhsRefs } => h_1 lhsRefs rhsRefs) =
    h_1 lhsRefs rhsRefs
-- Std.Time.Date.Unit.Week
Std.Time.Week.instDecidableLtOffset : {x y : Std.Time.Week.Offset} → Decidable (x < y)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}
  {h' : k ∈ Std.DTreeMap.filterMap f t}, (Std.DTreeMap.filterMap f t).get k h' = (f k (t.get k ⋯)).get ⋯
-- Init.Data.Array.Int
Array.sum_replicate_int : ∀ {n : ℕ} {a : ℤ}, (Array.replicate n a).sum = ↑n * a
-- Mathlib.Probability.Martingale.BorelCantelli
/-- **Lévy's generalization of the Borel-Cantelli lemma**: given a sequence of sets `s` and a
filtration `ℱ` such that for all `n`, `s n` is `ℱ n`-measurable, `limsup s atTop` is almost
everywhere equal to the set for which `∑ k, ℙ(s (k + 1) | ℱ k) = ∞`.  -/
MeasureTheory.ae_mem_limsup_atTop_iff : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    ∀ᵐ (ω : Ω) ∂μ,
      ω ∈ Filter.limsup s Filter.atTop ↔
        Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) Filter.atTop Filter.atTop
-- Mathlib.Data.Num.ZNum
ZNum.abs_to_nat : ∀ (n : ZNum), ↑n.abs = (↑n).natAbs
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.hom_id : ∀ {A : ProfiniteGrp.{u}},
  ProfiniteGrp.Hom.hom (CategoryTheory.CategoryStruct.id A) = ContinuousMonoidHom.id ↑A.toProfinite.toTop
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
/-- If a non-unital subalgebra of a non-unital topological algebra is commutative, then so is its
topological closure.

See note [reducible non-instances].  -/
NonUnitalSubalgebra.nonUnitalCommRingTopologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : NonUnitalRing A] →
          [inst_3 : Module R A] →
            [inst_4 : ContinuousConstSMul R A] →
              [inst_5 : IsSemitopologicalRing A] →
                [T2Space A] →
                  (s : NonUnitalSubalgebra R A) →
                    (∀ (x y : ↥s), x * y = y * x) → NonUnitalCommRing ↥s.topologicalClosure
-- Mathlib.CategoryTheory.Subobject.Basic
/-- `map f : Subobject X ⥤ Subobject Y` is
the left adjoint of `pullback f : Subobject Y ⥤ Subobject X`.  -/
CategoryTheory.Subobject.mapPullbackAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Mono f] → CategoryTheory.Subobject.map f ⊣ CategoryTheory.Subobject.pullback f
-- Mathlib.RingTheory.Coalgebra.Basic
/-- An arbitrarily chosen representation.  -/
Coalgebra.termℛ : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_rco' : ∀ {m n k : ℤ}, Array.map (fun x => k + x) (m...n).toArray = ((k + m)...k + n).toArray
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.exists_mem_support_forall_mem_support_imp_eq : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v} (s : Finset V),
  {x ∈ s | x ∈ p.support}.Nonempty → ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_bot : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.map f ⊥ = ⊥
-- Mathlib.Data.Finset.Max
Finset.min_insert : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, (insert a s).min = min (↑a) s.min
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inter.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E E_1 : CategoryTheory.PreOneHypercover S)
  (e_E : E = E_1) (F F_1 : CategoryTheory.PreOneHypercover S) (e_F : F = F_1)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))],
  E.inter F = E_1.inter F_1
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) (i : Z.affineCover.I₀),
  CategoryTheory.Limits.HasPullback
    (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f Z.affineCover).f i) f) g
-- Std.Async.Process
/-- CPU time spent in kernel mode (milliseconds)
 -/
Std.IO.Process.ResourceUsageStats.cpuSystemTime : Std.IO.Process.ResourceUsageStats → Std.Time.Millisecond.Offset
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- A mixin typeclass saying that the `(c +ᵥ ·)` is a proper map for all `c`.

Note that this is **not** the same as a proper additive action (not yet in `Mathlib`).  -/
ProperConstVAdd : (M : Type u_1) → (X : Type u_2) → [VAdd M X] → [TopologicalSpace X] → Prop
-- Mathlib.RingTheory.Henselian
HenselianLocalRing.toIsLocalRing : ∀ {R : Type u_1} {inst : CommRing R} [self : HenselianLocalRing R], IsLocalRing R
-- Mathlib.Topology.Connected.Clopen
Topology.IsCoinducing.image_connectedComponent : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsCoinducing f →
    (∀ (y : β), IsConnected (f ⁻¹' {y})) → ∀ (a : α), f '' connectedComponent a = connectedComponent (f a)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_iff_exists_mul : ∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] {a b : α}, a ≤ b ↔ ∃ c, b = a * c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.abs_iteratedDeriv_sin_le_one : ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n Real.sin x| ≤ 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The size of `s * s` is at least the size of `s`, version with right-cancellative multiplication.
See `card_le_card_mul_self` for the version with left-cancellative multiplication.
 -/
Finset.card_le_card_mul_self' : ∀ {α : Type u_2} [inst : Mul α] [IsRightCancelMul α] [inst_2 : DecidableEq α] {s : Finset α}, s.card ≤ (s * s).card
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.Normal.of_addCommutator_le : ∀ (G : Type u_1) [inst : AddGroup G] {H : AddSubgroup G}, addCommutator G ≤ H → H.Normal
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I),
  (I.multicoforkEquivSigmaCofork.functor.obj K).pt = K.pt
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_mul : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Mul β] (f g : α → β),
  (UniformOnFun.ofFun 𝔖) (f * g) = (UniformOnFun.ofFun 𝔖) f * (UniformOnFun.ofFun 𝔖) g
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.dotIdCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ →
      Lean.Elab.ContextInfo →
        Lean.LocalContext →
          Lean.Name → Option Lean.Expr → Lean.Server.CancellableM (Array Lean.Lsp.ResolvableCompletionItem)
-- Mathlib.Topology.Algebra.Support
mulTSupport_div : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : DivisionMonoid α] (f g : X → α),
  (mulTSupport fun x => f x / g x) ⊆ mulTSupport f ∪ mulTSupport g
-- Mathlib.Data.Finset.SDiff
Finset.empty_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ∅ \ s = ∅
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSMul : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : (i : ι) → SMul R (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] → SMul R (DirectLimit G f)
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'_k : Lean.Grind.AC.Expr → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.withFn.parenthesizer : (Lean.Parser.ParserFn → Lean.Parser.ParserFn) → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- The Leibniz functor associated to the internal hom on a monoidal closed category. This is the
bifunctor of arrow categories that sends `f : A ⟶ B` and `g : X ⟶ Y` to the canonical map from
`B ⟹ X` to the pullback of `(ihom A).map g : A ⟹ X ⟶ A ⟹ Y` and
`(pre f).app Y : B ⟹ Y ⟶ A ⟹ Y`, induced by the following diagram:
```
  B ⟹ X --> A ⟹ X
     |          |
     v          v
  B ⟹ Y --> A ⟹ Y
```
 -/
CategoryTheory.MonoidalCategory.Arrow.pullbackHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPullbacks C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [CategoryTheory.MonoidalClosed C] →
          CategoryTheory.Functor (CategoryTheory.Arrow C)ᵒᵖ
            (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C))
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instOrdOffset : Ord Std.Time.Millisecond.Offset
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.symmetrifyStar : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) (u : U),
  φ.symmetrify.star u =
    ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
-- Init.Data.Vector.Lemmas
Vector.toArray_take : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, (xs.take i).toArray = xs.toArray.take i
-- Init.Tactics
/-- Configuration for the `decide` tactic family.
 -/
Lean.Parser.Tactic.DecideConfig : Type
-- Init.Conv
/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
which only unfolds `@[reducible]` definitions).  -/
Lean.Parser.Tactic.Conv.convErw__ : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_mul : ∀ (a b : Cardinal.{u}), Cardinal.lift.{v, u} (a * b) = Cardinal.lift.{v, u} a * Cardinal.lift.{v, u} b
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The "inclusion" morphism in the factorization given by
the small object argument.  -/
CategoryTheory.SmallObject.ιObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              {X Y : C} → (f : X ⟶ Y) → X ⟶ CategoryTheory.SmallObject.obj I κ f
-- Mathlib.Order.Hom.Lattice
SupHom.instMax.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β],
  SupHom.instMax = { max := fun f g => { toFun := ⇑f ⊔ ⇑g, map_sup' := ⋯ } }
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorph_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  e.toPartialHomeomorph.source = Set.univ
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The category of additive commutative monoids has all limits.  -/
AddCommMonCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddCommMonCat
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_one_lt_lift : ∀ {c : Cardinal.{u}}, Cardinal.aleph 1 < Cardinal.lift.{v, u} c ↔ Cardinal.aleph 1 < c
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Data.Multiset.Bind
Multiset.bind_map_comm : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : α → β → γ},
  (m.bind fun a => Multiset.map (fun b => f a b) n) = n.bind fun b => Multiset.map (fun a => f a b) m
-- Lean.Data.JsonRpc
/-- Generic version of `Message.responseError`.

References:
- [JSON-RPC](https://www.jsonrpc.org/specification#error_object)
- [LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#responseError).
 -/
Lean.JsonRpc.ResponseError : Type u → Type u
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β}, k ∈ m₂ → Std.DHashMap.Const.getD (m₁.diff m₂) k fallback = fallback
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehavior : Lean.Parser.Parser
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨅ i, f i = 0` when the domain of the real-valued function `f` is empty, it suffices to show
that all values of `f` are at least some nonpositive number `a` to show that `a ≤ ⨅ i, f i`.

See also `le_ciInf`.  -/
Real.le_iInf : ∀ {ι : Sort u_1} {f : ι → ℝ} {a : ℝ}, (∀ (i : ι), a ≤ f i) → a ≤ 0 → a ≤ ⨅ i, f i
-- Mathlib.Order.Fin.Basic
Fin.instIsBotZeroClass : ∀ {n : ℕ} [inst : NeZero n], IsBotZeroClass (Fin n)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBiproduct_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : F.PreservesZeroMorphisms] [inst_6 : CategoryTheory.Limits.PreservesBiproduct f F],
  (F.mapBiproduct f).inv = CategoryTheory.Limits.biproduct.desc fun j => F.map (CategoryTheory.Limits.biproduct.ι f j)
-- Lean.DocString.Types
/-- An unordered list.
 -/
Lean.Doc.Block.ul : {i : Type u} → {b : Type v} → Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block i b
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel κ.swapRight
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- An `IntegrationParams` is a structure holding 3 Boolean values used to define a filter to be
used in the definition of a box-integrable function.
 -/
BoxIntegral.IntegrationParams : Type
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkAndCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkAndCached
-- Init.Data.Nat.MinMax
Nat.mul_min_mul_left : ∀ (a b c : ℕ), min (a * b) (a * c) = a * min b c
-- Mathlib.Order.SupClosed
supClosure_min : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s t : Set α}, s ⊆ t → SupClosed t → supClosure s ⊆ t
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] {p : Polynomial K}, p ≠ 0 → (Polynomial.C p.leadingCoeff⁻¹).degree = 0
-- Mathlib.Algebra.Lie.Derivation.BaseChange
/-- A derivation of an associative `R`-algebra `A`, induces a Lie derivation of `A ⊗[R] L` for any
Lie algebra `L` over `R`.  -/
Lie.Derivation.ofDerivation : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (L : Type u_3) →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                Derivation R A A →ₗ⁅R⁆ LieDerivation R (TensorProduct R A L) (TensorProduct R A L)
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.lt_iff_ssubset`. -/
HasSSubset.SSubset.lt : ∀ {α : Type u} {s t : Set α}, s ⊂ t → s ⊂ t
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).inv.app X).2.2 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inrCompInrCompInverseAssociator A A' T).inv X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Sum.inr_ A' T).associator
            ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).comp (CategoryTheory.sum.inverseAssociator A A' T)) X).hom
        ((CategoryTheory.Sum.inr_ A' T).whiskerLeft
          ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).hom))