mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- The image of a zero morphism is the zero object.  -/
CategoryTheory.Limits.imageZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] → {X Y : C} → CategoryTheory.Limits.image 0 ≅ 0
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationInlOfIsStableUnderCobaseChangeCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [inst_2 : CategoryTheory.Limits.HasPushout f g]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange] [hg : HomotopicalAlgebra.Cofibration g],
  HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.pushout.inl f g)
-- Lean.Parser.StrInterpolation
Lean.Parser.interpolatedStrNoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.instPartialOrder : {α : Type u_2} → [inst : BooleanAlgebra α] → PartialOrder (BooleanSubalgebra α)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instIsCancelMulZero : IsCancelMulZero Complex.UnitDisc
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_injective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective ⇑DFinsupp.toMultiset
-- Mathlib.Order.Filter.Pointwise
Filter.le_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g h : Filter β},
  h ≤ f +ᵥ g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s +ᵥ t ∈ h
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsLT_neg : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Iio (-a))) (nhdsWithin a (Set.Ioi a))
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : TopologicalSpace.NonemptyCompacts α}, CompactSpace ↥s
-- Mathlib.Topology.Sets.Opens
/-- The open neighborhoods of a point. See also `Opens` or `nhds`.  -/
TopologicalSpace.OpenNhdsOf : {α : Type u_2} → [TopologicalSpace α] → α → Type u_2
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets_comap_eq_comap_image : ∀ {α : Type u_1} {β : Type u_2} (l : Filter β) (f : α → β),
  (Filter.comap f l).smallSets = Filter.comap (Set.image f) l.smallSets
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_eq_one_iff_commute : ∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G}, ⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂
-- Mathlib.Algebra.Ring.AddAut
AddAut.mulRight_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] (u : Rˣ) (x : R), (AddEquiv.symm (AddAut.mulRight u)) x = x * ↑u⁻¹
-- Mathlib.Data.Matrix.Reflection
Matrix.Forall.eq_2 : ∀ {α : Type u_1} (x n : ℕ) (x_1 : Matrix (Fin n.succ) (Fin x) α → Prop),
  Matrix.Forall x_1 = FinVec.Forall fun r => Matrix.Forall fun A => x_1 (Matrix.of (Matrix.vecCons r A))
-- Mathlib.Algebra.Group.Action.Defs
instSMulOfMul.eq_1 : ∀ {α : Type u} [inst : Mul α], instSMulOfMul = { smul := fun x y => Mul.mul x y }
-- Mathlib.RingTheory.ReesAlgebra
mem_reesAlgebra_iff_support : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (f : Polynomial R),
  f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.inv_eq_self : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} {A : Set G}, IsApproximateSubgroup K A → A⁻¹ = A
-- Mathlib.Dynamics.Transitive
MulAction.IsTopologicallyTransitive.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α],
  (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, (m • U ∩ V).Nonempty) →
    MulAction.IsTopologicallyTransitive M α
-- Mathlib.NumberTheory.Ostrowski
/-- Values of an absolute value on the rationals are determined by the values on the natural
numbers.  -/
Rat.AbsoluteValue.eq_on_nat_iff_eq : ∀ {f g : AbsoluteValue ℚ ℝ}, (∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g
-- Init.Data.Vector.MapIdx
Vector.back?_mapIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β},
  (Vector.mapIdx f xs).back? = Option.map (f (n - 1)) xs.back?
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.of_rank_eq_one : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Module.rank K V = 1 → FiniteDimensional K V
-- Init.Data.List.Lemmas
List.getElem_replace_of_ne : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [LawfulBEq α] {l : List α} {i : ℕ} {h : i < l.length},
  l[i] ≠ a → (l.replace a b)[i] = l[i]
-- Lean.Level
Lean.Level.PP.Result.leaf.inj : ∀ {a a_1 : Lean.Name}, Lean.Level.PP.Result.leaf a = Lean.Level.PP.Result.leaf a_1 → a = a_1
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.comp_liftAddHom : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] (g : N →+ P) (f : α → M →+ N),
  g.comp (Finsupp.liftAddHom f) = Finsupp.liftAddHom fun a => g.comp (f a)
-- Init.Data.Vector.Basic
/-- The size of a vector.  -/
Vector.size : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.instLinearEquivClass : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N], LinearEquivClass (M ≃ₗ⁅R,L⁆ N) R M N
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.mk.inj : ∀ {E : Type u_5} {F : Type u_6} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {toFun : E → F} {smooth' : ContDiff ℝ (↑⊤) toFun}
  {decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C} {toFun_1 : E → F}
  {smooth'_1 : ContDiff ℝ (↑⊤) toFun_1}
  {decay'_1 : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun_1 x‖ ≤ C},
  { toFun := toFun, smooth' := smooth', decay' := decay' } =
      { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 } →
    toFun = toFun_1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_isBigO : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : NormedField β] [inst_1 : LinearOrder β]
  [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop → (Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z)