mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The canonical isomorphism `(X ×[Z] Y) ×[Y] W ≅ X ×[Z] W`  -/
CategoryTheory.Limits.pullbackLeftPullbackSndIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (g' : W ⟶ Y) →
            [inst_1 : CategoryTheory.Limits.HasPullback f g] →
              [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] →
                CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd f g) g' ≅
                  CategoryTheory.Limits.pullback f (CategoryTheory.CategoryStruct.comp g' g)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.cofree_obj_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C),
  (G.cofree.obj X).A = G.obj X
-- Mathlib.Algebra.Category.ModuleCat.LeftResolution
ModuleCat.instProjectiveObjFree : ∀ (R : Type u) [inst : Ring R] (X : Type u), CategoryTheory.Projective ((ModuleCat.free R).obj X)
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
HasCardinalLT.of_injective : ∀ {X : Type u} {κ : Cardinal.{v}},
  HasCardinalLT X κ → ∀ {Y : Type u'} (f : Y → X), Function.Injective f → HasCardinalLT Y κ
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsNonneg.nonneg : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsNonneg → ∀ (x : M), 0 ≤ (B x) x
-- Mathlib.Data.Set.Function
/-- If `f : α → β` and `g : β → γ` and if `f` is injective on `s`, then `f ∘ g` is a bijection
on `s` iff  `g` is a bijection on `f '' s`.  -/
Set.bijOn_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {p : Set γ} {f : α → β} {g : β → γ},
  Set.InjOn f s → (Set.BijOn (g ∘ f) s p ↔ Set.BijOn g (f '' s) p)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.sum_eq_zero_iff_of_nonpos : ∀ {ι : Type u_9} {M : Type u_10} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M] [AddLeftMono M]
  {f : ι → M}, f ≤ 0 → (∑ i, f i = 0 ↔ f = 0)
-- Mathlib.Order.Monotone.Monovary
Antivary.dual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Antivary f g → Monovary (⇑OrderDual.toDual ∘ f) g
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substAlgHom_comp_substAlgHom_apply : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] {υ : Type u_5} {T : Type u_6}
  [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {a : PowerSeries S}
  {b : MvPowerSeries υ T} [IsScalarTower R S T] (ha : PowerSeries.HasSubst a) (hb : PowerSeries.HasSubst b)
  (f : PowerSeries R), (PowerSeries.substAlgHom hb) ((PowerSeries.substAlgHom ha) f) = (PowerSeries.substAlgHom ⋯) f