mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_eq_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t.get? a = t[a]?
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.instAddCommGroup : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → (ρ : Representation k G V) → AddCommGroup ρ.Coinvariants
-- Mathlib.Data.PFun
PFun.fixInduction'_stop : ∀ {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a)
  (fa : Sum.inl b ∈ f a) (hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final)
  (hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀), PFun.fixInduction' h hbase hind = hbase a fa
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.isometric : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : MetricSpace A} {inst_8 : Algebra R A}
  [self : IsometricContinuousFunctionalCalculus R A p] (a : A) (ha : p a), Isometry ⇑(cfcHom ha)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sub_iff_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₂ =O[l] g → ((fun x => f₁ x - f₂ x) =O[l] g ↔ f₁ =O[l] g)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instInt : Lean.Elab.ConfigEval.EvalExpr ℤ
-- Mathlib.Data.Analysis.Filter
/-- `Unit` is a realizer for the principal filter  -/
Filter.Realizer.principal : {α : Type u_1} → (s : Set α) → (Filter.principal s).Realizer
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.rTensorEquivAlgEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} (S : Type u_4) (A : Type u_5) (B : Type u_6) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : CommMonoid M],
  MonoidAlgebra.rTensorEquivAlgEquiv R S A B =
    AlgEquiv.restrictScalars S
      (AlgEquiv.ofAlgHom
        (Algebra.TensorProduct.lift
          ((IsScalarTower.toAlgHom A (TensorProduct R A B) (MonoidAlgebra (TensorProduct R A B) M)).comp
            Algebra.TensorProduct.includeLeft)
          (MonoidAlgebra.mapAlgHom M Algebra.TensorProduct.includeRight) ⋯)
        MonoidAlgebra.rTensorEquivAlgEquiv.invFun ⋯ ⋯)
-- Init.Data.Array.Lemmas
Array.contains_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, xs.contains a = true ↔ a ∈ xs
-- Lean.InternalExceptionId
/-- Register a new internal exception in the system.
Each internal exception has a unique index.
Throw an exception if the given name is not unique.
This method is usually invoked using the `initialize` command.
 -/
Lean.registerInternalExceptionId : Lean.Name → IO Lean.InternalExceptionId
-- Mathlib.Data.Int.ModEq
Int.ModEq.of_div : ∀ {m a b c : ℤ}, a / c ≡ b / c [ZMOD m / c] → c ∣ a → c ∣ b → c ∣ m → a ≡ b [ZMOD m]
-- Init.Data.List.Basic
List.Perm.brecOn : ∀ {α : Type u} {motive : (a a_1 : List α) → a.Perm a_1 → Prop} {a a_1 : List α} (t : a.Perm a_1),
  (∀ (a a_2 : List α) (t : a.Perm a_2), List.Perm.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_mk'_self : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], Subgroup.map (QuotientGroup.mk' N) N = ⊥
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.quotientEquivOrthogonal_symm_eq_mk : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x : E) (hx : x ∈ Kᗮ),
  K.quotientEquivOrthogonal.symm ⟨x, hx⟩ = Submodule.Quotient.mk x
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The functor `pointwiseLeftKanExtension L F` is a pointwise left Kan
extension of `F` along `L`.  -/
CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension F] →
                  (CategoryTheory.Functor.LeftExtension.mk (L.pointwiseLeftKanExtension F)
                      (L.pointwiseLeftKanExtensionUnit F)).IsPointwiseLeftKanExtension
-- Batteries.Data.Char.Basic
Char.exists_eq_false_of_all_eq_false : ∀ {p : Char → Bool}, Char.all p = false → ∃ c, p c = false
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.det : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (t : Matrix.TransvectionStruct n R), t.toMatrix.det = 1
-- Init.Data.Ord.Basic
Ordering.isGT_eq : Ordering.eq.isGT = false
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.functionField_isScalarTower : ∀ (X : AlgebraicGeometry.Scheme) [inst : IrreducibleSpace ↥X] (U : X.Opens) (x : ↥U) [inst_1 : Nonempty ↥↑U],
  IsScalarTower ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.stalk ↑x) ↑X.functionField
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.State.mk.sizeOf_spec : ∀ (newGoals : Array Lean.MVarId) (patterns : List (Lean.TSyntax `rintroPat)),
  sizeOf { newGoals := newGoals, patterns := patterns } = 1 + sizeOf newGoals + sizeOf patterns
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.mk_right_as : ∀ {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.WeaklyEtale f],
  (AlgebraicGeometry.Scheme.ProEt.mk f).right.as = PUnit.unit
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- Reverse a path in `toQuiver A` to a path in `toQuiver Aᵀ`, swapping endpoints.  -/
Matrix.transposePath : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Ring R] → [inst_1 : LinearOrder R] → {A : Matrix n n R} → {i j : n} → Quiver.Path i j → Quiver.Path j i
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair_functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (j : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)).obj
      j =
    F.obj j
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.Hom.hom_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [inst_3 : CategoryTheory.IsCommMonObj N.X]
  (f g : M ⟶ N), (f * g).hom = f.hom * g.hom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.isEmpty = true → t.minKeyD fallback = fallback
-- Std.Data.ExtHashMap.Basic
/-- Removes all mappings of the hash map for which the given function returns `false`.  -/
Std.ExtHashMap.filter : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → (α → β → Bool) → Std.ExtHashMap α β → Std.ExtHashMap α β
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.mk'_eq_coe : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (f : α → β), Quotient.mk' f = ↑f
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- Sakai's definition of a von Neumann algebra as a C⋆ algebra with a Banach space predual.

So that we can unambiguously talk about these "abstract" von Neumann algebras
in parallel with the "concrete" ones (weakly closed \*-subalgebras of B(H)),
we name this definition `WStarAlgebra`.

Note that for now we only assert the mere existence of predual, rather than picking one.
This may later prove problematic, and need to be revisited.
Picking one may cause problems with definitional unification of different instances.
One the other hand, not picking one means that the weak-\* topology
(which depends on a choice of predual) must be defined using the choice,
and we may be unhappy with the resulting opaqueness of the definition.
 -/
WStarAlgebra : (M : Type u) → [CStarAlgebra M] → Prop
-- Mathlib.RingTheory.Lasker
/-- An `R`-module `M` satisfies `IsLasker R M` when any `N : Submodule R M` can be
decomposed into finitely many primary submodules.  -/
IsLasker : (R : Type u_1) → (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.Data.Finsupp.PWO
/-- A version of **Dickson's lemma**: `σ →₀ α` is well-quasi-ordered when `σ` is `Finite` and `α` is
well-quasi-ordered.
This version uses finsupps on a finite type as it is intended for use with `MVPowerSeries`.
 -/
Finsupp.wellQuasiOrderedLE : ∀ {α : Type u_1} {σ : Type u_2} [inst : Zero α] [inst_1 : Preorder α] [WellQuasiOrderedLE α] [Finite σ],
  WellQuasiOrderedLE (σ →₀ α)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.step_eq_monadicStep : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it : Std.Iter α},
  Std.Rxi.Iterator.step it = Std.IterStep.mapIterator Std.IterM.toIter (Std.Rxi.Iterator.Monadic.step it.toIterM)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv_mk' : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} {Q : Type u_8} [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] {h : R ≃ₐ[A] P}
  (H : Submonoid.map h M = T) (x : R) (y : ↥M),
  (IsLocalization.algEquivOfAlgEquiv S Q h H) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (h x) ⟨h ↑y, ⋯⟩
-- Mathlib.GroupTheory.Torsion
/-- A monoid is not a torsion monoid if it has an element of infinite order.  -/
not_isMulTorsion_iff : ∀ (G : Type u_1) [inst : Monoid G], ¬IsMulTorsion G ↔ ∃ g, ¬IsOfFinOrder g
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.instWellPoweredShrinkHoms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u₁} C]
  [CategoryTheory.WellPowered.{w, v, u₁} C], CategoryTheory.WellPowered.{w, w, u₁} (CategoryTheory.ShrinkHoms.{u₁} C)
-- Mathlib.Analysis.BoxIntegral.Basic
/-- The `ε`-`δ` definition of `BoxIntegral.HasIntegral`.  -/
BoxIntegral.hasIntegral_iff : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
  BoxIntegral.HasIntegral I l f vol y ↔
    ∀ ε > 0,
      ∃ r,
        (∀ (c : NNReal), l.RCond (r c)) ∧
          ∀ (c : NNReal) (π : BoxIntegral.TaggedPrepartition I),
            l.MemBaseSet I c (r c) π → π.IsPartition → dist (BoxIntegral.integralSum f vol π) y ≤ ε
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `⊥` is contained in any simple graph having sufficiently many vertices.  -/
SimpleGraph.bot_isContained_iff_card_le : ∀ {α : Type u_4} {β : Type u_5} {B : SimpleGraph β} [inst : Fintype α] [inst_1 : Fintype β],
  ⊥.IsContained B ↔ Fintype.card α ≤ Fintype.card β
-- Mathlib.NumberTheory.Divisors
Nat.left_ne_zero_of_mem_divisorsAntidiagonal : ∀ {n : ℕ} {p : ℕ × ℕ}, p ∈ n.divisorsAntidiagonal → p.1 ≠ 0
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instDecidableEqOrdinal : DecidableEq Std.Time.Weekday.Ordinal
-- Init.Data.AC
Lean.Data.AC.Context.evalList_sort_congr : ∀ {α : Sort u_1} {a b c : List ℕ} (ctx : Lean.Data.AC.Context α),
  Std.Commutative ctx.op →
    Lean.Data.AC.evalList α ctx a = Lean.Data.AC.evalList α ctx b →
      a ≠ [] →
        b ≠ [] →
          Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop a c) =
            Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop b c)
-- Mathlib.Analysis.Normed.Group.InfiniteSum
enorm_tsum_le_tsum_enorm : ∀ {ι : Type u_1} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] {f : ι → ε},
  ‖∑' (i : ι), f i‖ₑ ≤ ∑' (i : ι), ‖f i‖ₑ
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- Get the coequalizer morphism from the typeclass `IsSplitPair`.  -/
CategoryTheory.HasSplitCoequalizer.coequalizerπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.HasSplitCoequalizer f g] →
          Y ⟶ CategoryTheory.HasSplitCoequalizer.coequalizerOfSplit f g
-- Lean.Expr
Lean.Int.mkInstHDiv : Lean.Expr
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.strFn.go : (str : String) → Lean.Parser.ParserContext → str.Pos → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.instAdditiveTriangleTriangleFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ),
  (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).Additive
-- Mathlib.Order.KrullDimension
Order.krullDim_enat : Order.krullDim ℕ∞ = ⊤
-- Mathlib.Algebra.Order.ZeroLEOne
/-- See `zero_lt_one` for a version with the type implicit.  -/
zero_lt_one' : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1], 0 < 1
-- Mathlib.Analysis.Complex.Trigonometric
Real.neg_one_le_cos : ∀ (x : ℝ), -1 ≤ Real.cos x
-- Mathlib.Data.Finset.Attach
Finset.coe_attach : ∀ {α : Type u_1} (s : Finset α), ↑s.attach = Set.univ
-- Mathlib.Tactic.ProxyType
Mathlib.ProxyType.ProxyEquivConfig.mk : Lean.Name →
  Lean.Name →
    (List (Lean.Expr × Lean.Name) → Lean.Elab.TermElabM (Lean.Expr × Lean.Term)) →
      (Array (Lean.Name × Lean.Expr × Lean.Term) →
          Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)) →
        Mathlib.ProxyType.ProxyEquivConfig
-- Init.Data.Order.Lemmas
Std.instIrreflLtOfIsPreorderOfLawfulOrderLT : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α], Std.Irrefl fun x1 x2 => x1 < x2
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
SeminormedRing.toRingSeminorm_apply : ∀ (R : Type u_2) [inst : SeminormedRing R] (x : R), (SeminormedRing.toRingSeminorm R) x = ‖x‖
-- Lean.Parser.Term
Lean.Parser.Term.macroDollarArg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwInfo.mk.inj : ∀ {rootExpr subExpr : Lean.Expr} {rflTarget? : Option Lean.Expr} {pos : Lean.SubExpr.Pos}
  {rwKind : Mathlib.Tactic.ClickSuggestions.RwKind} {rootExpr_1 subExpr_1 : Lean.Expr} {rflTarget?_1 : Option Lean.Expr}
  {pos_1 : Lean.SubExpr.Pos} {rwKind_1 : Mathlib.Tactic.ClickSuggestions.RwKind},
  { rootExpr := rootExpr, subExpr := subExpr, rflTarget? := rflTarget?, pos := pos, rwKind := rwKind } =
      { rootExpr := rootExpr_1, subExpr := subExpr_1, rflTarget? := rflTarget?_1, pos := pos_1, rwKind := rwKind_1 } →
    rootExpr = rootExpr_1 ∧ subExpr = subExpr_1 ∧ rflTarget? = rflTarget?_1 ∧ pos = pos_1 ∧ rwKind = rwKind_1
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSlice.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → ℕ → List α → Sort u_2) (n m : ℕ) (x : α) (xs : List α)
  (h_1 : (x x_1 : ℕ) → motive x x_1 []) (h_2 : (m : ℕ) → (xs : List α) → motive 0 m xs)
  (h_3 : (n m : ℕ) → (x : α) → (xs : List α) → motive n.succ m (x :: xs)),
  (match n.succ, m, x :: xs with
    | x, x_1, [] => h_1 x x_1
    | 0, m, xs => h_2 m xs
    | n.succ, m, x :: xs => h_3 n m x xs) =
    h_3 n m x xs
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.toSubspaceUnit.eq_1 : ∀ {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι),
  l.toSubspaceUnit = { idxFun := fun i => (l.idxFun i).elim (Sum.inr ()) Sum.inl, proper := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.MorphismProperty.kernels.of_isLimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W : CategoryTheory.MorphismProperty C} {X₁ X₂ : C} (f : X₁ ⟶ X₂) (k : CategoryTheory.Limits.KernelFork f)
  (hk : CategoryTheory.Limits.IsLimit k), W f → W.kernels k.pt
-- Mathlib.Data.Sym.Sym2
Sym2.other_spec' : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z), s(a, Sym2.Mem.other' h) = z