mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.strictMap (CategoryTheory.Functor.id C) = P
-- Mathlib.Order.Filter.Defs
/-- If a set belongs to a filter, then its superset belongs to the filter as well.  -/
Filter.sets_of_superset : ∀ {α : Type u_1} (self : Filter α) {x y : Set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.card_le_one_iff_eq_bot : ∀ {M : Type u_1} [inst : AddMonoid M] {S : AddSubmonoid M} [inst_1 : Fintype ↥S], Fintype.card ↥S ≤ 1 ↔ S = ⊥
-- Mathlib.Analysis.Normed.Group.Basic
nndist_nnnorm_nnnorm_le : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_counitIso_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : (A × D) × C × E),
  (CategoryTheory.prod.prodμ C D E A).counitIso.inv.app X =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodCongr_symm_apply : ∀ {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {δ : Sort u_8} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (x : β ×' δ),
  (e₁.pprodCongr e₂).symm x = ⟨e₁.symm x.fst, e₂.symm x.snd⟩
-- Init.Data.ByteArray.Bootstrap
List.toList_data_toByteArray : ∀ {l : List UInt8}, l.toByteArray.data.toList = l
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.coe_inf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S T : NonUnitalSubalgebra R A), ↑(S ⊓ T) = ↑S ∩ ↑T
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.mono : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l l' : Filter α}, f =o[l'] g → l ≤ l' → f =o[l] g
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.defaultRatCDF_nonneg : ∀ (q : ℚ), 0 ≤ ProbabilityTheory.defaultRatCDF q
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
IsometryEquiv.refl.eq_1 : ∀ (α : Type u_3) [inst : PseudoEMetricSpace α], IsometryEquiv.refl α = { toEquiv := Equiv.refl α, isometry_toFun := ⋯ }
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- If `F` has a limit, then it has a weak limit.
 -/
CategoryTheory.Limits.instHasWeakLimitOfHasLimit : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.HasWeakLimit F
-- Mathlib.MeasureTheory.Function.LpSeminorm.Trim
MeasureTheory.eLpNormEssSup_trim : ∀ {α : Type u_1} {ε : Type u_3} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.eLpNormEssSup f (μ.trim hm) = MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotalOrZero_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂)
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂),
  CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) =
    CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A finite product of locally path-connected spaces is locally path-connected.  -/
Pi.locallyPathConnectedSpace_of_finite : ∀ {ι : Type u_3} [Finite ι] {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)]
  [∀ (i : ι), LocallyPathConnectedSpace (Z i)], LocallyPathConnectedSpace ((i : ι) → Z i)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons of different weights, strict inequality
version: there is a pigeonhole with the total weight of pigeons in it greater than `b` provided that
the total number of pigeonholes times `b` is less than the total weight of all pigeons.  -/
Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {w : α → M} {b : M} [inst_3 : AddCommMonoid M] [inst_4 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  Fintype.card β • b < ∑ x, w x → ∃ y, b < ∑ x with f x = y, w x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The underlying cone of a kernel fork is mapped to a limit cone if and only if
the mapped kernel fork is limit.  -/
CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              {f : X ⟶ Y} →
                (c : CategoryTheory.Limits.KernelFork f) →
                  (G : CategoryTheory.Functor C D) →
                    [inst_4 : G.PreservesZeroMorphisms] →
                      CategoryTheory.Limits.IsLimit (G.mapCone c) ≃ CategoryTheory.Limits.IsLimit (c.map G)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEquiv_symm_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)}
  (x : F.obj X) (Y : C) (f : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaEquiv.symm x).app Y)) f =
    (CategoryTheory.ConcreteCategory.hom (F.map f)) x
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.wideCospan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {I : Type u_1}
  [Finite I] {i : C} {j : I → C} (f : (x : I) → j x ⟶ i),
  ∃ k fki g, ∀ (x : I), CategoryTheory.CategoryStruct.comp (g x) (f x) = fki
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given full range as an array in ascending order.
 -/
Std.Rii.toArray : {α : Type u_1} →
  [Std.PRange.UpwardEnumerable α] →
    [Std.PRange.Least? α] →
      Std.Rii α →
        [inst : Std.Iterator (Std.Rxi.Iterator α) Id α] → [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] → Array α
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- The injection `x ↦ LinearMap.inr E F x` as a linear isometry.  -/
LinearIsometry.inr : (𝕜 : Type u_9) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_10) →
      (F : Type u_11) →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] → [inst_3 : SeminormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → F →ₗᵢ[𝕜] E × F
-- Mathlib.Data.Set.Prod
Set.exists_prod_set : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β → Prop},
  (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_fst : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : E × F), ((WithCStarModule.equiv A (E × F)).symm x).1 = x.1
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.applyReplacementFun.visitForall : Mathlib.Tactic.Translate.TranslateData →
  Lean.Expr →
    optParam (Array Lean.Expr) #[] → optParam Lean.LocalContext { } → Mathlib.Tactic.Translate.ReplacementM Lean.Expr
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.lattice : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Lattice (FractionalIdeal S P)
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.BisimO.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2)
  (x x_1 : Option (Stream'.Seq1 α)) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s')))
  (h_3 : (x x_2 : Option (Stream'.Seq1 α)) → motive x x_2),
  (x = none → x_1 = none → False) →
    (∀ (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α), x = some (a, s) → x_1 = some (a', s') → False) →
      (match x, x_1 with
        | none, none => h_1 ()
        | some (a, s), some (a', s') => h_2 a s a' s'
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.continuousLinearEquivAt_prod : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : TopologicalSpace B] {F₁ : Type u_3}
  [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_4}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [inst_5 : NormedAddCommGroup F₂]
  [inst_6 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_8 : (x : B) → AddCommMonoid (E₁ x)] [inst_9 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_10 : (x : B) → AddCommMonoid (E₂ x)] [inst_11 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : FiberBundle F₂ E₂] {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂] {x : B} (hx : x ∈ (e₁.prod e₂).baseSet),
  Bundle.Trivialization.continuousLinearEquivAt 𝕜 (e₁.prod e₂) x hx =
    (Bundle.Trivialization.continuousLinearEquivAt 𝕜 e₁ x ⋯).prodCongr
      (Bundle.Trivialization.continuousLinearEquivAt 𝕜 e₂ x ⋯)
-- Batteries.Tactic.Alias
/-- Get the old alias information for a name.  -/
Batteries.Tactic.Alias.getOldAliasInfo? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Batteries.Tactic.Alias.AliasInfo)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.ofLeftInverse_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : ↥f.srange), (AddEquiv.ofLeftInverse f h).symm a = g ↑a
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.withNeededEqTelescope.go : {α : Type} →
  Array Lean.Expr →
    (Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) →
      List Lean.Expr → List Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Init.Data.List.Perm
List.isPerm.eq_def : ∀ {α : Type u} [inst : BEq α] (x x_1 : List α),
  x.isPerm x_1 =
    match x, x_1 with
    | [], l₂ => l₂.isEmpty
    | a :: l₁, l₂ => l₂.contains a && l₁.isPerm (l₂.erase a)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.canLiftSet : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α},
  CanLift (Set α) (TopologicalSpace.OpenNhdsOf x) SetLike.coe fun s => IsOpen s ∧ x ∈ s
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β] (f : α ≃+ β)
  (h : ∀ {a b : α}, f.toFun a ≤ f.toFun b ↔ a ≤ b), ⇑{ toAddEquiv := f, map_le_map_iff' := h } = ⇑f
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instFunLike : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : Star A] → [inst_2 : NonUnitalNonAssocSemiring B] → [inst_3 : Star B] → FunLike (A →⋆ₙ+* B) A B
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_or_nonempty : ∀ (α : Sort u_1), IsEmpty α ∨ Nonempty α
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict.0.QuasispectrumRestricts.termσₙ : Lean.ParserDescr
-- Lean.Expr
Lean.Nat.mkInstDiv : Lean.Expr
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap_pruneLT_eq_prependMapGT : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (z : Std.DTreeMap.Internal.Zipper α β) (lowerBound : α),
      Std.DTreeMap.Internal.Zipper.prependMap (Std.DTreeMap.Internal.Impl.pruneLT✝ t lowerBound) z =
        Std.DTreeMap.Internal.Zipper.prependMapGT t lowerBound z
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- Returns `some (charInst, c)` if the current ring has a nonzero characteristic `c`.  -/
Lean.Meta.Grind.Arith.CommRing.nonzeroCharInst? : {m : Type → Type} → [Monad m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m (Option (Lean.Expr × ℕ))
-- Lean.Parser.Term
Lean.Parser.Term.letRecDecl.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.BitVec.BasicAux
/-- Adds two bitvectors. This can be interpreted as either signed or unsigned addition modulo `2^n`.
Usually accessed via the `+` operator.

SMT-LIB name: `bvadd`.
 -/
BitVec.add : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.det_kroneckerTMul : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [inst : CommRing R] [inst_1 : CommRing α]
  [inst_2 : CommRing β] [inst_3 : Algebra R α] [inst_4 : Algebra R β] [inst_5 : Fintype m] [inst_6 : Fintype n]
  [inst_7 : DecidableEq m] [inst_8 : DecidableEq n] (A : Matrix m m α) (B : Matrix n n β),
  (Matrix.kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Model.0.Lean.Meta.Grind.Arith.Linear.hasType : Lean.Expr → Lean.Meta.Grind.ENode → Lean.MetaM Bool
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.stRun.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_3} {k : K} (motive : Turing.TM2to1.StAct K Γ σ k → Sort u_4)
  (f : σ → Γ k) (h_1 : (f : σ → Γ k) → motive (Turing.TM2to1.StAct.push f))
  (h_2 : (f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.peek f))
  (h_3 : (f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.pop f)),
  (match Turing.TM2to1.StAct.push f with
    | Turing.TM2to1.StAct.push f => h_1 f
    | Turing.TM2to1.StAct.peek f => h_2 f
    | Turing.TM2to1.StAct.pop f => h_3 f) =
    h_1 f
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.measure_cast : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)] {a b : ℕ} (h : a = b)
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)), MeasureTheory.Measure.map (cast ⋯) (μ a) = μ b
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.compl_adjMatrix_completeGraph : ∀ (α : Type u_1) (V : Type u_2) [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq α] [inst_3 : DecidableEq V],
  (SimpleGraph.adjMatrix α (SimpleGraph.completeGraph V)).compl = 0
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- the extension of a valuation on a division ring to its completion.  -/
Valued.extensionValuation : {K : Type u_1} →
  [inst : Field K] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [hv : Valued K Γ₀] → Valuation (UniformSpace.Completion K) Γ₀
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.mk.congr_simp : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (toEquiv toEquiv_1 : A ≃ B) (e_toEquiv : toEquiv = toEquiv_1)
  (map_mul' : ∀ (x y : A), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y)
  (commutes' : ∀ (r : R), toEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r),
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add', commutes' := commutes' } =
    { toEquiv := toEquiv_1, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- Version of the Kuratowski embedding for nonempty compacts  -/
NonemptyCompacts.kuratowskiEmbedding : (α : Type u) →
  [inst : MetricSpace α] → [CompactSpace α] → [Nonempty α] → TopologicalSpace.NonemptyCompacts ↥(lp (fun x => ℝ) ⊤)
-- Mathlib.Order.Directed
Directed.eq_1 : ∀ {α : Type u_1} {ι : Sort u_3} (r : α → α → Prop) (f : ι → α),
  Directed r f = ∀ (x y : ι), ∃ z, r (f x) (f z) ∧ r (f y) (f z)
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.neg_one_pow_smul_map_insertNth : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N) (p : Fin (n + 1)) (x : M)
  (v : Fin n → M), (-1) ^ ↑p • f (p.insertNth x v) = f (Matrix.vecCons x v)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map `Zⁿ(H, A) ⟶ Zⁿ(G, B)` sending `x : Hⁿ → A` to
`(g : Gⁿ) ↦ φ (x (f ∘ g))`.  -/
groupCohomology.cocyclesMap : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k H} →
          {B : Rep.{u, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (n : ℕ) → groupCohomology.cocycles A n ⟶ groupCohomology.cocycles B n
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.trans_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ p₂ : Path x₀ x₁} (F : p₀.Homotopy p₁) (G : p₁.Homotopy p₂)
  (x : ↑unitInterval × ↑unitInterval),
  (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_single_mul_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : DecidableEq G] (x : AddMonoidAlgebra k G)
  (r : k) (a : G), (AddMonoidAlgebra.single a r * x).coeff.support ⊆ Finset.image (fun x => a + x) x.coeff.support
-- Mathlib.NumberTheory.Divisors
Nat.sum_div_divisors : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (f : ℕ → α), ∑ d ∈ n.divisors, f (n / d) = n.divisors.sum f
-- Mathlib.Algebra.Module.Presentation.RestrictScalars
/-- A presentation of the restriction of scalars from `B` to `A` of a `B`-module `M`,
given a presentation of `M` as a `B`-module, a presentation of `B` as an `A`-module,
and an additional data.  -/
Module.Presentation.restrictScalars : {B : Type u_1} →
  [inst : Ring B] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module B M] →
          [inst_3 : DecidableEq B] →
            (presM : Module.Presentation B M) →
              [inst_4 : DecidableEq presM.G] →
                {A : Type u_3} →
                  [inst_5 : CommRing A] →
                    [inst_6 : Algebra A B] →
                      [inst_7 : Module A M] →
                        [IsScalarTower A B M] →
                          (presB : Module.Presentation A B) → presM.RestrictScalarsData presB → Module.Presentation A M
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_eq_forIn : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] [inst_4 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  {it : Std.Iter β}, it.length = (forIn it 0 fun x acc => pure (ForInStep.yield (acc + 1))).run
-- Mathlib.Topology.Order.Bornology
Bornology.IsBounded.eq_1 : ∀ {α : Type u_2} [inst : Bornology α] (s : Set α), Bornology.IsBounded s = Bornology.IsCobounded sᶜ
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'} {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}
  {g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))},
  HasMFDerivAt[u] g (f x) g' → HasMFDerivAt[s] f x f' → s ⊆ f ⁻¹' u → HasMFDerivAt[s] (g ∘ f) x (g' ∘SL f')
-- Init.Control.Lawful.Instances
ReaderT.run_liftWith : ∀ {m : Type u → Type u_1} {ρ α : Type u} [inst : Monad m]
  (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m α) (ctx : ρ),
  (liftWith f).run ctx = f fun {β} x => x.run ctx
-- Mathlib.Order.RelSeries
RelSeries.eraseLast_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.eraseLast.length = p.length - 1
-- Mathlib.Topology.Category.Stonean.Basic
CompHaus.Gleason : ∀ (X : CompHaus), CategoryTheory.Projective X ↔ ExtremallyDisconnected ↑X.toTop
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Metrizable.Basic
/-- A topological space is metrizable if there exists a metric space structure compatible with the
topology. To minimize imports, we implement this class in terms of the existence of a
countably generated uniformity inducing the topology, which is mathematically
equivalent.
To endow such a space with a compatible uniformity, use
`letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X`.
To endow such a space with a compatible distance, use
`letI : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X`.  -/
TopologicalSpace.MetrizableSpace : (X : Type u_5) → [t : TopologicalSpace X] → Prop
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.HasMapBifunctor.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ K₁_1 : HomologicalComplex C₁ c₁),
  K₁ = K₁_1 →
    ∀ (K₂ K₂_1 : HomologicalComplex C₂ c₂),
      K₂ = K₂_1 →
        ∀ (F F_1 : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) (e_F : F = F_1)
          [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
          (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c],
          K₁.HasMapBifunctor K₂ F c = K₁_1.HasMapBifunctor K₂_1 F_1 c
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.ofArray_eq_ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (a : Array (α × β)),
  Std.HashMap.Raw.ofArray a = Std.HashMap.Raw.ofList a.toList
-- Mathlib.Control.Traversable.Basic
Traversable.mk : {t : Type u → Type u} →
  [toFunctor : Functor t] →
    ({m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → t α → m (t β)) → Traversable t
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.ObjectProperty.homMk_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory), CategoryTheory.ObjectProperty.homMk 0 = 0