mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.coe_toLinearEquiv : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (e : M ≃+ M₂)
  (h : ∀ (c : R) (x : M), e (c • x) = c • e x), ⇑(e.toLinearEquiv h) = ⇑e
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mkIso'_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.IsCommMonObj M] [inst_5 : CategoryTheory.MonObj N] [inst_6 : CategoryTheory.IsCommMonObj N]
  [inst_7 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.CommMon.mkIso' e).hom.hom.hom = e.hom
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.cast.sizeOf_spec : sizeOf Lean.Meta.CongrArgKind.cast = 1
-- Init.Data.String.Lemmas.FindPos
String.Pos.le_prev_iff_lt : ∀ {s : String} {p q : s.Pos} {h : q ≠ s.startPos}, p ≤ q.prev h ↔ p < q
-- Mathlib.Topology.Instances.ENNReal.ENatENNReal
ENat.isClosedEmbedding_toENNReal : Topology.IsClosedEmbedding ENat.toENNReal
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.restrictIndexHom_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {ι : Type w'}
  (f : ι → E.I₀) (a : ι), (E.restrictIndexHom f).s₀ a = f a
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.eq_3 : ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize✝ ByteArray.utf8DecodeChar?.FirstByte.oneMore = 2
-- Std.Sat.AIG.Basic
Std.Sat.AIG.mk.injEq : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size)
  (hconst : decls[0] = Std.Sat.AIG.Decl.false) (decls_1 : Array (Std.Sat.AIG.Decl α))
  (cache_1 : Std.Sat.AIG.Cache α decls_1) (hdag_1 : Std.Sat.AIG.IsDAG α decls_1) (hzero_1 : 0 < decls_1.size)
  (hconst_1 : decls_1[0] = Std.Sat.AIG.Decl.false),
  ({ decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst } =
      { decls := decls_1, cache := cache_1, hdag := hdag_1, hzero := hzero_1, hconst := hconst_1 }) =
    (decls = decls_1 ∧ cache ≍ cache_1)
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_zero : ∀ {α : Type u_1} {n : Type u_3} [inst : Zero α], Matrix.IsSymm 0
-- Init.Data.SInt.Lemmas
Int8.toInt_toInt32 : ∀ (x : Int8), x.toInt32.toInt = x.toInt
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_disjoint_union : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s t : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasurableSet s →
    MeasurableSet t →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ →
          Disjoint s t →
            ∀ (x : G),
              MeasureTheory.condExpIndL1 hm μ (s ∪ t) x =
                MeasureTheory.condExpIndL1 hm μ s x + MeasureTheory.condExpIndL1 hm μ t x
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.continuous_toLoop : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N),
  Continuous (GenLoop.toLoop i)
-- Init.Control.Lawful.Basic
/-- Mapping a function over the result of `pure` is equivalent to applying the function under `pure`.

This means that `pure` really is pure with respect to `Functor.map`.
 -/
LawfulApplicative.map_pure : ∀ {f : Type u → Type v} {inst : Applicative f} [self : LawfulApplicative f] {α β : Type u} (g : α → β) (x : α),
  g <$> pure x = pure (g x)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod_eq_top_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {s : AddSubmonoid M}
  {t : AddSubmonoid N}, s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFVarAliasInfo.inj : ∀ {i i_1 : Lean.Elab.FVarAliasInfo}, Lean.Elab.Info.ofFVarAliasInfo i = Lean.Elab.Info.ofFVarAliasInfo i_1 → i = i_1
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_apply_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ) → (MeasureTheory.Measure.comap f μ) s ≤ μ (f '' s)
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppTactic : Lean.TSyntax `tactic → Lean.CoreM Std.Format
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The counit is defined as follows: given a locally constant map `f : S → Y(*)`, let
`S = S₁ ⊔ ⋯ ⊔ Sₙ` be the corresponding decomposition of `S` into the fibers. We need to provide an
element of `Y(S)`. It suffices to provide an element of `Y(Sᵢ)` for all `i`. Let `yᵢ ∈ Y(*)` denote
the value of `f` on `Sᵢ`. Our desired element is the image of `yᵢ` under the canonical map
`Y(*) → Y(Sᵢ)`.
 -/
CompHausLike.LocallyConstant.counitAppApp : {P : TopCat → Prop} →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
      (S : CompHausLike P) →
        (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) →
          [CategoryTheory.Limits.PreservesFiniteProducts Y] →
            [CompHausLike.HasExplicitFiniteCoproducts P] →
              LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y.obj (Opposite.op S)
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_add : ∀ {w : ℕ} (x : BitVec w) (n m : ℕ), x <<< (n + m) = x <<< n <<< m
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_eq_one_of_subsingleton : ∀ {α : Type u_1} {f : α → α} {x : α} [Subsingleton α], Function.minimalPeriod f x = 1
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_mk : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃ N) (hf : ∀ (x y : M), f (x * y) = f x * f y),
  ⇑{ toEquiv := f, map_mul' := hf } = ⇑f
-- Init.Data.List.Lemmas
List.forall_mem_singleton : ∀ {α : Type u_1} {p : α → Prop} {a : α}, (∀ x ∈ [a], p x) ↔ p a
-- Mathlib.NumberTheory.WellApproximable
/-- In a seminormed additive group `A`, given a sequence of
distances `δ₁, δ₂, ...`, `addWellApproximable A δ` is the limsup as `n → ∞` of the sets
`approxAddOrderOf A n δₙ`. Thus, it is the set of points that lie in infinitely many of the sets
`approxAddOrderOf A n δₙ`.  -/
addWellApproximable : (A : Type u_1) → [SeminormedAddGroup A] → (ℕ → ℝ) → Set A
-- Mathlib.Data.Finset.Sum
/-- Disjoint sum of finsets.  -/
Finset.disjSum : {α : Type u_1} → {β : Type u_2} → Finset α → Finset β → Finset (α ⊕ β)
-- Init.Data.UInt.Lemmas
mod_usizeSize_uInt16Size : ∀ (n : ℕ), n % USize.size % UInt16.size = n % UInt16.size
-- Mathlib.Data.Matrix.Basis
Matrix.induction_on' : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : AddCommMonoid α] [Finite m] [Finite n] {P : Matrix m n α → Prop} (M : Matrix m n α),
  P 0 → (∀ (p q : Matrix m n α), P p → P q → P (p + q)) → (∀ (i : m) (j : n) (x : α), P (Matrix.single i j x)) → P M
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_range : ∀ {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : Std.Legacy.Range}
  {init : β} {f : (a : ℕ) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List ℕ) (cur : ℕ) (suff : List ℕ) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.GroupTheory.Perm.Basic
Set.BijOn.perm_inv : ∀ {α : Type u_1} {f : Equiv.Perm α} {s : Set α}, Set.BijOn (⇑f) s s → Set.BijOn (⇑f⁻¹) s s
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_neg_iff : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f : α → E}, MeasureTheory.IntegrableOn (-f) s μ ↔ MeasureTheory.IntegrableOn f s μ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_lt_iff_lt_add`. -/
sub_right_lt_of_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a < b + c → a - c < b
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The rank of a finite product of free modules is the sum of the ranks.  -/
rank_pi : ∀ {R : Type u} {η : Type u₁'} {φ : η → Type u_1} [inst : Semiring R] [StrongRankCondition R]
  [inst_2 : (i : η) → AddCommMonoid (φ i)] [inst_3 : (i : η) → Module R (φ i)] [∀ (i : η), Module.Free R (φ i)]
  [Finite η], Module.rank R ((i : η) → φ i) = Cardinal.sum fun i => Module.rank R (φ i)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_spanning_iff : ∀ {α : Type u_2} {M : Matroid α} {S : Set α},
  autoParam (S ⊆ M.E) Matroid.closure_spanning_iff._auto_1 → (M.Spanning (M.closure S) ↔ M.Spanning S)
-- Mathlib.Order.Closure
/-- A lower adjoint of `u` on the preorder `α` is a function `l` such that `l` and `u` form a Galois
connection. It allows us to define closure operators whose output does not match the input. In
practice, `u` is often `(↑) : β → α`.  -/
LowerAdjoint : {α : Type u_1} → {β : Type u_4} → [Preorder α] → [Preorder β] → (β → α) → Type (max u_1 u_4)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.map_comp_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] {M'' : Type u_6} {N'' : Type u_7} [inst_4 : AddZeroClass M'']
  [inst_5 : AddZeroClass N''] (f' : M' →+ M'') (g' : N' →+ N'') (f : M →+ M') (g : N →+ N'),
  (AddMonoid.Coprod.map f' g').comp (AddMonoid.Coprod.map f g) = AddMonoid.Coprod.map (f'.comp f) (g'.comp g)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
AlgHom.norm_apply_le_self : ∀ {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [CompleteSpace A] [NormOneClass A] [inst_5 : FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F)
  (a : A), ‖f a‖ ≤ ‖a‖
-- Mathlib.Order.CompleteLattice.Basic
iInf_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β × γ → α}, ⨅ x, f x = ⨅ i, ⨅ j, f (i, j)
-- Mathlib.Data.Nat.PSub
Nat.psub_zero : ∀ {m : ℕ}, m.psub 0 = some m
-- Mathlib.Tactic.Translate.Core
/-- `(dont_translate := ...)` takes a list of type variables (separated by spaces) that should not be
considered for translation. For example in
```
lemma foo {α β : Type} [Group α] [Group β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1
```
we can choose to only translate `α` by writing `to_additive (dont_translate := β)`.
 -/
Mathlib.Tactic.Translate.dontTranslateOption : Lean.ParserDescr
-- Init.Data.Array.Range
Array.mk_add_mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {k i : ℕ} {x : α} {xs : Array α}, (x, k + i) ∈ xs.zipIdx k ↔ xs[i]? = some x
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_map : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} [inst_1 : CommSemiring S]
  (f : R →+* S) (p : MvPowerSeries σ R),
  (MvPowerSeries.truncFinset S s) ((MvPowerSeries.map f) p) = (MvPolynomial.map f) ((MvPowerSeries.truncFinset R s) p)
-- Mathlib.Combinatorics.Quiver.Path
/-- Bounded paths of length zero between two vertices have decidable equality.  -/
Quiver.Path.decidableEqBddPathsZero : {V : Type u_1} → [inst : Quiver V] → (v w : V) → DecidableEq (Quiver.Path.BoundedPaths v w 0)
-- Mathlib.Data.Nat.Basic
Nat.instNontrivial : Nontrivial ℕ
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.natCast : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] (d : ℕ), (↑d).PosSemidef
-- Mathlib.GroupTheory.Perm.List
List.formPerm_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α), [x].formPerm = 1
-- Mathlib.Data.Finsupp.Weight
Finsupp.finite_of_degree_le : ∀ {σ : Type u_1} [Finite σ] (n : ℕ), {f | Finsupp.degree f ≤ n}.Finite
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.go.match_1.splitter : (motive : List String.Slice → Sort u_1) →
  (x : List String.Slice) →
    ((a : String.Slice) → (as : List String.Slice) → motive (a :: as)) → (Unit → motive []) → motive x
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_single_same : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
  nndist (PiLp.single p i b₁) (PiLp.single p i b₂) = nndist b₁ b₂
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  (f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)) (i : I) (j : J) (hij : p (i, j) = k) {Z : C₃}
  (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorMapObjDesc f) h) =
    CategoryTheory.CategoryStruct.comp (f i j hij) h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_int_mul_pi_sub : ∀ (x : ℝ) (n : ℤ), Real.tan (↑n * Real.pi - x) = -Real.tan x
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ : E → E} {s : Set E} {x : E},
  DifferentiableWithinAt 𝕜 V s x →
    DifferentiableWithinAt 𝕜 V₁ s x →
      UniqueDiffWithinAt 𝕜 s x →
        VectorField.lieBracketWithin 𝕜 (V + V₁) W s x =
          VectorField.lieBracketWithin 𝕜 V W s x + VectorField.lieBracketWithin 𝕜 V₁ W s x
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bindOnSupport_eq_zero_iff : ∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (b : β),
  (p.bindOnSupport f) b = 0 ↔ ∀ (a : α) (ha : p a ≠ 0), (f a ha) b = 0
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Every isometry equivalence is a dilation equivalence of ratio `1`.  -/
IsometryEquiv.toDilationEquiv : {X : Type u_1} → {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → X ≃ᵢ Y → X ≃ᵈ Y
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInfo.numNested : Lean.Elab.Structural.IndGroupInfo → ℕ
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.uniformSpace_eq_iInf_precomp_of_cover : ∀ {α : Type u_1} (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] {δ : ι → Type u_6} (φ : (i : ι) → δ i → α),
  (∃ I, I.Finite ∧ ⋃ i ∈ I, Set.range (φ i) = Set.univ) →
    UniformFun.uniformSpace α β =
      ⨅ i,
        UniformSpace.comap (⇑UniformFun.ofFun ∘ (fun x => x ∘ φ i) ∘ ⇑UniformFun.toFun)
          (UniformFun.uniformSpace (δ i) β)
-- Mathlib.Logic.Equiv.Defs
Equiv.ofBijective.congr_simp : ∀ {α : Sort u} {β : Sort v} (f f_1 : α → β) (e_f : f = f_1) (hf : Function.Bijective f),
  Equiv.ofBijective f hf = Equiv.ofBijective f_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsStrictlyGEObjIntSingleFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (A : C) (n : ℤ),
  ((CochainComplex.singleFunctor C n).obj A).IsStrictlyGE n
-- Std.Sync.Channel
/-- The central state structure for a bounded channel. Maintains the following invariants:
1. `0 < capacity`
2. `0 < bufCount → consumers = ∅`
3. `bufCount < capacity → producers = ∅`
4. `producers = ∅ ∨ consumers = ∅`, implied by 1, 2 and 3.
5. `bufCount` corresponds to the amount of slots in `buf` that are `some`.
6. `sendIdx = (recvIdx + bufCount) % capacity`. However all four of these values still get tracked
   as there is potential to make a non-blocking send lock-free in the future with this approach.
7. `closed = true → consumers = ∅`

While it (currently) lacks the partial lock-freeness of go channels, the protocol is based on
[Go channels on steroids](https://docs.google.com/document/d/1yIAYmbvL3JxOKOjuCyon7JhW4cSv1wy5hC0ApeGMV9s/pub)
as well as its [implementation](https://go.dev/src/runtime/chan.go).
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State : Type → Type
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfLocalizations_id : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N), f.ofMulEquivOfLocalizations (MulEquiv.refl N) = f
-- Init.Data.Array.Lex.Lemmas
Array.lt_of_le_of_lt : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {xs ys zs : Array α},
  xs ≤ ys → ys < zs → xs < zs
-- Mathlib.Analysis.Analytic.Order
/-- At a zero with nonvanishing derivative, the analytic order is 1.
This is a variant of `analyticOrderAt_sub_eq_one_of_deriv_ne_zero` with `f z₀ = 0`
replacing the subtraction.  -/
AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, AnalyticAt 𝕜 f x → f x = 0 → deriv f x ≠ 0 → analyticOrderAt f x = 1
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {c d : C} (f : c ⟶ d) (γ : c ⟶ c),
  (CategoryTheory.Groupoid.vertexGroupIsomOfMap f) γ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) (CategoryTheory.CategoryStruct.comp γ f)
-- Mathlib.Algebra.Group.Basic
sub_eq_iff_eq_add' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a - b = c ↔ a = b + c
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around `x`.  -/
WithSeminorms.mem_nhds_iff : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p → ∀ (x : E) (U : Set E), U ∈ nhds x ↔ ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.oppositeShiftFunctorAdd'_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b c : A) (h : a + b = c),
  (CategoryTheory.shiftFunctorAdd' (CategoryTheory.OppositeShift C A) a b c h).inv.app X =
    ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app (Opposite.unop X)).op
-- Mathlib.GroupTheory.Perm.DomMulAct
DomMulAct.mem_stabilizer_iff : ∀ {α : Type u_1} {ι : Type u_2} {f : α → ι} {g : (Equiv.Perm α)ᵈᵐᵃ},
  g ∈ MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f ↔ f ∘ ⇑(DomMulAct.mk.symm g) = f
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry preserves non-negative distances.  -/
Isometry.nndist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x y : α), nndist (f x) (f y) = nndist x y
-- Mathlib.NumberTheory.Chebyshev
/-- `lcmUpto n` is divisible by `choose n k` for all `k ≤ n`  -/
Chebyshev.choose_dvd_lcmUpto : ∀ {n k : ℕ}, k ≤ n → n.choose k ∣ n.lcmUpto
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.comp_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃)
  (f : NormedAddGroupHom V₁ V₂) (a : V₁), (g.comp f) a = g (f a)
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermApplyNewGoals : Lean.Elab.ConfigEval.EvalTerm Lean.Meta.ApplyNewGoals
-- Init.Data.Bool
Bool.lt_iff_le_not_le : ∀ {x y : Bool}, x < y ↔ x ≤ y ∧ ¬y ≤ x
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.List.headI.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (tail : List α) → motive (a :: tail)),
  (match [] with
    | [] => h_1 ()
    | a :: tail => h_2 a tail) =
    h_1 ()
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.pow_one : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α), a ^ 1 = a
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.isNonloop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e → M.IsNonloop e
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.preservesTerminalIso_algSpec_inv_left : ∀ {R : CommRingCat},
  CategoryTheory.Over.Hom.left
      (CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (AlgebraicGeometry.algSpec R)).inv =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centerCongr_symm_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : Type u_1} [inst_1 : NonUnitalNonAssocRing S] (e : R ≃+* S)
  (s : ↥(Subsemigroup.center S)), ↑((NonUnitalSubring.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology], S.HasLeftHomology
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_invOf : ∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Semiring R] [inst_2 : Module Rᵐᵒᵖ M] [inst_3 : Module R M]
  (x : TrivSqZeroExt R M) [inst_4 : Invertible x] [inst_5 : Invertible x.fst], (⅟x).fst = ⅟x.fst
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ι_t_ι_eq_ι_l_b_ι_assoc : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.t i d)
        (CategoryTheory.CategoryStruct.comp ((SSet.skeletonOfMono i) d).ι h)) =
    CategoryTheory.CategoryStruct.comp (SSet.boundary d).ι
      (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex
        (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.b i d)
          (CategoryTheory.CategoryStruct.comp ((SSet.skeletonOfMono i) (d + 1)).ι h)))
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoid.Coprod.swap M N).comp AddMonoid.Coprod.inl = AddMonoid.Coprod.inr
-- Init.Data.Nat.Basic
Nat.not_lt : ∀ {a b : ℕ}, ¬a < b ↔ b ≤ a