mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The candidate for the scalar product `r • m`.  -/
PresheafOfModules.Sheafify.SMulCandidate.x : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          {α : R₀ ⟶ R.obj} →
            {M₀ : PresheafOfModules R₀} →
              {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                {φ : M₀.presheaf ⟶ A.obj} →
                  {X : Cᵒᵖ} →
                    {r : ↑(R.obj.obj X)} →
                      {m : ↑(A.obj.obj X)} → PresheafOfModules.Sheafify.SMulCandidate α φ r m → ↑(A.obj.obj X)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.deficient_one : Nat.Deficient 1
-- Mathlib.RepresentationTheory.FDRep
/-- Auxiliary definition for `FDRep.dualTensorIsoLinHom`.  -/
FDRep.dualTensorIsoLinHomAux : {k : Type u} →
  {G : Type v} →
    {V : Type u} →
      [inst : Field k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              [inst_4 : FiniteDimensional k V] →
                (ρV : Representation k G V) →
                  (W : FDRep k G) →
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj (FDRep.of ρV.dual) W).V ≅
                      (FDRep.of (ρV.linHom W.ρ)).V
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_iso_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).iso.hom =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Lean.Parser.Term
/-- Syntax kind for syntax nodes representing the field of a projection in the `InfoTree`.
Specifically, the `InfoTree` node for a projection `s.f` contains a child `InfoTree` node
with syntax ``(Syntax.node .none identProjKind #[`f])``.

This is necessary because projection syntax cannot always be detected purely syntactically
(`s.f` may refer to either the identifier `s.f` or a projection `s.f` depending on
the available context).
 -/
Lean.Parser.Term.identProjKind : Lean.Name
-- Batteries.Control.ForInStep.Lemmas
ForInStep.run_done : ∀ {α : Type u_1} {a : α}, (ForInStep.done a).run = a
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_mul₃_le : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] {a b c : α}, ‖a * b * c‖₊ ≤ ‖a‖₊ * ‖b‖₊ * ‖c‖₊
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_fac_assoc : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F) {Z : CategoryTheory.Functor C H} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (LF'.leftDerivedNatTrans LF α' α W τ))
      (CategoryTheory.CategoryStruct.comp α h) =
    CategoryTheory.CategoryStruct.comp α' (CategoryTheory.CategoryStruct.comp τ h)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.maxEntryD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → (a : α) × β a → (a : α) × β a
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_eq_prod_odd : ∀ (n : ℕ), (2 * n + 1).doubleFactorial = ∏ i ∈ Finset.range n, (2 * (i + 1) + 1)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.finitaryExtensive_TopCat : CategoryTheory.FinitaryExtensive TopCat
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.le_csSup_image : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : Preorder α] {f : α → β},
  Monotone f → ∀ {s : Set α} {c : α}, c ∈ s → BddAbove s → f c ≤ sSup (f '' s)
-- Mathlib.Data.NNReal.Basic
NNReal.mul_finset_sup : ∀ {α : Type u_3} (r : NNReal) (s : Finset α) (f : α → NNReal), r * s.sup f = s.sup fun a => r * f a
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_self_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] (a : α) {b : α}, a / b < a ↔ 1 < b
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (self : J.MayerVietorisSquare), CategoryTheory.Mono self.f₁₃
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The left commuting triangle of the factorization morphism.  -/
CategoryTheory.Factorisation.Hom.ι_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  (self : d.Hom e), CategoryTheory.CategoryStruct.comp d.ι self.h = e.ι
-- Mathlib.Analysis.Convex.BetweenList
List.wbtw_four : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {p₁ p₂ p₃ p₄ : P},
  List.Wbtw R [p₁, p₂, p₃, p₄] ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄
-- Mathlib.Data.Nat.Cast.Order.Basic
/-- See also `Nat.cast_pos`, specialised to `IsOrderedRing`.  -/
Nat.cast_pos' : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1]
  {n : ℕ}, 0 < ↑n ↔ 0 < n
-- Mathlib.Order.Types.Defs
OrderType.type_eq_one : ∀ {α : Type u} [inst : LinearOrder α], OrderType.type α = 1 ↔ Nonempty (Unique α)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.isEmbedding_toFun_finite : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β], Topology.IsEmbedding ⇑(UniformOnFun.toFun {s | s.Finite})
-- Mathlib.RingTheory.IsTensorProduct
Algebra.pushoutDesc.congr_simp : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_11 : Semiring A] [inst_12 : Algebra R A] (f f_1 : S →ₐ[R] A)
  (e_f : f = f_1) (g g_1 : R' →ₐ[R] A) (e_g : g = g_1) (hf : ∀ (x : S) (y : R'), f x * g y = g y * f x),
  Algebra.pushoutDesc S' f g hf = Algebra.pushoutDesc S' f_1 g_1 ⋯
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.nhds_eq : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) {x₀ : G}, nhds x₀ = B.N x₀
-- Mathlib.Util.Export
Lean.Export.instInhabitedAlloc : {a : Type u_1} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Lean.Export.Alloc a)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_eq_zero : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] {x : WithLp p V}, x.ofLp = 0 ↔ x = 0
-- Mathlib.Algebra.Ring.Parity
even_neg_two : ∀ {α : Type u_2} [inst : Ring α], Even (-2)
-- Mathlib.Topology.MetricSpace.Isometry
/-- The composition of two isometric isomorphisms, as an isometric isomorphism.  -/
IsometryEquiv.trans : {α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      [inst : PseudoEMetricSpace α] →
        [inst_1 : PseudoEMetricSpace β] → [inst_2 : PseudoEMetricSpace γ] → α ≃ᵢ β → β ≃ᵢ γ → α ≃ᵢ γ
-- Mathlib.CategoryTheory.MarkovCategory.Positive
CategoryTheory.PositiveCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [toMarkovCategory : CategoryTheory.MarkovCategory C] →
        (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
            [h : CategoryTheory.Deterministic (CategoryTheory.CategoryStruct.comp f g)],
            CategoryTheory.CategoryStruct.comp f
                (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                  (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id Y))) =
              CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) f)) →
          CategoryTheory.PositiveCategory C
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_pred_left_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  ¬IsMin b → Set.Ioo (Order.pred b) a = Set.Ico b a
-- Mathlib.CategoryTheory.Limits.Indization.LocallySmall
CategoryTheory.instSmallHomFunctorOppositeTypeColimitCompYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} I]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape I (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)]
  [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : CategoryTheory.Functor I C)
  (G : CategoryTheory.Functor Cᵒᵖ (Type v)),
  Small.{v, max u v} (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda) ⟶ G)
-- Mathlib.Order.Defs.Unbundled
/-- `IsTrans` as a definition, suitable for use in proofs.  -/
Transitive : {α : Sort u_1} → (α → α → Prop) → Prop
-- Mathlib.Data.List.MinMax
List.minimum_of_length_pos_le_getElem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {i : ℕ} (w : i < l.length) (h : optParam (0 < l.length) ⋯),
  List.minimum_of_length_pos h ≤ l[i]
-- Mathlib.Order.Defs.LinearOrder
max_def' : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), max a b = if b ≤ a then a else b
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.uniqueMDiffOn_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  n ≠ 0 → ∀ {s : Set M}, UniqueMDiff[⇑h '' s] ↔ UniqueMDiff[s]
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.ιSigmaStdSimplex_jointly_surjective : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) {d : ℕ}
  {j : ι} (a : (f.sigmaStdSimplex j).obj (Opposite.op { len := d })),
  ∃ c x, (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := d }))) x = a
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.subset_iUnion : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π → ↑J ⊆ π.iUnion
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.isReal : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K}, NumberField.InfinitePlace.IsRamified k w → (w.comap (algebraMap k K)).IsReal
-- Mathlib.Order.Filter.Map
Filter.map_id : ∀ {α : Type u_1} {f : Filter α}, Filter.map id f = f
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph.0.SimpleGraph.Walk.map.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (Unit → motive u SimpleGraph.Walk.nil) →
              ((v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p)) → motive v x
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.toBitVec_minValueSealed_eq_intMinSealed : ISize.minValueSealed✝.toBitVec = BitVec.Signed.intMinSealed✝ System.Platform.numBits
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  QuasiIsoAt f i ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
-- Init.Data.Bool
Bool.and_or_inj_right_iff : ∀ {m x y : Bool}, (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- Since `Truncated.inclusion` is fully faithful, so is left Kan extension along it.  -/
SSet.Truncated.sk.fullyFaithful : (n : ℕ) → (SSet.Truncated.sk n).FullyFaithful
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring : ∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
  (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f) ∈ Valued.v.valuationSubring
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M),
  Function.Injective ⇑f → f.ker = ⊥
-- Mathlib.Data.Finset.NatDivisors
List.nat_divisors_prod : ∀ (l : List ℕ), l.prod.divisors = (List.map Nat.divisors l).prod
-- Init.PropLemmas
or_right_comm : ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b
-- Init.Data.UInt.Lemmas
UInt8.toUSize_eq_mod_256_iff : ∀ (a : UInt8) (b : USize), a.toUSize = b % 256 ↔ a = b.toUInt8
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.mk.congr_simp : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (left left_1 : X.left ⟶ Y.left)
  (e_left : left = left_1) (right right_1 : X.right ⟶ Y.right) (e_right : right = right_1)
  (w : CategoryTheory.CategoryStruct.comp (L.map left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map right)),
  { left := left, right := right, w := w } = { left := left_1, right := right_1, w := ⋯ }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `μ` is a finite measure then `∫ x in a..b, c ∂μ = (μ (Iic b) - μ (Iic a)) • c`.  -/
intervalIntegral.integral_const_of_cdf : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ] (c : E),
  ∫ (x : ℝ) in a..b, c ∂μ = (μ.real (Set.Iic b) - μ.real (Set.Iic a)) • c
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
contMDiffOn_coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_15 : MemTrivializationAtlas e] [inst_16 : MemTrivializationAtlas e'],
  ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b))
    (e.baseSet ∩ e'.baseSet)
-- Std.Sync.SharedMutex
/-- Creates a new `BaseSharedMutex`.  -/
Std.BaseSharedMutex.new : BaseIO Std.BaseSharedMutex
-- Mathlib.Logic.Equiv.Prod
Equiv.boolProdEquivSum_apply : ∀ (α : Type u_9) (p : Bool × α), (Equiv.boolProdEquivSum α) p = if p.1 = true then Sum.inr p.2 else Sum.inl p.2
-- Init.Core
PProd.mk.inj : ∀ {α : Sort u} {β : Sort v} {fst : α} {snd : β} {fst_1 : α} {snd_1 : β},
  ⟨fst, snd⟩ = ⟨fst_1, snd_1⟩ → fst = fst_1 ∧ snd = snd_1
-- Mathlib.Topology.Order.WithTop
WithBot.isEmbedding_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Topology.IsEmbedding WithBot.some
-- Mathlib.Data.List.Sublists
List.sublistsLen_length : ∀ {α : Type u} (l : List α), List.sublistsLen l.length l = [l]
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.tendsto_meas_vadd_symmDiff : ∀ {G : Type u_4} {X : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_6} {l : Filter ι} {F : ι → Set X},
  IsAddFoelner G μ l F → ∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g +ᵥ F i) (F i)) / μ (F i)) l (nhds 0)
-- Std.Do.Triple.SpecLemmas
Std.Do.WhileVariant.eval : {α : Type u_1} → {ps : Std.Do.PostShape} → Std.Do.WhileVariant α ps → α → ℕ → Std.Do.SPred ps.args
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
/-- A modification of a Gaussian process is a Gaussian process.  -/
ProbabilityTheory.IsGaussianProcess.congr : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : T → Ω → E}
  [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module ℝ E],
  ProbabilityTheory.IsGaussianProcess X P → (∀ (t : T), X t =ᵐ[P] Y t) → ProbabilityTheory.IsGaussianProcess Y P
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- A scheme `X` is separated if it is separated over `⊤_ Scheme`.  -/
AlgebraicGeometry.Scheme.IsSeparated : AlgebraicGeometry.Scheme → Prop
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y Z : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.Hom.right f)
      (CategoryTheory.StructuredArrow.Hom.right g)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A Hausdorff and weakly locally compact space is compactly generated.  -/
instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [T2Space X] [WeaklyLocallyCompactSpace X], CompactlyGeneratedSpace X
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUnopIsoUnopColimit F).hom
      (CategoryTheory.Limits.colimit.ι F j).unop =
    CategoryTheory.Limits.limit.π F.unop (Opposite.unop j)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An `n`-clique in a graph is a set of `n` vertices which are pairwise connected.  -/
SimpleGraph.IsNClique : {α : Type u_1} → SimpleGraph α → ℕ → Finset α → Prop
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ),
  CochainComplex.IsStrictlyLE ((HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A) n
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.Context.mk.injEq : ∀ (cache cache_1 : Bool), ({ cache := cache } = { cache := cache_1 }) = (cache = cache_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfcₙ_comp_re : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] [T2Space A]
  (f : ℝ → ℝ) (a : A),
  autoParam (ContinuousOn f (quasispectrum ℝ ↑(realPart a))) cfcₙ_comp_re._auto_1 →
    autoParam (f 0 = 0) cfcₙ_comp_re._auto_3 →
      autoParam (IsStarNormal a) cfcₙ_comp_re._auto_5 → cfcₙ (fun x => ↑(f x.re)) a = cfcₙ f ↑(realPart a)
-- Mathlib.CategoryTheory.Category.TwoP
/-- Turns a two-pointing into a two-pointed type.  -/
TwoP.of : {X : Type u_3} → TwoPointing X → TwoP
-- Lean.Elab.Import
_private.Lean.Elab.Import.0.Lean.Elab.checkComponentPortability : String → Option String
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).IsContinuous (Opens.grothendieckTopology ↥X)
    (Opens.grothendieckTopology ↥Y)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_symm_apply_left`. -/
Equiv.Perm.SameCycle.symm_apply_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x y → f.SameCycle ((Equiv.symm f) x) y
-- Lean.Meta.Basic
/-- Return `mvarId` kind. Throw an exception if `mvarId` is not declared in the current metavariable context.
 -/
Lean.MVarId.getKind : Lean.MVarId → Lean.MetaM Lean.MetavarKind
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `zipWithLeft'`.  -/
List.zipWithLeft'TR : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → List γ × List β
-- Mathlib.Topology.Order.LeftRightLim
Antitone.tendsto_rightLim_within : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhdsWithin (Function.rightLim f x) (Set.Iic (Function.rightLim f x)))
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀.nonempty_iff : ∀ (X : SSet), Nonempty X.π₀ ↔ X.Nonempty
-- Mathlib.Data.Set.Basic
Set.union_union_union_comm : ∀ {α : Type u} (s t u v : Set α), s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.right_assoc_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.mul)
      (CategoryTheory.CategoryStruct.comp self.actRight h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X B.X B.X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.actRight B.X)
        (CategoryTheory.CategoryStruct.comp self.actRight h))