mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G},
  groupHomology.mapShortComplexH1 (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (groupHomology.shortComplexH1 A)
-- Batteries.Data.UInt
UInt8.lt_iff_toNat_lt_toNat : ∀ {x y : UInt8}, x < y ↔ x.toNat < y.toNat
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_toEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), e.toEquiv.symm = ↑e.symm
-- Mathlib.Analysis.Complex.Basic
Complex.conjCLE_apply : ∀ (z : ℂ), Complex.conjCLE z = (starRingEnd ℂ) z
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.instMonoι : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H), CategoryTheory.Mono (ModuleCat.image.ι f)
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set,
`deriv` version.  -/
Convex.image_deriv : ∀ {f : ℝ → ℝ} {s : Set ℝ}, Convex ℝ s → (∀ x ∈ s, DifferentiableAt ℝ f x) → Convex ℝ (deriv f '' s)
-- Mathlib.Order.UpperLower.Prod
UpperSet.inf_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s₁ s₂ : UpperSet α) (t : UpperSet β),
  (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality_assoc : ∀ {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₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂] {Z : D}
  (h : F.obj S₂.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapCyclesIso F).hom h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ)) h)
-- Mathlib.Computability.Partrec
Partrec₂.comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [inst : Primcodable α]
  [inst_1 : Primcodable β] [inst_2 : Primcodable γ] [inst_3 : Primcodable δ] [inst_4 : Primcodable σ] {f : γ → δ →. σ}
  {g : α → β → γ} {h : α → β → δ}, Partrec₂ f → Computable₂ g → Computable₂ h → Partrec₂ fun a b => f (g a b) (h a b)
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.builtinCmdCodeActions : IO.Ref Lean.CodeAction.CommandCodeActions
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.Sym.share1 : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.mulAction : {R' : Type u_1} → {α : Type u_2} → [inst : Semiring R'] → [MulAction R' α] → (S : Subsemiring R') → MulAction (↥S) α
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.genWeightSpace_ne_bot : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ : LieModule.Weight R L M), LieModule.genWeightSpace M ⇑χ ≠ ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_iff_hasProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → α},
  (∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) →
    (∀ (v : Finset β), ∃ u, ∀ (u' : Finset γ), u ⊆ u' → ∃ v', v ⊆ v' ∧ ∏ b ∈ v', f b = ∏ x ∈ u', g x) →
      (HasProd f a ↔ HasProd g a)
-- Mathlib.Tactic.Peel
/-- If `unfold` is false then do `whnfR`, otherwise unfold everything that's not a quantifier,
according to the `quantifiers` list.  -/
Mathlib.Tactic.Peel.whnfQuantifier : Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Commute.Hom
SemiconjBy.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst_1 : Mul N] {a x y : M} [inst_2 : FunLike F M N]
  [MulHomClass F M N], SemiconjBy a x y → ∀ (f : F), SemiconjBy (f a) (f x) (f y)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `g ∘ f = id` as `ContinuousLinearMap`s implies `g ∘ f = id` as functions.  -/
ContinuousLinearMap.leftInverse_of_comp : ∀ {R : Type u_9} {E : Type u_10} {F : Type u_11} [inst : Semiring R] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} {g : F →L[R] E},
  g ∘SL f = ContinuousLinearMap.id R E → Function.LeftInverse ⇑g ⇑f
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.append_mk : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l₁ l₂ : List Γ),
  Turing.ListBlank.append l₁ (Turing.ListBlank.mk l₂) = Turing.ListBlank.mk (l₁ ++ l₂)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Extract the forward direction of a multiplicative equivalence
as a multiplication-preserving function.
 -/
MulEquiv.toMonoidHom : {M : Type u_4} → {N : Type u_5} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.comul_comp_inr : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B],
  CoalgebraStruct.comul ∘ₗ LinearMap.inr R A B =
    TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B) ∘ₗ CoalgebraStruct.comul
-- Mathlib.CategoryTheory.Limits.Indization.LocallySmall
CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.LocallySmall.{v, max u v, max u (v + 1)}
    (CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Limits.IsIndObject)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.baseOf.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : AddMonoid M] [inst_1 : LinearOrder S] [inst_2 : AddMonoid S]
  (v : ι → M) (f : M →+ S), IsAddIndecomposable.baseOf v f = {j | IsAddIndecomposable v {i | 0 < f (v i)} j}
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_fun_sub : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f g : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f → μ.Integrable g → ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
-- Init.Core
iff_comm : ∀ {a b : Prop}, (a ↔ b) ↔ (b ↔ a)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.BinaryRefVec w → Std.Sat.AIG.RefVecEntry α w
-- Lean.Data.Name
/-- Checks whether the name is an implementation-detail hypothesis name.

Implementation-detail hypothesis names start with a double underscore.
 -/
Lean.Name.isImplementationDetail : Lean.Name → Bool
-- Mathlib.Data.Fintype.Order
Finite.ciInf_prod : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Finite ι] [Finite ι'] [inst : ConditionallyCompleteLattice α]
  (f : ι × ι' → α), ⨅ a, f a = ⨅ i, ⨅ i', f (i, i')
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.log_pow_int_eq_self : ∀ {x : ℤ}, 1 < x.natAbs → ∀ (m : ℕ), Submonoid.log (Submonoid.pow x m) = m
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Every presheaf is a sheaf for the family `{𝟙 X}`.

[Elephant] C2.1.5(i)
 -/
CategoryTheory.Presieve.isSheafFor_singleton_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_monomial : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : T},
  a ≠ 0 → ∀ (n : ℕ), ((Polynomial.monomial n) a).aroots S = n • {0}
-- Init.Data.Range.Polymorphic.Char
Char.instHasSize_1 : Std.Rxo.HasSize Char
-- Aesop.Tree.Data
Aesop.Rapp.foldSubgoalsM : {m : Type → Type} →
  {σ : Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → σ → (σ → Aesop.GoalRef → m σ) → Aesop.Rapp → m σ
-- Init.Data.UInt.Lemmas
UInt32.sub_zero : ∀ (a : UInt32), a - 0 = a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceEquiv_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceEquiv.inverse = f.iteratedSliceBackward
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_nat_eq_natCast_ascFactorial : ∀ (S : Type u_1) [inst : Semiring S] (n k : ℕ), Polynomial.eval (↑n) (ascPochhammer S k) = ↑(n.ascFactorial k)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X : C}
  (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {Z : D}
  (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0)
      (CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) h) =
    CategoryTheory.CategoryStruct.comp (F.map (P.π.f 0)) h
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The "canonical" value group-with-zero of a ring with a valuative relation.  -/
ValuativeRel.ValueGroupWithZero : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Type u_1
-- Mathlib.LinearAlgebra.Span.Basic
/-- We can regard `coe_iSup_of_chain` as the statement that `(↑) : (Submodule R M) → Set M` is
Scott continuous for the ω-complete partial order induced by the complete lattice structures.  -/
Submodule.coe_scott_continuous : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  OmegaCompletePartialOrder.ωScottContinuous SetLike.coe
-- Lean.Level
Lean.Level.instToString : ToString Lean.Level
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.ofList_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List ((a : α) × β a)},
  Std.DHashMap.Raw.ofList l = ↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.algEquivToLimit_continuous : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K],
  Continuous ⇑(InfiniteGalois.algEquivToLimit k K)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.of_exists_mul_mem : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_6}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (S T : Submonoid R),
  S ≤ T → (∀ (x : ↥T), ∃ m, m * ↑x ∈ S) → ∀ (f : M →ₗ[R] N) [IsLocalizedModule S f], IsLocalizedModule T f
-- Lean.Meta.Tactic.Grind.ForallProp
_private.Lean.Meta.Tactic.Grind.ForallProp.0.Lean.Meta.Grind.isForallOrNot? : Lean.Expr → Option (Lean.Name × Lean.Expr × Lean.Expr)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonAssocCommSemiringQuotient : {R : Type u_1} → [inst : NonAssocCommSemiring R] → (c : RingCon R) → NonAssocCommSemiring c.Quotient
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.equiv_eq_conj : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (a : ↥A),
  HNNExtension.of ↑(φ a) = HNNExtension.t * HNNExtension.of ↑a * HNNExtension.t⁻¹
-- Std.Async.ContextAsync
/-- Returns the current context for inspection or to pass to other functions.
 -/
Std.Async.ContextAsync.getContext : Std.Async.ContextAsync Std.CancellationContext
-- Mathlib.Algebra.Order.Hom.Monoid
/-- The inverse of an order isomorphism is an order isomorphism.  -/
OrderAddMonoidIso.symm : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Add α] → [inst_3 : Add β] → (α ≃+o β) → β ≃+o α
-- Mathlib.Algebra.Group.Submonoid.Finsupp
AddSubmonoid.mem_closure_iff_of_fintype : ∀ {M : Type u_1} [inst : AddCommMonoid M] {x : M} {s : Set M} [inst_1 : Fintype ↑s],
  x ∈ AddSubmonoid.closure s ↔ ∃ a, x = ∑ i, a i • ↑i
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.instContinuousMapClass : ∀ {F : Type u_5} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : EquivLike F α β] [HomeomorphClass F α β], ContinuousMapClass F α β
-- Mathlib.Data.Sym.Sym2
Set.mk_mem_sym2_iff : ∀ {α : Type u_1} {s : Set α} {x y : α}, s(x, y) ∈ s.sym2 ↔ x ∈ s ∧ y ∈ s
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- `x` is the only fixed point of `pointReflection x`. This lemma requires
`x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument.  -/
AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {x y : P₁},
  (Function.Injective fun x => 2 • x) → ((AffineEquiv.pointReflection k x) y = y ↔ y = x)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Multiset.finsetSum_eq_sup_iff_disjoint : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] {i : Finset β} {f : β → Multiset α},
  i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
-- Mathlib.RingTheory.WittVector.Domain
WittVector.instIsDomain : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] [IsDomain R],
  IsDomain (WittVector p R)
-- Mathlib.Tactic.Linarith.Frontend
/-- Retrieves the list of values at a key, as well as the index of the key for later modification.
(If the key is not in the map it returns `self.size` as the index.)  -/
Mathlib.Tactic.Linarith.ExprMultiMap.find : {α : Type} → Mathlib.Tactic.Linarith.ExprMultiMap α → Lean.Expr → Lean.MetaM (ℕ × List α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instDecidableEqBVUnOp : DecidableEq Std.Tactic.BVDecide.BVUnOp
-- Mathlib.RingTheory.Etale.Locus
Algebra.IsEtaleAt.comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] (p : Ideal A) (P : Ideal B)
  [P.LiesOver p] [inst_8 : p.IsPrime] [inst_9 : P.IsPrime] [Algebra.IsEtaleAt R p] [Algebra.IsEtaleAt A P],
  Algebra.IsEtaleAt R P
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitUncurryIsoColimitCompColim.eq_1 : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)],
  CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F =
    (CategoryTheory.Limits.coconeOfCoconeUncurryIsColimit (fun j => CategoryTheory.Limits.colimit.isColimit (F.obj j))
          (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Functor.uncurry.obj F))).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimit.isColimit (F.comp CategoryTheory.Limits.colim))
-- Mathlib.Algebra.FreeMonoid.Basic
_private.Mathlib.Algebra.FreeMonoid.Basic.0.FreeAddMonoid.sumAux.match_1.eq_2 : ∀ {M : Type u_1} (motive : List M → Sort u_2) (x : M) (xs : List M) (h_1 : Unit → motive [])
  (h_2 : (x : M) → (xs : List M) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Mathlib.Order.Category.BddDistLat
BddDistLat.inv_hom_apply : ∀ {X Y : BddDistLat} (e : X ≅ Y) (x : ↑X.toDistLat),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).right = X.right.right
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
finrank_span_singleton : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {v : V},
  v ≠ 0 → Module.finrank K ↥(K ∙ v) = 1
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_duple : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {N : Type u_10}
  [inst_2 : IsStrictOrderedRing R] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : M) (f : M → N),
  Convexity.StdSimplex.map f (Convexity.StdSimplex.duple x y hs ht h) = Convexity.StdSimplex.duple (f x) (f y) hs ht h
-- Mathlib.Order.RelClasses
right_iff_left_not_left : ∀ {α : Type u} {r s : α → α → Prop} [IsNonstrictStrictOrder α r s] {a b : α}, s a b ↔ r a b ∧ ¬r b a
-- Mathlib.Data.Set.Sups
Set.Nonempty.of_sups_left : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α}, (s ⊻ t).Nonempty → s.Nonempty
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.nodup_toList : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] {a : α}, (*...a).toList.Nodup
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_congr₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {f g : β → γ → α} {M : SummationFilter γ},
  (∀ (b : β) (c : γ), f b c = g b c) → ∏'[L] (b : β), ∏'[M] (c : γ), f b c = ∏'[L] (b : β), ∏'[M] (c : γ), g b c
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to an `Int`, sending `NaN` to `0` and positive and negative
infinity to the given values.
 -/
Float.Model.UnpackedFloat.toInt : ℤ → ℤ → Float.Model.UnpackedFloat → ℤ
-- Mathlib.Computability.RegularExpressions
/-- The language of the map is the map of the language.  -/
RegularExpression.matches'_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (P : RegularExpression α),
  (RegularExpression.map f P).matches' = (Language.map f) P.matches'
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_anti : ∀ {α : Type u_1} {G G' : SimpleGraph α}, G ≤ G' → G'.ediam ≤ G.ediam
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpaceProduct_def : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H],
  LieAlgebra.rootSpaceProduct R L H = LieAlgebra.rootSpaceWeightSpaceProduct R L H L
-- Mathlib.Data.EReal.Operations
EReal.toENNReal_add : ∀ {x y : EReal}, 0 ≤ x → 0 ≤ y → (x + y).toENNReal = x.toENNReal + y.toENNReal
-- Mathlib.Topology.Order.LeftRightLim
/-- Let `f : α → β` be a function from a linear order `α` to a topological space `β`, and
let `a : α`. The limit strictly to the right of `f` at `a`, denoted with `rightLim f a`, is defined
by using the order topology on `α`. If `a` is isolated to its right or the function has no right
limit, we use `f a` instead to guarantee a good behavior in most cases.  -/
Function.rightLim : {α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [TopologicalSpace β] → (α → β) → α → β
-- Mathlib.Data.Rat.Lemmas
Rat.pnatDen_zero : Rat.pnatDen 0 = 1
-- Std.Time.Format.Modifier
Std.Time.instReprZoneId.repr : Std.Time.ZoneId → ℕ → Std.Format
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- `SMulMemClass S R M` says `S` is a type of subsets `s ≤ M` that are closed under the
scalar action of `R` on `M`.

Note that only `R` is marked as an `outParam` here, since `M` is supplied by the `SetLike`
class instead.
 -/
SMulMemClass : (S : Type u_1) → (R : outParam (Type u_2)) → (M : Type u_3) → [SMul R M] → [SetLike S M] → Prop
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.max : {α : Type u} →
  (self : Std.Packages.LinearOrderOfLEArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    Max α
-- Init.Data.String.Extra
/-- Replaces each `\r\n` with `\n` to normalize line endings, but does not validate that there are no
isolated `\r` characters.

This is an optimized version of `String.replace text "\r\n" "\n"`.
 -/
String.crlfToLf : String → String
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_eq_of_lt : ∀ {a b : Ordinal.{u_4}}, a < b → a % b = a
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.mk_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b),
  (CategoryTheory.Limits.WidePullbackCone.mk b π h).pt = W
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.single.injEq : ∀ {ι : Type v} (a a_1 : ι), (CategoryTheory.Pairwise.single a = CategoryTheory.Pairwise.single a_1) = (a = a_1)
-- Mathlib.Topology.Separation.Hausdorff
/-- In a `R1Space X`, for disjoint closed sets `s t` such that `closure sᶜ` is compact,
there are neighbourhoods that separate `s` and `t`.  -/
SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {s t : Set X},
  IsClosed s → IsCompact (closure sᶜ) → IsClosed t → Disjoint s t → SeparatedNhds s t
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.expr : Lean.Meta.GeneralizeArg → Lean.Expr
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Option.orElse.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → (Unit → Option α) → Sort u_2) (b : Unit → Option α)
  (h_1 : (a : α) → (x : Unit → Option α) → motive (some a) x) (h_2 : (b : Unit → Option α) → motive none b),
  (match none, b with
    | some a, x => h_1 a x
    | none, b => h_2 b) =
    h_2 b
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.counit_comp_lsingle : ∀ (R : Type u) (ι : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (i : ι), CoalgebraStruct.counit ∘ₗ Finsupp.lsingle i = CoalgebraStruct.counit
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.finrank_add_finrank_dualAnnihilator_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (W : Subspace K V), Module.finrank K ↥W + Module.finrank K ↥(Submodule.dualAnnihilator W) = Module.finrank K V