mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.head_replace : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a b : α} (w : l.replace a b ≠ []),
  (l.replace a b).head w = if (a == l.head ⋯) = true then b else l.head ⋯
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.Context.mk.sizeOf_spec : ∀ (α : Lean.Expr) (univ : Lean.Level) (α0 : Lean.Expr) (isGroup : Bool) (inst : Lean.Expr),
  sizeOf { α := α, univ := univ, α0 := α0, isGroup := isGroup, inst := inst } =
    1 + sizeOf α + sizeOf univ + sizeOf α0 + sizeOf isGroup + sizeOf inst
-- Lean.Elab.DocString
/-- Records a deferred check. Deferred checks represent a docstring task that can't be carried out at
the elaboration site, such as resolving a forward reference. Recorded checks include the current
namespace, open namespaces, and options, but not the local context.

The origin site `ref` is used to record the origin of the deferred check. Returns the check's index
within the current docstring, which the docstring's AST stores to refer back to it.

The saved deferred check is not associated with the docstring or module doc until it is actually
added to the environment. After this call, the internal state stores `Name.anonymous`.
 -/
Lean.Doc.addDeferredCheck : Dynamic → Array Lean.Name → Lean.Syntax → Lean.Doc.DocM ℕ
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
/-- An approximate subgroup in a group is a symmetric set `A` containing the identity and such that
`A * A` can be covered by a small number of translates of `A`.

In practice, we will take `K` fixed and `A` large but finite.
 -/
IsApproximateSubgroup : {G : Type u_1} → [Group G] → ℝ → Set G → Prop
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toOrderIso_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β],
  Function.Injective OrderAddMonoidIso.toOrderIso
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.ciInf_mem_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α) {s : Set ι},
  s.Finite → (∃ x ∈ s, f x ≤ sInf ∅) → ⨅ i ∈ s, f i ∈ f '' s
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `add_apply`. -/
MultilinearMap.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_injective : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], Function.Injective CentroidHom.toEnd
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_zero : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N], LinearMap.baseChange A 0 = 0
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.leadingCoeff 1 = 1
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool}
  {k : α}, k ∈ Std.HashSet.filter f m → k ∈ m
-- Mathlib.SetTheory.Lists
Lists.equiv_atom : ∀ {α : Type u_1} {a : α} {l : Lists α}, (Lists.atom a).Equiv l ↔ Lists.atom a = l
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insertMany_cons : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {l : List (α × β)} {k : α} {v : β}, m.insertMany ((k, v) :: l) = (m.insert k v).insertMany l
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The Euler characteristic of a finite bounded order.  -/
IncidenceAlgebra.eulerChar : (𝕜 : Type u_2) →
  (α : Type u_5) →
    [AddCommGroup 𝕜] → [One 𝕜] → [inst : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → [BoundedOrder α] → 𝕜
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.bot_isUniform : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} (G : SimpleGraph α) [inst_4 : DecidableRel G.Adj] {ε : 𝕜},
  0 < ε → ⊥.IsUniform G ε
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Access the first component of an element of `YonedaCollection F X`.  -/
CategoryTheory.OverPresheafAux.YonedaCollection.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
        {X : C} → CategoryTheory.OverPresheafAux.YonedaCollection F X → (CategoryTheory.yoneda.obj X ⟶ A)
-- Mathlib.Analysis.Normed.Field.Basic
norm_zpow : ∀ {α : Type u_2} [inst : NormedDivisionRing α] (a : α) (n : ℤ), ‖a ^ n‖ = ‖a‖ ^ n
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.topologicalClosure_minimal : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G] (s : AddSubgroup G)
  {t : AddSubgroup G}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instPartialOrder : {M : Type u_1} → [inst : CommMonoidWithZero M] → [IsCancelMulZero M] → PartialOrder (Associates M)
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.apply_lie' : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : CommRing A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {σ : A₁ →ₐ[R] A₂} {L₁ : Type u_8} {L₂ : Type u_9}
  [inst_5 : LieRing L₁] [inst_6 : Module A₁ L₁] [inst_7 : LieRingModule L₁ A₁] [inst_8 : LieAlgebra R L₁]
  [inst_9 : LieRing L₂] [inst_10 : Module A₂ L₂] [inst_11 : LieRingModule L₂ A₂] [inst_12 : LieAlgebra R L₂]
  (self : LieRinehartAlgebra.Hom σ L₁ L₂) (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅self.toLieHom x, σ a⁆
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.sinh` is real analytic.  -/
Real.analyticOn_sinh : ∀ {s : Set ℝ}, AnalyticOn ℝ Real.sinh s
-- Aesop.Tree.Data
Aesop.instInhabitedMVarClusterData : {a a_1 : Type} → Inhabited (Aesop.MVarClusterData a a_1)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- The images by `logEmbedding` of a family of units of maximal rank form a basis of `logSpace K`.
 -/
NumberField.Units.basisOfIsMaxRank : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} →
        NumberField.Units.IsMaxRank u →
          Module.Basis (Fin (NumberField.Units.rank K)) ℝ (NumberField.Units.dirichletUnitTheorem.logSpace K)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_injective : ∀ {m : Type u_2} {n : Type u_3} {α : Type v}, Function.Injective Matrix.transpose
-- Std.Http.Server.Connection
/-- Processes all H1 events from a single machine step, updating the connection state.
Handles keep-alive resets, body-size tracking, `Expect: 100-continue`, and parse errors.
Returns the updated state; stops early on `.failed`.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.processH1Events : {σ β : Type} →
  [Std.Http.Server.Handler σ] →
    [Std.Http.Body β] →
      σ →
        Std.Http.Config →
          Std.CancellationContext →
            Array (Std.Http.Protocol.H1.Event Std.Http.Protocol.H1.Direction.receiving) →
              Std.Http.Server.Connection.ConnectionState✝ β →
                Std.Async.Async (Std.Http.Server.Connection.ConnectionState✝ β)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Morphisms satisfying `(monomorphism C).presheaf` are in particular monomorphisms.  -/
CategoryTheory.MorphismProperty.presheaf_monomorphisms_le_monomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MorphismProperty.monomorphisms C).presheaf ≤
    CategoryTheory.MorphismProperty.monomorphisms (CategoryTheory.Functor Cᵒᵖ (Type v₁))
-- Mathlib.Algebra.Order.Monoid.Basic
/-- Pullback an `IsOrderedMonoid` under an injective map.  -/
Function.Injective.isOrderedMonoid : ∀ {α : Type u} {β : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α] [inst_3 : CommMonoid β]
  [inst_4 : Preorder β] (f : β → α),
  (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) → IsOrderedMonoid β
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.instEquivLike : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → EquivLike (X ≃ₜ Y) X Y
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffSMulOfNatWithTopENatOfContinuousSMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M] [ContinuousSMul G M],
  ContMDiffSMul I I' 0 G M
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F G : CategoryTheory.Functor C D} {app : (X : C) → F.obj X ⟶ G.obj X}
  {naturality :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f))
      CategoryTheory.NatTrans.naturality._autoParam}
  {app_1 : (X : C) → F.obj X ⟶ G.obj X}
  {naturality_1 :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app_1 Y) = CategoryTheory.CategoryStruct.comp (app_1 X) (G.map f))
      CategoryTheory.NatTrans.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- A set of nonzero vectors is linearly independent if and only if,
given a point `p₁`, the vectors added to `p₁` and `p₁` itself are
affinely independent.  -/
linearIndependent_set_iff_affineIndependent_vadd_union_singleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set V},
  (∀ v ∈ s, v ≠ 0) → ∀ (p₁ : P), (LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun p => ↑p
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.isTrivial : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Bool
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.StrictPseudofunctor.mapAdjunction_counit' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.StrictPseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  (F.mapAdjunction adj).counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (F.map₂ adj.counit) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Topology.Category.TopCat.Basic
/-- The trivial topology on any type.  -/
TopCat.trivial : CategoryTheory.Functor (Type u) TopCat
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.instIsMulTorsionFree : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [IsMulTorsionFree G], IsMulTorsionFree ↥H
-- Mathlib.Algebra.Group.Basic
add_ne_right : ∀ {M : Type u_4} [inst : AddMonoid M] [IsRightCancelAdd M] {a b : M}, a + b ≠ b ↔ a ≠ 0
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheoremsExt : Type
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- A lift of a 2-morphism to the free bicategory.
This should only exist for "structural" 2-morphisms.  -/
Mathlib.Tactic.BicategoryCoherence.LiftHom₂.lift : {B : Type u} →
  {inst : CategoryTheory.Bicategory B} →
    {a b : B} →
      {f g : a ⟶ b} →
        {inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f} →
          {inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g} →
            (η : f ⟶ g) →
              [self : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] →
                Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f ⟶ Mathlib.Tactic.BicategoryCoherence.LiftHom.lift g
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.toGroupSeminorm_eq_coe : ∀ {E : Type u_3} [inst : Group E] {p : GroupNorm E}, ⇑p.toGroupSeminorm = ⇑p
-- Mathlib.Util.Export
Lean.Export.State.mk.sizeOf_spec : ∀ (names : Lean.Export.Alloc Lean.Name) (levels : Lean.Export.Alloc Lean.Level) (exprs : Lean.Export.Alloc Lean.Expr)
  (defs : Std.HashSet Lean.Name) (stk : Array (Bool × Lean.Export.Entry)),
  sizeOf { names := names, levels := levels, exprs := exprs, defs := defs, stk := stk } =
    1 + sizeOf names + sizeOf levels + sizeOf exprs + sizeOf defs + sizeOf stk
-- Mathlib.Algebra.Homology.AlternatingConst
ChainComplex.alternatingConst_map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) (x : ℕ), (ChainComplex.alternatingConst.map f).f x = f
-- Mathlib.Order.Directed
/-- A class for an `IsDirected` relation `≤`.  -/
IsDirectedOrder : (α : Type u_5) → [LE α] → Prop
-- Mathlib.Topology.Defs.Filter
/-- `Filter.coclosedCompact` is the filter generated by complements to closed compact sets.
In a Hausdorff space, this is the same as `Filter.cocompact`.  -/
Filter.coclosedCompact : (X : Type u_1) → [TopologicalSpace X] → Filter X
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β) (x : α),
  Set.IccExtend h f x = f ⟨max a (min b x), ⋯⟩
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.NatTrans.mapHomotopyCategory_id : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (c : ComplexShape ι) (F : CategoryTheory.Functor V W) [inst_4 : F.Additive],
  CategoryTheory.NatTrans.mapHomotopyCategory (CategoryTheory.CategoryStruct.id F) c =
    CategoryTheory.CategoryStruct.id (F.mapHomotopyCategory c)
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.comap_ne_bot_of_algebraic_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {I : Ideal S} [inst_2 : Algebra R S]
  [IsDomain S] {x : S}, x ≠ 0 → x ∈ I → IsAlgebraic R x → Ideal.comap (algebraMap R S) I ≠ ⊥
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_two_mul_le_mul_multinomial : ∀ {ι : Type u_1} {s : Finset ι} {f : ι → ℕ},
  (Nat.multinomial s fun i => 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * Nat.multinomial s f
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {l : List ((a : α) × β a)} {f : (a : α) → β a → γ a},
  Std.Internal.List.keys (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Std.Internal.List.keys l
-- Init.Data.BitVec.Lemmas
/-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow.
Thus, `(x * y).toNat = x.toNat * y.toNat`.
 -/
BitVec.toNat_mul_of_lt : ∀ {w : ℕ} {x y : BitVec w}, x.toNat * y.toNat < 2 ^ w → (x * y).toNat = x.toNat * y.toNat
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_5 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (P Q : RegularExpression α),
  (P.comp Q).deriv x = if P.matchEpsilon = true then P.deriv x * Q + Q.deriv x else P.deriv x * Q
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- This is the default implementation of the `IteratorLoop` class.
It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
implementations are possible and should be used instead.
 -/
Std.IteratorLoop.defaultImplementation : {β α : Type w} →
  {m : Type w → Type w'} → {n : Type x → Type x'} → [Monad n] → [inst : Std.Iterator α m β] → Std.IteratorLoop α m n
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrM : Type → Type
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R 1 = 2 * Polynomial.X
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E), balancedCore 𝕜 s ⊆ s
-- Mathlib.Data.Int.ModEq
Int.add_modEq_left : ∀ {n a : ℤ}, n + a ≡ a [ZMOD n]
-- Init.Data.Range.Polymorphic.PRange
/-- This type class allows taking the intersection of a left-open right-unbounded range with a
left-closed right-open range, resulting in another left-closed right-open range.
 -/
Std.Roi.HasRcoIntersection : Type w → Type w
-- Mathlib.Data.PFun
/-- Turns a function into a partial function to a subtype.  -/
PFun.toSubtype : {α : Type u_1} → {β : Type u_2} → (p : β → Prop) → (α → β) → α →. Subtype p
-- Lean.Elab.Tactic.RCases
/-- An alternation / variant pattern `p1 | p2 | p3`  -/
Lean.Elab.Tactic.RCases.RCasesPatt.alts : Lean.Syntax → List Lean.Elab.Tactic.RCases.RCasesPatt → Lean.Elab.Tactic.RCases.RCasesPatt
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.size_cons : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β},
  Std.DTreeMap.Internal.Zipper.size✝ (Std.DTreeMap.Internal.Zipper.cons k v t it) =
    1 + t.treeSize + Std.DTreeMap.Internal.Zipper.size✝ it
-- Mathlib.Topology.UniformSpace.Separation
UniformSpace.to_regularSpace : ∀ {α : Type u} [inst : UniformSpace α], RegularSpace α
-- Mathlib.Topology.UniformSpace.Uniformizable
/-- To construct a real-valued function separating a point `x` from a closed set in a uniform
space, we recursively construct pairs of a closed set `c` contained in an open set `u`
satisfying the following predicate: `u` is a thickening of `c` by some entourage `s`,
in the sense that `c` is the closure of the ball centered at `x`
associated to some open entourage `uc`, and `u` contains the ball centered at `x`
associated to the composition `s ○ uc ○ s`.  -/
_private.Mathlib.Topology.UniformSpace.Uniformizable.0.IsThickening : {X : Type u_1} → [UniformSpace X] → Set X → Set X → Prop
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_one₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀] {n : ℕ},
  0 ≤ a → a ≤ 1 → a ^ n ≤ 1
-- Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
AlgebraicTopology.DoldKan.MorphComponents.postComp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} {n : ℕ}
  {Z Z' : C} (f : AlgebraicTopology.DoldKan.MorphComponents X n Z) (h : Z ⟶ Z'),
  f.postComp h =
    { a := CategoryTheory.CategoryStruct.comp f.a h, b := fun i => CategoryTheory.CategoryStruct.comp (f.b i) h }
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.mk_hom : ∀ {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.WeaklyEtale f],
  (AlgebraicGeometry.Scheme.ProEt.mk f).hom = f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_diff!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff! m₂).getKey! k = default
-- Init.GetElem
Lean.Syntax.instGetElemNatTrue : GetElem Lean.Syntax ℕ Lean.Syntax fun x x_1 => True
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCyclesIso_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hj : c.next i = j) (h : K.d i j = 0)
  [inst_2 : K.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.iCyclesIso i j hj h).inv =
    CategoryTheory.CategoryStruct.id (K.cycles i)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instSMulHom : {R : Type u} →
  [inst : Semiring R] →
    {M N : SemimoduleCat R} →
      {S : Type u_1} → [inst_1 : Monoid S] → [inst_2 : DistribMulAction S ↑N] → [SMulCommClass R S ↑N] → SMul S (M ⟶ N)
-- Mathlib.MeasureTheory.Measure.AddContent
/-- An additive content is a set function with value 0 at the empty set which is finitely additive
on a given set of sets.  -/
MeasureTheory.AddContent : {α : Type u_1} → (G : Type u_2) → [AddCommMonoid G] → Set (Set α) → Type (max u_1 u_2)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_fintype : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) [MeasurableSingletonClass α] (s : Set α) [inst_2 : Fintype α],
  p.toMeasure s = ∑ x, s.indicator (⇑p) x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_singleton_append : ∀ {m n : ℕ}, m < n → (m<...=n).toArray = #[m + 1] ++ ((m + 1)<...=n).toArray
-- Mathlib.Data.Nat.ModEq
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`  -/
Nat.ModEq.cancel_left_div_gcd : ∀ {m a b c : ℕ}, 0 < m → c * a ≡ c * b [MOD m] → a ≡ b [MOD m / m.gcd c]
-- Batteries.Data.Nat.Bisect
Nat.avg_comm : ∀ (a b : ℕ), a.avg b = b.avg a
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.image : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A],
  SpectrumRestricts a f → f '' spectrum S a = spectrum R a
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.ofNatTrans_toSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (ε : CategoryTheory.Functor.id C ⟶ F) (G : CategoryTheory.Functor C C),
  (CategoryTheory.SmallObject.SuccStruct.ofNatTrans ε).toSucc G = G.whiskerLeft ε
-- Mathlib.Logic.Small.Defs
instNontrivialShrink : ∀ {α : Type u} [inst : Small.{v, u} α] [Nontrivial α], Nontrivial (Shrink.{v, u} α)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.toMonoidWithZeroHom : {R : Type u_2} → [inst : NonAssocRing R] → MulRingSeminorm R → R →*₀ ℝ
-- Init.Data.Option.Attach
/-- Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`Option {x // P x}` is the same as the input `Option α`.
 -/
_private.Init.Data.Option.Attach.0.Option.attachWithImpl : {α : Type u_1} → (o : Option α) → (P : α → Prop) → (∀ (x : α), o = some x → P x) → Option { x // P x }
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opSymm_d : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm) (i j : ι),
  X.opSymm.d i j = (X.d j i).op
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.add.inj : ∀ {a b a_1 b_1 : Lean.Grind.Linarith.Expr}, a.add b = a_1.add b_1 → a = a_1 ∧ b = b_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hᵢ(G, A)` is isomorphic
to the homology of the short complex of `k`-modules `A --(ρ(g) - 𝟙)--> A --N--> A` when `i` is
nonzero and even.  -/
Rep.FiniteCyclicGroup.groupHomologyIsoEven : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [inst_2 : Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            [DecidableEq G] →
              (∀ (x : G), x ∈ Subgroup.zpowers g) →
                (i : ℕ) →
                  [h₀ : NeZero i] → Even i → (groupHomology A i ≅ (Rep.FiniteCyclicGroup.subCompNormHom A g).homology)