mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearEquiv_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (v : V),
  φ.toContinuousLinearEquiv v = ↑φ v
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.id.eq_1 : ∀ (A : Type u_2) [inst : Monoid A] [inst_1 : TopologicalSpace A],
  ContinuousMonoidHom.id A = { toMonoidHom := MonoidHom.id A, continuous_toFun := ⋯ }
-- Mathlib.Data.Fin.Fin2
Fin2.fz.sizeOf_spec : ∀ {n : ℕ}, sizeOf Fin2.fz = 1 + sizeOf n
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Every object's comonoid structure is commutative.  -/
CategoryTheory.CopyDiscardCategory.isCommComonObj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.CopyDiscardCategory C] (X : C), CategoryTheory.IsCommComonObj X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The braiding isomorphism is symmetric.  -/
CategoryTheory.Limits.biprod.symmetry : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding P Q).hom
      (CategoryTheory.Limits.biprod.braiding Q P).hom =
    CategoryTheory.CategoryStruct.id (P ⊞ Q)