mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Induction
List.twoStepInduction.eq_2 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) (a : α),
  List.twoStepInduction nil singleton cons_cons [a] = singleton a
-- Lean.Parser.Types
Lean.Parser.FirstTokens.tokens.sizeOf_spec : ∀ (a : List Lean.Parser.Token), sizeOf (Lean.Parser.FirstTokens.tokens a) = 1 + sizeOf a
-- Init.Data.Array.Lemmas
Array.getElem?_eq_none_iff : ∀ {α : Type u_1} {i : ℕ} {xs : Array α}, xs[i]? = none ↔ xs.size ≤ i
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The measure on `ℝ / ℤ` is a probability measure.  -/
instIsProbabilityMeasureUnitAddCircleVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.adj_getVert_succ : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {i : ℕ},
  i < w.length → G.Adj (w.getVert i) (w.getVert (i + 1))
-- Mathlib.Logic.Equiv.Basic
Equiv.isEmpty : ∀ {α : Sort u_1} {β : Sort u_4} (e : α ≃ β) [IsEmpty β], IsEmpty α
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.op_ringCon : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R), I.op.ringCon = I.ringCon.op
-- Mathlib.Analysis.Calculus.FDeriv.Pow
differentiableWithinAt_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ) {x : 𝔸} {s : Set 𝔸}, DifferentiableWithinAt 𝕜 (fun x => x ^ n) s x
-- Mathlib.LinearAlgebra.Prod
LinearMap.inl_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (x : M), (LinearMap.inl R M M₂) x = (x, 0)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_eq_zero_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R}, v.restrict x = 0 ↔ v x = 0
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- Dense sets have small difference constant.  -/
Finset.divConst_le_inv_dens : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} [inst_2 : Fintype G],
  A.divConst B ≤ A.dens⁻¹
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst_mul_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A.subConst B * ↑A.card = ↑(A - B).card
-- Mathlib.Algebra.Ring.Equiv
RingHom.inverse_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (g : S → R)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : S), (f.inverse g h₁ h₂) a = g a
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If every finite diagram in `C` admits a cone, then `C` is cofiltered. It is sufficient to
verify this for diagrams whose shape lives in any one fixed universe.  -/
CategoryTheory.IsCofiltered.of_cone_nonempty : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (∀ {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
      (F : CategoryTheory.Functor J C), Nonempty (CategoryTheory.Limits.Cone F)) →
    CategoryTheory.IsCofiltered C
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_inf_units : ∀ {M : Type u_1} [inst : Monoid M] (S T : Subgroup Mˣ), (S.ofUnits ⊓ T.ofUnits).units = S ⊓ T
-- Mathlib.Algebra.Module.ULift
ULift.smulZeroClass : {R : Type u} → {M : Type v} → [inst : Zero M] → [SMulZeroClass R M] → SMulZeroClass (ULift.{u_1, u} R) M
-- Init.Internal.Order.Basic
Lean.Order.inf_spec : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {x : α} {c : α → Prop},
  Lean.Order.PartialOrder.rel x (Lean.Order.inf c) ↔ ∀ (y : α), c y → Lean.Order.PartialOrder.rel x y
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- The inverse of a local diffeomorphism.  -/
PartialDiffeomorph.symm : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} → PartialDiffeomorph I J M N n → PartialDiffeomorph J I N M n
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.perpBisector_nonempty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P}, (↑(AffineSubspace.perpBisector p₁ p₂)).Nonempty
-- Std.Sync.Mutex
Std.instCoeOutMutexBaseMutex : {α : Type} → CoeOut (Std.Mutex α) Std.BaseMutex
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.continuous_realToRCLike : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜],
  Continuous (ContinuousMap.realToRCLike 𝕜)
-- Mathlib.Data.Finset.Powerset
Finset.map_val_val_powersetCard : ∀ {α : Type u_1} (s : Finset α) (i : ℕ),
  Multiset.map Finset.val (Finset.powersetCard i s).val = Multiset.powersetCard i s.val
-- Mathlib.Analysis.SpecificLimits.Normed
/-- The **alternating series test** for antitone sequences.
See also `Antitone.tendsto_alternating_series_of_tendsto_zero`.  -/
Antitone.cauchySeq_alternating_series_of_tendsto_zero : ∀ {f : ℕ → ℝ},
  Antitone f → Filter.Tendsto f Filter.atTop (nhds 0) → CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.eval_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤)
  (h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m) (n : ℕ),
  AdicCompletion.eval I N n ∘ₗ AdicCompletion.lift I f ⋯ = f n
-- Init.Data.Int.Gcd
Int.gcd_dvd_natAbs_right : ∀ (a b : ℤ), a.gcd b ∣ b.natAbs
-- Mathlib.Topology.Path
/-- The start point of a `Path`.  -/
Path.source' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (self : Path x y), self.toFun 0 = x
-- Mathlib.Order.Interval.Finset.Fin
Fin.Iic_sub_one_eq_Iio : ∀ {n : ℕ} {b : Fin n}, 0 < b → Finset.Iic (b - 1) = Finset.Iio b
-- Init.Data.Vector.Lemmas
Vector.foldlM_toList : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] {f : β → α → m β} {init : β}
  {xs : Vector α n}, List.foldlM f init xs.toList = Vector.foldlM f init xs
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.instAdditiveFunctorCurriedTensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C],
  (CategoryTheory.MonoidalCategory.curriedTensor C).Additive
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_dif : ∀ {α : Type u_1} {p : Prop} [inst : Decidable p] (s : p → Set α), ⋃ (h : p), s h = if h : p then s h else ∅
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
csInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {s : Set β} {f : β → α},
  BddBelow (Set.range fun i => f ↑i) → ⨅ i, f ↑i ≤ sInf ∅ → sInf (f '' s) = ⨅ a ∈ s, f a
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- Auxiliary definition for `transfiniteComposition.wellOrderInductionData`.  -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cocone F} →
              {X Y : C} →
                {p : X ⟶ Y} →
                  {f : F.obj ⊥ ⟶ X} →
                    {g : c.pt ⟶ Y} →
                      [F.IsWellOrderContinuous] →
                        {j : J} →
                          Order.IsSuccLimit j →
                            ↑(⋯.functor.op.comp
                                    (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f
                                      g)).sections →
                              (F.obj j ⟶ X)
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.unique' : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p.Monic →
    (Polynomial.aeval x) p = 0 →
      (∀ (q : Polynomial A), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0) → p = minpoly A x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.fac_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Limits.image.lift F') =
    F'.e
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- Auxiliary definition for `horn.IsCompatible.desc`.  -/
_private.Mathlib.AlgebraicTopology.SimplicialSet.HornColimits.0.SSet.horn.IsCompatible.multicofork : {n : ℕ} →
  {X : SSet} →
    {i : Fin (n + 2)} →
      {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)} →
        SSet.horn.IsCompatible f →
          CategoryTheory.Limits.Multicofork
            ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map SSet.Subcomplex.toSSetFunctor)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.divisionMonoid.eq_1 : ∀ {α : Type u_2} [inst : DivisionMonoid α],
  Set.divisionMonoid =
    { toMonoid := Set.monoid, toInv := Set.involutiveInv.toInv, toDiv := Set.div, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_inv := ⋯, mul_inv_rev := ⋯,
      inv_eq_of_mul := ⋯ }
-- Mathlib.Data.Nat.Log
Nat.log_pow_left : ∀ (b k n : ℕ), Nat.log (b ^ k) n = Nat.log b n / k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.DHashMap.Raw.Const.insertMany m l},
  (Std.DHashMap.Raw.Const.insertMany m l).getKey k h' = m.getKey k ⋯
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelUp' : (α : Type u_1) → [inst : AddRightCancelSemigroup α] → [DecidableEq α] → (a : α) → DecidableRel (ComplexShape.up' a).Rel
-- Mathlib.GroupTheory.Coset.Defs
/-- **Alias** of `QuotientAddGroup.induction_on`. -/
QuotientAddGroup.induction_on' : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_inv : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), a⁻¹⁺ᵐ = a⁻ᵐ
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instAddMonoid : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → AddMonoid (MultilinearMap R M₁ M₂)
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.normedCommGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedCommGroup E] {s : Subgroup E},
  Subgroup.normedCommGroup =
    { toNorm := Subgroup.seminormedCommGroup.toNorm, toCommGroup := s.toCommGroup, toMetricSpace := Subtype.metricSpace,
      dist_eq := ⋯ }
-- Mathlib.Data.Int.Interval
Int.card_fintype_Ico_of_le : ∀ (a b : ℤ), a ≤ b → ↑(Fintype.card ↑(Set.Ico a b)) = b - a
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatEraLong : Std.Time.DateFormatSymbols → Std.Time.Year.Era → String
-- Std.Time.Date.Unit.Month
Std.Time.Month.instMulOffset : Mul Std.Time.Month.Offset
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftK_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0), CategoryTheory.CategoryStruct.comp (h.liftK k hk) h.i = k
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` and types `I₁`, `I₂`, `I₃`,
this is the obvious functor
`GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄`.
 -/
CategoryTheory.GradedObject.mapTrifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)) →
                  (I₁ : Type u_7) →
                    (I₂ : Type u_8) →
                      (I₃ : Type u_9) →
                        CategoryTheory.Functor (CategoryTheory.GradedObject I₁ C₁)
                          (CategoryTheory.Functor (CategoryTheory.GradedObject I₂ C₂)
                            (CategoryTheory.Functor (CategoryTheory.GradedObject I₃ C₃)
                              (CategoryTheory.GradedObject (I₁ × I₂ × I₃) C₄)))
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_cons_div_left : ∀ {x : ℤ} {xs : List ℤ}, ↑(Lean.Omega.IntList.gcd (x :: xs)) ∣ x
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_copy : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (s : Set M) (hs : s = ↑p), ↑(p.copy s hs) = s
-- Mathlib.Topology.Path
Path.ofLine.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x)
  (h₁ : f 1 = y),
  Path.ofLine hf h₀ h₁ = { toFun := f ∘ Subtype.val, continuous_toFun := ⋯, source' := h₀, target' := h₁ }
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) the left unitor for R-modules  -/
SemimoduleCat.MonoidalCategory.leftUnitor : {R : Type u} → [inst : CommSemiring R] → (M : SemimoduleCat R) → SemimoduleCat.of R (TensorProduct R R ↑M) ≅ M
-- Lean.Parser.Extra
Lean.Parser.evalInsideQuot.parenthesizer : Lean.Name → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_finite : ∀ (R : Type u_1) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Finite M],
  IsNoetherian R M
-- Mathlib.Probability.Moments.Variance
/-- The `ℝ`-valued variance of a real-valued random variable defined by applying `ENNReal.toReal`
to `evariance`.  -/
ProbabilityTheory.variance : {Ω : Type u_1} → {mΩ : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ℝ
-- Mathlib.Data.List.AList
AList.keys_mk : ∀ {α : Type u} {β : α → Type v} (l : List (Sigma β)) (h : l.NodupKeys), { entries := l, nodupKeys := h }.keys = l.keys
-- Mathlib.CategoryTheory.Monoidal.Limits.Preserves
/-- When `C` is braided and `tensorRight c` preserves a limit, then so does `tensorLeft k`.
We are not making this an instance to avoid an instance loop with
`preservesLimit_of_braided_and_preservesLimit_tensor_left`.  -/
CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.BraidedCategory C] (c : C)
  [CategoryTheory.Limits.PreservesLimit F (CategoryTheory.MonoidalCategory.tensorRight c)],
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.MonoidalCategory.tensorLeft c)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instZPow : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → DivInvMonoid (R i)] →
              [∀ (i : ι), SubgroupClass (S i) (R i)] → Pow (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) ℤ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} (t t_1 : Std.TreeSet α cmp) (e_t : t = t_1) (a a_1 : α) (e_a : a = a_1)
  (h : a ∈ t), t.get a h = t_1.get a_1 ⋯
-- Mathlib.Topology.Bornology.Hom
/-- The pullback of the `Bornology.cobounded` filter under the function is contained in the
cobounded filter. Equivalently, the function maps bounded sets to bounded sets.  -/
LocallyBoundedMapClass.comap_cobounded_le : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Bornology α} {inst_1 : Bornology β}
  {inst_2 : FunLike F α β} [self : LocallyBoundedMapClass F α β] (f : F),
  Filter.comap (⇑f) (Bornology.cobounded β) ≤ Bornology.cobounded α
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_add_inter₀' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_union_add_inter₀'._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_union_add_inter₀'._auto_3 →
        μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processCtor : Lean.Syntax → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Mathlib.Algebra.Ring.ULift
ULift.nonUnitalCommSemiring : {R : Type u} → [NonUnitalCommSemiring R] → NonUnitalCommSemiring (ULift.{u_1, u} R)
-- Mathlib.Algebra.Notation.Prod
Prod.zero_eq_mk : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N], 0 = (0, 0)
-- Mathlib.Computability.Ackermann
ack_lt_iff_left : ∀ {m₁ m₂ n : ℕ}, ack m₁ n < ack m₂ n ↔ m₁ < m₂
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
/-- **Alias** of `Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar`.

---

The center of `GL n R` consists of scalar matrices.  -/
Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {g : GL n R},
  g ∈ Subgroup.center (GL n R) ↔ ↑g ∈ Set.range ⇑(Matrix.scalar n)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instCoeSortType : CoeSort MonCat (Type u)
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.zero : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S], MvPowerSeries.HasEval 0
-- Mathlib.Algebra.Group.Hom.Basic
zsmulAddGroupHom.eq_1 : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (n : ℤ),
  zsmulAddGroupHom n = { toFun := fun x => n • x, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.FieldTheory.Finite.GaloisField
GaloisField.card : ∀ (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ), n ≠ 0 → Nat.card (GaloisField p n) = p ^ n
-- Mathlib.Analysis.Convex.Integral
/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an
integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`:
`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma.  -/
Convex.set_average_mem : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E},
  Convex ℝ s →
    IsClosed s →
      μ t ≠ 0 →
        μ t ≠ ⊤ → (∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) → MeasureTheory.IntegrableOn f t μ → ⨍ (x : α) in t, f x ∂μ ∈ s
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- If matrices `A` and `C + C * V * A⁻¹ * U * C` are invertible, then so is `A + U * C * V`.  -/
Matrix.invertibleAddMulMul' : {m : Type u_1} →
  {n : Type u_2} →
    {α : Type u_3} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : Fintype m] →
            [inst_3 : DecidableEq m] →
              [inst_4 : Ring α] →
                (A : Matrix n n α) →
                  (U : Matrix n m α) →
                    (C : Matrix m m α) →
                      (V : Matrix m n α) →
                        [inst_5 : Invertible A] → [Invertible (C + C * V * ⅟A * U * C)] → Invertible (A + U * C * V)
-- Lean.Util.MonadBacktrack
Lean.MonadBacktrack.saveState : {s : outParam Type} → {m : Type → Type} → [self : Lean.MonadBacktrack s m] → m s
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.commaFromUnder_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Under X)),
  (CategoryTheory.WithInitial.commaFromUnder.obj K).left = X
-- Mathlib.Analysis.Complex.Exponential
Real.exp_bound_div_one_sub_of_interval : ∀ {x : ℝ}, 0 ≤ x → x < 1 → Real.exp x ≤ 1 / (1 - x)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.div.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Div β],
  e.div = { div := fun x y => e.invFun (e.toFun x / e.toFun y) }
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expand.go_neg : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] {i : ℕ} {source : Array (Std.DHashMap.Internal.AssocList α β)}
  {target : { d // 0 < d.size }}, ¬i < source.size → Std.DHashMap.Internal.Raw₀.expand.go✝ i source target = target
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_div : ∀ {ι : Type u_1} {K : Type u_3} [inst : Semifield K] [inst_1 : CharZero K] (s : Finset ι) (f : ι → K) (a : K),
  (s.expect fun i => f i) / a = s.expect fun i => f i / a
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instNontrivial : ∀ {M : Type u_1} [inst : MonoidWithZero M] [Nontrivial M], Nontrivial (Associates M)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinitesimal.eq_1 : ∀ (x : ℝ*), x.Infinitesimal = x.IsSt 0
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.injTheoremFailureHeader : Lean.Name → Lean.MessageData
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- In a C⋆-algebra, the spectral radius of a self-adjoint element is equal to its norm.
See `IsSelfAdjoint.toReal_spectralRadius_eq_norm` for a version involving
`spectralRadius ℝ a`.  -/
IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A}, IsSelfAdjoint a → (spectralRadius ℂ a).toReal = ‖a‖
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.underlyingIso_inv_top_arrow_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso (CategoryTheory.CategoryStruct.id B)).inv
      (CategoryTheory.CategoryStruct.comp ⊤.arrow h) =
    h