mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparisonNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.Limits.HasBinaryCoproducts D]
  (F : CategoryTheory.Functor C D) (A B : C),
  (CategoryTheory.Limits.coprodComparisonNatTrans F A).app B = CategoryTheory.Limits.coprodComparison F A B
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.isIntegral_of_isAffine_of_isDomain : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [Nonempty ↥X]
  [IsDomain ↑(X.presheaf.obj (Opposite.op ⊤))], AlgebraicGeometry.IsIntegral X
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderivWithin_comp_smul_eq_fderivWithin_smul : ∀ {𝕜 : 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] {f : E → F}
  {s : Set E} {x : E} (c : 𝕜), fderivWithin 𝕜 (fun x => f (c • x)) s x = fderivWithin 𝕜 (c • f) (c • s) (c • x)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hom_comp : ∀ {X Y Z : PartOrdEmb} (f : X ⟶ Y) (g : Y ⟶ Z),
  PartOrdEmb.Hom.hom (CategoryTheory.CategoryStruct.comp f g) =
    RelEmbedding.trans (PartOrdEmb.Hom.hom f) (PartOrdEmb.Hom.hom g)
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- **Alias** of the reverse direction of `Submonoid.saturation_le_iff_le`. -/
Submonoid.saturation_le_of_le : ∀ {M : Type u_1} [inst : MulOneClass M] {a : Submonoid M} {b : SaturatedSubmonoid M},
  a ≤ b.toSubmonoid → a.saturation ≤ b
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.anti : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {l' : Filter α},
  Filter.EventuallyConst f l → l' ≤ l → Filter.EventuallyConst f l'
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.comp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (_X _Y _Z : C),
  CategoryTheory.WithTerminal.comp = fun f g => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.RepresentationTheory.FDRep
FDRep.dualTensorIsoLinHom_hom_hom : ∀ {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),
  (FDRep.dualTensorIsoLinHom ρV W).hom.hom = CategoryTheory.ConcreteCategory.ofHom (dualTensorHom k V ↑W.V)
-- Lean.Meta.Structure
/-- Overrides to param binders to apply after param binder info inference.  -/
Lean.Meta.StructProjDecl.paramInfoOverrides : Lean.Meta.StructProjDecl → List (Option Lean.BinderInfo)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
mulEquivOfOrderOfEq_symm_apply_gen : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g)
  {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g'),
  (mulEquivOfOrderOfEq hg hg' h).symm g' = g
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.mem_positive : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : PartialOrder E]
  [inst_7 : IsOrderedAddMonoid E] [inst_8 : PosSMulMono R E] [inst_9 : OrderClosedTopology E] {x : E},
  x ∈ ProperCone.positive R E ↔ 0 ≤ x
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.id_apply : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A : TopRep k G) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
/-- `SeparationQuotient.mk` as a `MonoidHom`.  -/
SeparationQuotient.mkMonoidHom : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : MulOneClass M] → [inst_2 : ContinuousMul M] → M →* SeparationQuotient M
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedErasureFrom : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.Algebra.Order.Field.Basic
le_of_neg_of_one_div_le_one_div : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → 1 / a ≤ 1 / b → b ≤ a
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.left_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → I ⊆ M.E
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
isTheta_deriv_ofReal_cpow_const_atTop : ∀ {c : ℂ}, c ≠ 0 → (deriv fun x => ↑x ^ c) =Θ[Filter.atTop] fun x => x ^ (c.re - 1)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ), (MvPowerSeries.coeff 0) (MvPowerSeries.X s) = 0
-- Mathlib.Util.Notation3
/-- Adds all the names in `boundNames` to the local context
with types that are fresh metavariables.
This is used for example when initializing `p` in `(scoped p => ...)` when elaborating `...`.  -/
Mathlib.Notation3.setupLCtx : Lean.LocalContext → Array Lean.Name → Lean.MetaM (Lean.LocalContext × Std.HashMap Lean.FVarId Lean.Name)
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.centerToAddOpposite.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G], AddSubgroup.centerToAddOpposite G = AddSubmonoid.centerToAddOpposite
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.NameSetModPrivate.ofArray : Array Lean.Name → Lean.Server.Completion.NameSetModPrivate✝
-- Init.Core
/-- A _subsingleton_ is a type with at most one element. It is either empty or has a unique element.

All propositions are subsingletons because of proof irrelevance: false propositions are empty, and
all proofs of a true proposition are equal to one another. Some non-propositional types are also
subsingletons.
 -/
Subsingleton : Sort u → Prop
-- Mathlib.Data.Set.Card
Set.subset_iff_eq_of_ncard_le : ∀ {α : Type u_1} {s t : Set α},
  t.ncard ≤ s.ncard → autoParam t.Finite Set.subset_iff_eq_of_ncard_le._auto_1 → (s ⊆ t ↔ s = t)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
iteratedDerivWithin_tsum_cexp_eq : ∀ (k : ℕ) (z : UpperHalfPlane),
  iteratedDerivWithin k (fun z => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n)
      UpperHalfPlane.upperHalfPlaneSet ↑z =
    ∑' (n : ℕ),
      iteratedDerivWithin k (fun s => Complex.exp (2 * ↑Real.pi * Complex.I * s) ^ n) UpperHalfPlane.upperHalfPlaneSet
        ↑z
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommSemiRingCat.Hom.mk.sizeOf_spec : ∀ {R S : CommSemiRingCat} (hom' : ↑R →+* ↑S), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_unzeroD_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithZero α} {a b : α}, x ≠ 0 → (b < WithZero.unzeroD a x ↔ ↑b < x)
-- Mathlib.Algebra.Order.Ring.Abs
one_lt_sq_iff_one_lt_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), 1 < a ^ 2 ↔ 1 < |a|
-- Mathlib.Analysis.Normed.Lp.Matrix
/-- A copy of `toLpLin_mul` that works for `simp`, for the common case where the domain and codomain
have the same norm.  -/
Matrix.toLpLin_mul_same : ∀ {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : CommRing R] (p : ENNReal) [inst_3 : Fintype o] [inst_4 : DecidableEq o] (A : Matrix m n R)
  (B : Matrix n o R), (Matrix.toLpLin p p) (A * B) = (Matrix.toLpLin p p) A ∘ₗ (Matrix.toLpLin p p) B
-- Mathlib.Data.Finset.Update
/-- If one replaces the variables indexed by a finite set `t`, then `f` no longer depends on
those variables.  -/
DependsOn.updateFinset : ∀ {ι : Type u_2} {π : ι → Type u_3} [inst : DecidableEq ι] {α : Type u_1} {f : ((i : ι) → π i) → α} {s : Set ι},
  DependsOn f s → ∀ {t : Finset ι} (y : (i : ↥t) → π ↑i), DependsOn (fun x => f (Function.updateFinset x t y)) (s \ ↑t)
-- Qq.Macro
/-- Maps quoted expressions (of type Expr) in the old context to expressions in the new context  -/
Qq.Impl.UnquoteState.exprSubst : Qq.Impl.UnquoteState → Std.HashMap Lean.Expr Lean.Expr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_ofObjects_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {X : C} {i : I} (g : X ⟶ Y i),
  CategoryTheory.Sieve.ofObjects Y X = ⊤
-- Lean.Meta.Basic
Lean.Meta.throwIsDefEqStuck : {α : Type} → Lean.MetaM α
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Variant with `fun x => x` rather than `id`  -/
deriv_id'' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜], (deriv fun x => x) = fun x => 1
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.congr_arg : ∀ {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₂] (f : MultilinearMap R M₁ M₂) {x y : (i : ι) → M₁ i}, x = y → f x = f y
-- Mathlib.CategoryTheory.Category.GaloisConnection
/-- A Galois connection between preorders induces an adjunction between the associated categories.
 -/
GaloisConnection.adjunction : {X : Type u} →
  {Y : Type v} →
    [inst : Preorder X] →
      [inst_1 : Preorder Y] → {l : X → Y} → {u : Y → X} → (gc : GaloisConnection l u) → ⋯.functor ⊣ ⋯.functor
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.Options.recursive : Lean.Lsp.DeleteFile.Options → Bool
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_allM : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs : List α), Lean.Order.monotone f → Lean.Order.monotone fun x => List.allM (f x) xs
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
tsum_mul_tsum_of_nonarchimedean : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R]
  [NonarchimedeanRing R] [T0Space R] {f : α → R} {g : β → R},
  Summable f → Summable g → (∑' (i : α), f i) * ∑' (i : β), g i = ∑' (i : α × β), f i.1 * g i.2
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.SubmonoidPresheaf.map : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (self : F.SubmonoidPresheaf) {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ}
  (i : U ⟶ V), self.obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (self.obj V)
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.instCoeOutHomeomorph : {F : Type u_5} →
  {α : Type u_6} →
    {β : Type u_7} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → [inst_2 : EquivLike F α β] → [HomeomorphClass F α β] → CoeOut F (α ≃ₜ β)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Real.ediam_Icc : ∀ (a b : ℝ), Metric.ediam (Set.Icc a b) = ENNReal.ofReal (b - a)
-- Mathlib.Topology.Order.LeftRightNhds
LinearOrderedAddCommGroup.tendsto_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedAddMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α},
  Filter.Tendsto f x (nhds a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.comp_mulSingle : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι),
  DFunLike.coe ∘ RestrictedProduct.mulSingle A i = Pi.mulSingle i
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_self_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [inst_1 : CommRing L] (i : K →+* L) (p : ℕ) [inst_2 : ExpChar K p]
  [inst_3 : IsPRadical i p] [inst_4 : ExpChar L p] [inst_5 : PerfectRing L p] (x : L), (PerfectRing.lift i i p) x = x
-- Init.Data.UInt.Lemmas
UInt8.toUInt8_toUInt16 : ∀ (n : UInt8), n.toUInt16.toUInt8 = n
-- Mathlib.GroupTheory.Nilpotent
Group.normalizerCondition_of_isNilpotent : ∀ {G : Type u_1} [inst : Group G] [h : Group.IsNilpotent G], NormalizerCondition G
-- Mathlib.Control.Random
/-- Generate a random value of type `α` between `x` and `y` inclusive.  -/
Random.randBound : {m : Type u → Type u_1} →
  {g : Type} →
    (α : Type u) →
      [inst : Preorder α] →
        [BoundedRandom m α] → (lo hi : α) → lo ≤ hi → [RandomGen g] → RandGT g m { a // lo ≤ a ∧ a ≤ hi }
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.mk_add_mk_neg_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ S.addUnits),
  ⟨(AddUnits.coeHom M) x, ⋯⟩ + ⟨(AddUnits.coeHom M) (-x), ⋯⟩ = 0
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁ ++ s == s₂`  -/
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.prefix : Lean.Grind.AC.Seq → Lean.Grind.AC.StartsWithResult✝
-- Init.Data.String.ToSlice
String.ToSlice.toSlice : {α : Type u} → [self : String.ToSlice α] → α → String.Slice
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_bit1 : ∀ {R : Type u_1} [inst : CommSemiring R] {a b c : R} {k : ℕ} {d : R},
  a ^ k = b → b * b = c → c * a = d → a ^ (Nat.mul 2 k).add 1 = d
-- Mathlib.CategoryTheory.Sites.Point.Comap
CategoryTheory.GrothendieckTopology.Point.comap_fiber : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} (Φ : K.Point)
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.RepresentablyFlat F]
  {J : CategoryTheory.GrothendieckTopology C} (hF : CategoryTheory.CoverPreserving J K F)
  [inst_3 : CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements], (Φ.comap F hF).fiber = F.comp Φ.fiber
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.one : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} (j : J),
  MonCat.Colimits.Relation F (MonCat.Colimits.Prequotient.of j 1) MonCat.Colimits.Prequotient.one
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U → (GeneralizingMap f ↔ ∀ (i : ι), GeneralizingMap ((U i).carrier.restrictPreimage f))
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D), (P.map F).IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instConcreteCategoryMulHomCarrier : CategoryTheory.ConcreteCategory Semigrp fun x1 x2 => ↑x1 →ₙ* ↑x2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.ordered_iff_pairwise_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered ↔ List.Pairwise (fun x1 x2 => compare x1 x2 = Ordering.lt) (List.map (fun x => x.fst) t.toListModel)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.cotTermUpperBound : ℕ → ℝ → (B : ℝ) → 0 < B → ℕ → ℝ
-- Mathlib.Data.Nat.Multiplicity
/-- The multiplicity of `p` in `choose n k` is the number of carries when `k` and `n - k`
are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
is any bound greater than `log p n`.  -/
Nat.Prime.emultiplicity_choose : ∀ {p n k b : ℕ},
  Nat.Prime p →
    k ≤ n →
      Nat.log p n < b → emultiplicity p (n.choose k) = ↑{i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card
-- Mathlib.Data.List.Infix
List.IsPrefix.take : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → ∀ (n : ℕ), List.take n l₁ <+: List.take n l₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km fallback : α},
  t.min? = some km → t.getD km fallback = km
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.instMonoidalCategoryLocalizedMonoidal : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.MonoidalCategory (CategoryTheory.LocalizedMonoidal L W ε)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Given an adjunction, assigning to a coalgebra over the right adjoint an algebra over the left
adjoint and going back is isomorphic to the identity functor.  -/
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (adj : F ⊣ G) →
        (CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf adj).comp
            (CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf adj) ≅
          CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Coalgebra G)
-- Mathlib.Order.Circular
btw_refl_right : ∀ {α : Type u_1} [inst : CircularOrder α] (a b : α), btw a b b
-- Mathlib.Algebra.Group.Action.Defs
/-- Type class for actions by semigroups, with notation `g • p`.

The `SemigroupAction G P` typeclass says that the semigroup `G` acts multiplicatively on a type `P`.
More precisely this means that the action satisfies the axiom `(g₁ * g₂) • p = g₁ • (g₂ • p)`.
A mathematician might simply say that the semigroup `G` acts on `P`.

For example, if `G` is a semigroup and `X` is a type, if a mathematician says
say "let `G` act on the set `X`" they will probably mean  `[SemigroupAction G X]`.  -/
SemigroupAction : (α : Type u_9) → Type u_10 → [Semigroup α] → Type (max u_10 u_9)
-- Mathlib.Topology.Algebra.Valued.WithVal
NumberField.RingOfIntegers.instCoeHeadWithVal : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {K : Type u_3} →
      [inst_1 : Field K] → (v : Valuation K Γ₀) → CoeHead (NumberField.RingOfIntegers (WithVal v)) (WithVal v)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ici_eq_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Icc a b ∪ Set.Ici b = Set.Ici a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, ¬cmp k (t.maxKey ⋯) = Ordering.eq → (t.erase k).maxKey he = t.maxKey ⋯
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).cofan₂ =
    CategoryTheory.Limits.Cofan.mk (∐ fun i => B i.i) (CategoryTheory.Limits.Sigma.ι fun i => B i.i)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- Given a natural transformation `τ : F ⟶ G` between functors `C ⥤ D` which preserve
the right homology of a short complex `S`, and a right homology data for `S`,
this is the right homology map data for the morphism `S.mapNatTrans τ`
obtained by evaluating `τ`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              {F G : CategoryTheory.Functor C D} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] →
                    [inst_6 : F.PreservesRightHomologyOf S] →
                      [inst_7 : G.PreservesRightHomologyOf S] →
                        (h : S.RightHomologyData) →
                          (τ : F ⟶ G) →
                            CategoryTheory.ShortComplex.RightHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
Std.ExtDTreeMap.Const.maxEntry : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α (fun x => β) cmp) → t ≠ ∅ → α × β
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α], MeasureTheory.Measure.Regular 0
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.mkOfCovers_X : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x)
  (map_prop : autoParam (∀ (j : J), P (map j)) AlgebraicGeometry.Scheme.Cover.mkOfCovers._auto_1) (a : J),
  (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).X a = obj a
-- Mathlib.Topology.Order.SuccPred
SuccOrder.isOpen_singleton_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {a : α} [SuccOrder α]
  [NoMaxOrder α], IsOpen {a} ↔ ¬Order.IsSuccLimit a
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addZeroClass : {R : Type u} → {M : Type v} → [AddZeroClass R] → [AddZeroClass M] → AddZeroClass (TrivSqZeroExt R M)
-- Mathlib.Algebra.Homology.Opposite
/-- The homotopy between morphisms of homological complexes that is deduced
from a homotopy in the opposite category.  -/
Homotopy.unop : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {ι : Type u_2} →
      {c : ComplexShape ι} →
        [inst_1 : CategoryTheory.Preadditive V] →
          {F G : HomologicalComplex Vᵒᵖ c} →
            {φ₁ φ₂ : F ⟶ G} →
              Homotopy φ₁ φ₂ →
                Homotopy ((HomologicalComplex.unopFunctor V c).map φ₁.op)
                  ((HomologicalComplex.unopFunctor V c).map φ₂.op)
-- Mathlib.Algebra.Free
FreeSemigroup.length.eq_1 : ∀ {α : Type u} (x : FreeSemigroup α), x.length = x.tail.length + 1
-- Batteries.Data.String.Matcher
/-- Returns the first substring of `s` that matches `pattern`,
or `none` if there is no such substring.
 -/
Substring.findSubstr? : Substring.Raw → Substring.Raw → Option Substring.Raw
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.sum_zero : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Finset α}, (∀ x ∈ s, f x ≡ 0 [MOD n]) → ∑ x ∈ s, f x ≡ 0 [MOD n]
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
contMDiff_tangentBundleModelSpaceHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  ContMDiff I.tangent (I.prod (modelWithCornersSelf 𝕜 E)) n ⇑(tangentBundleModelSpaceHomeomorph I)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instNorm : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Norm ℤ_[p]
-- Init.Internal.Order.Basic
Lean.Order.fun_csup : {α : Sort u} →
  {β : α → Sort v} →
    [inst : (x : α) → Lean.Order.CCPO (β x)] → (c : ((x : α) → β x) → Prop) → Lean.Order.chain c → (x : α) → β x