mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {fg : X ⟶ Z},
  CategoryTheory.CategoryStruct.comp f g = fg →
    ∀ [HomotopicalAlgebra.WeakEquivalence g] [hfg : HomotopicalAlgebra.WeakEquivalence fg],
      HomotopicalAlgebra.WeakEquivalence f
-- Lean.Meta.Tactic.Grind.Action
/-- Given `[t₁, ..., tₙ]`, returns
```
(t₁
 ...
 tₙ)
```
If the list is empty, it returns `(skip)`.
 -/
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.mkGrindParen : List Lean.Meta.Grind.TGrind → Lean.CoreM Lean.Meta.Grind.TGrind
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'_right : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ), (Turing.Tape.mk' L R).right = R.tail
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.proj_surjective : ∀ (S : LightProfinite) (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))
-- Mathlib.NumberTheory.ModularForms.Cusps
IsCusp.of_isFiniteRelIndex : ∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ} [𝒢.IsFiniteRelIndex ℋ], IsCusp c ℋ → IsCusp c 𝒢
-- Mathlib.Analysis.Normed.Group.Defs
/-- the `ℝ≥0`-valued norm function.  -/
«term‖_‖₊» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel_not_mono_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f],
  f ≠ 0 → ¬CategoryTheory.Mono (CategoryTheory.Limits.cokernel.π f)
-- Mathlib.Order.Sublattice
/-- The empty sublattice of a lattice.  -/
Sublattice.instBot : {α : Type u_2} → [inst : Lattice α] → Bot (Sublattice α)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_eq : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] {p p' : β → α}
  {q : (b : β) → f (p b) ⟶ g b} {q' : (b : β) → f (p' b) ⟶ g b} (hp : p = p'),
  (∀ (b : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (q b) = q' b) →
    CategoryTheory.Limits.Pi.map' p q = CategoryTheory.Limits.Pi.map' p' q'
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.instFaithfulTopCatCompactlyGeneratedToTop : CompactlyGenerated.compactlyGeneratedToTop.Faithful
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
Measurable.borelSpace_codomain : ∀ {X : Type u_3} {Y : Type u_4} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : TopologicalSpace Y]
  [T0Space Y] [inst_4 : MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {f : X → Y},
  Measurable f → Function.Surjective f → BorelSpace Y
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- A function with finite support has a logarithmic counting function that is big-O of `log`.
 -/
Function.locallyFinsuppWithin.logCounting_isBigO_log_of_finite_support : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {D : Function.locallyFinsupp E ℤ},
  (Function.locallyFinsuppWithin.support D).Finite →
    Function.locallyFinsuppWithin.logCounting D =O[Filter.atTop] Real.log
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup `H` is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` 

[Wikidata Q743179](https://www.wikidata.org/wiki/Q743179) -/
Subgroup.Normal : {G : Type u_1} → [inst : Group G] → Subgroup G → Prop