mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonAddHom.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α], Finset.singletonAddHom = { toFun := singleton, map_add' := ⋯ }
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_mono : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Monotone (Set.kernImage f)
-- Mathlib.Algebra.Order.Ring.Pow
/-- **Bernoulli's inequality**. This version works for semirings but requires
additional hypotheses `0 ≤ a ^ 2` and `0 ≤ (1 + a) ^ 2`.  -/
one_add_mul_le_pow_of_sq_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a : R},
  0 ≤ a ^ 2 → 0 ≤ (1 + a) ^ 2 → 0 ≤ 2 + a → ∀ (n : ℕ), 1 + ↑n * a ≤ (1 + a) ^ n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  Std.DHashMap.Const.get! (m₁.union m₂) k = Std.DHashMap.Const.getD m₂ k (Std.DHashMap.Const.get! m₁ k)
-- Mathlib.Topology.DerivedSet
relDerivedSet_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Set X}, relDerivedSet A ⊆ A
-- Mathlib.Algebra.Module.ULift
ULift.mulDistribMulAction : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] → [inst_1 : Monoid M] → [MulDistribMulAction R M] → MulDistribMulAction (ULift.{u_1, u} R) M
-- Mathlib.Order.BoundedOrder.Basic
bot_eq_false : ⊥ = false
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {obj : C}
  {property : P obj} {obj_1 : C} {property_1 : P obj_1},
  { obj := obj, property := property } = { obj := obj_1, property := property_1 } → obj = obj_1
-- Mathlib.Order.GaloisConnection.Basic
/-- **Alias** of `GaloisInsertion.l_biInf_of_u_l_eq_self`. -/
GaloisInsertion.l_biInf_of_ul_eq_self : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → α),
  (∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi) → l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)
-- Mathlib.Topology.Order.LeftRight
nhdsGT_sup_nhdsLT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Ioi a) ⊔ nhdsWithin a (Set.Iio a) = nhdsWithin a {a}ᶜ
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_flattenList : ∀ {w : ℕ} (vs : List (BitVec w)) (i : ℕ),
  (BitVec.flattenList vs).getLsbD i =
    (decide (i < w * vs.length) && (vs[vs.length - 1 - i / w]?.getD 0#w).getLsbD (i % w))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} [inst_2 : Inhabited β] {f : Option β → Option β},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.alter m k f) k' =
    if (k == k') = true then (f (Std.ExtDHashMap.Const.get? m k)).get! else Std.ExtDHashMap.Const.get! m k'
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.LHom.mem_substructureReduct : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {L' : FirstOrder.Language} [inst_1 : L'.Structure M]
  (φ : L →ᴸ L') [inst_2 : φ.IsExpansionOn M] {x : M} {S : L'.Substructure M}, x ∈ φ.substructureReduct S ↔ x ∈ S
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_conjugation_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') {Z_1 : C}
  (h_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X' (CategoryTheory.MonoidalCategoryStruct.tensorObj Y' Z') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h)) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y' Z').hom h_1))
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpNatTrans_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (f : F ⟶ F')
  (X : CategoryTheory.AddGrp C), ((CategoryTheory.Functor.mapAddGrpNatTrans f).app X).hom.hom = f.app X.X
-- Mathlib.Logic.Equiv.Sum
Equiv.Perm.sumCongr_apply : ∀ {α : Type u_9} {β : Type u_10} (ea : Equiv.Perm α) (eb : Equiv.Perm β) (x : α ⊕ β),
  (ea.sumCongr eb) x = Sum.map (⇑ea) (⇑eb) x
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instMul : {X : AlgebraicGeometry.Scheme} → Mul X.IdealSheafData
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then `F.mapAddMon : AddMon C ⥤ AddMon D`
is fully faithful too.  -/
CategoryTheory.Functor.FullyFaithful.mapAddMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} → [inst_4 : F.Monoidal] → F.FullyFaithful → F.mapAddMon.FullyFaithful
-- Mathlib.RingTheory.Binomial
Ring.multichoose_eq_multichoose : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R) (n : ℕ),
  BinomialRing.multichoose r n = Ring.multichoose r n
-- Mathlib.Algebra.Order.Module.Field
Mathlib.Meta.Positivity.smul_nonneg_of_nonneg_of_pos : ∀ {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β] [inst_3 : Preorder α]
  [inst_4 : Preorder β] [PosSMulMono α β] {a : α} {b : β}, 0 ≤ a → 0 < b → 0 ≤ a • b
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasurableEmbedding.variation_map : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {Y : Type u_3} [inst_3 : MeasurableSpace Y] {φ : X → Y},
  MeasurableEmbedding φ → (μ.map φ).variation = MeasureTheory.Measure.map φ μ.variation
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_scalar : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (u : Rˣ),
  (Matrix.GeneralLinearGroup.map f) ((Matrix.GeneralLinearGroup.scalar n) u) =
    (Matrix.GeneralLinearGroup.scalar n) ((Units.map ↑f) u)
-- Mathlib.Data.Nat.Nth
Nat.nth_zero : ∀ {p : ℕ → Prop}, Nat.nth p 0 = sInf (Set.ofPred p)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisSkip : Lean.Options → Bool
-- Lean.Util.SCC
Lean.SCC.Data : Type
-- Mathlib.Analysis.SpecificLimits.Normed
/-- Partial sums of an alternating monotone series with an even number of terms provide
upper bounds on the limit.  -/
Monotone.tendsto_le_alternating_series : ∀ {E : Type u_4} [inst : Ring E] [inst_1 : PartialOrder E] [IsOrderedRing E] [inst_3 : TopologicalSpace E]
  [OrderClosedTopology E] {l : E} {f : ℕ → E},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l) →
    Monotone f → ∀ (k : ℕ), l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.le_iff_forall_le : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsPredPrelimit a → (b ≤ a ↔ ∀ (c : α), a < c → b ≤ c)
-- Mathlib.Data.Vector.Snoc
List.Vector.map₂_snoc : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {n : ℕ} {x : α} (xs : List.Vector α n) (ys : List.Vector β n)
  {f : α → β → σ} {y : β}, List.Vector.map₂ f (xs.snoc x) (ys.snoc y) = (List.Vector.map₂ f xs ys).snoc (f x y)
-- Mathlib.Order.Lex
/-- `ofLex` is the identity function from the `Lex` of a type.  -/
ofLex : {α : Type u_1} → Lex α ≃ α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' →
    Std.DHashMap.Const.get? (Std.DHashMap.map f m) k = Option.map (f k') (Std.DHashMap.Const.get? m k)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_two_of_utf8Size_eq_three : ∀ {c : Char} (hc : c.utf8Size = 3),
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte (String.utf8EncodeChar c)[2] = false
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.sub.sizeOf_spec : ∀ (a b : Int.Internal.Linear.Expr), sizeOf (a.sub b) = 1 + sizeOf a + sizeOf b
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.coeff_rescale : ∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (f : MvPowerSeries σ R) (a : σ → R) (n : σ →₀ ℕ),
  (MvPowerSeries.coeff n) ((MvPowerSeries.rescale a) f) = (n.prod fun s m => a s ^ m) * (MvPowerSeries.coeff n) f
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) (a : B),
  ((F.comp G).mapId a).inv = CategoryTheory.CategoryStruct.comp (G.mapId (F.obj a)).inv (G.map₂ (F.mapId a).inv)
-- Mathlib.Combinatorics.Quiver.Path
/-- `Reachable a b` holds when there is a directed path from `a` to `b`.

This is a preorder rather than an equivalence, since quiver paths are directed (compare the
symmetric `SimpleGraph.Reachable`).  -/
Quiver.Reachable : {V : Type u} → [Quiver V] → V → V → Prop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.forIn'_congr : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_3 : Std.Rxi.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_5 : Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rci α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
  {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableWithinAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x → DifferentiableWithinAt ℂ (fun x => Complex.sinh (f x)) s x
-- Mathlib.Algebra.Group.Hom.Instances
/-- `flip` arguments of `f : M →+ N →+ P`  -/
AddMonoidHom.flip : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} → {mM : AddZeroClass M} → {mN : AddZeroClass N} → {mP : AddCommMonoid P} → (M →+ N →+ P) → N →+ M →+ P
-- Mathlib.Order.RelClasses
instIsTransGt : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun x1 x2 => x2 < x1
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_neg : ∀ {x : ℝ}, x ∈ Set.Ioo (-1) 0 → Real.artanh x < 0
-- Init.Data.SInt.Lemmas
ISize.not_lt : ∀ {a b : ISize}, ¬a < b ↔ b ≤ a
-- Mathlib.Data.Rat.Defs
/-- **Alias** of `Rat.intCast_inj`. -/
Rat.coe_int_inj : ∀ {a b : ℤ}, ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.Functor.commShiftPullback_iso_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift B] (a : A) (b : B) (h : b = φ a),
  CategoryTheory.Functor.commShiftIso (CategoryTheory.PullbackShift.functor φ F) a =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.pullbackShiftIso C φ a b h) F ≪≫
      CategoryTheory.Functor.commShiftIso F b ≪≫ F.isoWhiskerLeft (CategoryTheory.pullbackShiftIso D φ a b h).symm
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.aemeasurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : Zero β]
  [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β]
  {f : α → β}, MeasureTheory.AEFinStronglyMeasurable f μ → AEMeasurable f μ
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.Tactic.Simps.NotationClass
/-- `className` is the name of the class we are looking for.  -/
Simps.AutomaticProjectionData.className : Simps.AutomaticProjectionData → Lean.Name
-- Batteries.Lean.TagAttribute
/-- Get the list of declarations tagged with the tag attribute `attr`.  -/
Lean.TagAttribute.getDecls : Lean.TagAttribute → Lean.Environment → Array Lean.Name
-- Mathlib.RingTheory.MvPowerSeries.Derivative
/-- The underlying function of the formal partial derivative with respect to variable `i`.
This is packaged as a derivation in `MvPowerSeries.pderiv`.  -/
MvPowerSeries.pderivFun : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → σ → MvPowerSeries σ R → MvPowerSeries σ R
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.range_toLin' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix m n R), (Matrix.toLin' M).range = Submodule.span R (Set.range M.col)
-- Mathlib.Data.List.Sigma
List.nodupKeys_singleton : ∀ {α : Type u} {β : α → Type v} (s : Sigma β), [s].NodupKeys
-- Init.Data.Int.Cooper
_private.Init.Data.Int.Cooper.0.Int.Cooper.resolve_left.eq_1 : ∀ (a c d p x : ℤ), Int.Cooper.resolve_left a c d p x = (a * x - p) % ↑(a.lcm (a * d / ↑((a * d).gcd c)))
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {i : ι} {Z : C} {q : Z ⟶ X i}
  (hq :
    (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows (CategoryTheory.Over.homMk q ⋯))
  {Z_1 : C} (h : S ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.hom✝ hq)
      (CategoryTheory.CategoryStruct.comp (f' (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.idx✝ hq))
        h) =
    CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (f i) h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_minKey!_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey ⋯
-- Mathlib.Order.Hom.Set
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices.  -/
OrderIso.Icc : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Lattice α] → [inst_1 : Lattice β] → (e : α ≃o β) → (x y : α) → ↑(Set.Icc x y) ≃o ↑(Set.Icc (e x) (e y))
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.smul_X_eq_monomial : ∀ {R : Type u} {a : R} [inst : Semiring R] {n : ℕ}, a • Polynomial.X ^ n = (Polynomial.monomial n) a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter m₂ ⋯).get! k = m₁.get! k
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toEventualRanges_map : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [inst_1 : CategoryTheory.IsCofilteredOrEmpty J] {X Y : J} (f : X ⟶ Y),
  F.toEventualRanges.map f =
    TypeCat.ofHom
      (Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (F.eventualRange X) (F.eventualRange Y) ⋯)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.exists_list_of_mem_closure : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {x : M},
  x ∈ AddSubmonoid.closure s → ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.sum = x
-- Mathlib.Data.W.Constructions
/-- The arity of the constructors for the naturals, `zero` takes no arguments, `succ` takes one  -/
WType.Natβ : WType.Natα → Type
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.ofHom_apply : ∀ {M N : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N] (f : NormedAddGroupHom M N)
  (r : M), (CategoryTheory.ConcreteCategory.hom (SemiNormedGrp.ofHom f)) r = f r
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {V W : CoalgCat R} [inst_1 : SizeOf R]
  (toCoalgHom' : ↑V.toModuleCat →ₗc[R] ↑W.toModuleCat), sizeOf { toCoalgHom' := toCoalgHom' } = 1 + sizeOf toCoalgHom'
-- Mathlib.CategoryTheory.Square
/-- the bottom-left object  -/
CategoryTheory.Square.X₃ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → C
-- Init.Data.Fin.Lemmas
Fin.castSucc_ne_zero_iff : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, a.castSucc ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Star.LinearMap
/-- The convolutive intrinsic star ring on linear maps from coalgebras
to ⋆-algebras, given that `star (toConv comul) = toConv (comm ∘ₗ comul)`.

In finite-dimensional C⋆-algebras, under the GNS construction, and the adjoint
coalgebra, we get this hypothesis.

See note [reducible non-instances].  -/
LinearMap.convIntrinsicStarRing : {R : Type u_5} →
  {A : Type u_6} →
    {C : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : NonUnitalNonAssocSemiring A] →
            [inst_3 : Module R A] →
              [inst_4 : SMulCommClass R A A] →
                [inst_5 : IsScalarTower R A A] →
                  [inst_6 : StarRing A] →
                    [StarModule R A] →
                      [inst_8 : AddCommMonoid C] →
                        [inst_9 : Module R C] →
                          [inst_10 : StarAddMonoid C] →
                            [inst_11 : StarModule R C] →
                              [inst_12 : Coalgebra R C] →
                                star (WithConv.toConv CoalgebraStruct.comul) =
                                    WithConv.toConv (↑(TensorProduct.comm R C C) ∘ₗ CoalgebraStruct.comul) →
                                  StarRing (WithConv (C →ₗ[R] A))
-- Mathlib.Order.CompleteLattice.Defs
/-- Note that we rarely use `CompleteSemilatticeSup`
(in fact, any such object is always a `CompleteLattice`, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.
 -/
CompleteSemilatticeSup : Type u_8 → Type u_8
-- Mathlib.Logic.IsEmpty.Defs
PEmpty.instIsEmpty : IsEmpty PEmpty.{u_1}
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂_map_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)}
  (φ : X ⟶ Y),
  ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).map φ).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Analysis.CStarAlgebra.Extreme
/-- **Alias** of `isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall`.

---

The star projections in a non-unital C⋆-algebra are exactly the extreme points of
the nonnegative closed unit ball.  -/
isStarProjection_iff_mem_extremePoints_setOf_nonneg_inter_unitClosedBall : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {e : A},
  IsStarProjection e ↔ e ∈ Set.extremePoints ℝ ({x | 0 ≤ x} ∩ Metric.closedBall 0 1)
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, Meromorphic f → MeromorphicAt f x
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.smul_def : ∀ (D : Type u_1) (Q : Type u_2) [inst : Group D] [inst_1 : Group Q] (Λ : Type u_3) [inst_2 : MulAction D Λ] {w : D ≀ᵣ Q}
  {p : Λ × Q}, w • p = (w.left (w.right * p.2) • p.1, w.right * p.2)
-- Init.Data.SInt.Bitwise
Int64.shiftRight_zero : ∀ {a : Int64}, a >>> 0 = a
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_sub_iff_add_le' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, b ≤ c - a ↔ a + b ≤ c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.tensorObjComp_hom_app : ∀ {C : Type u_2} {D : Type u_3} {E : Type u_4} [inst : CategoryTheory.Category.{v_2, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory C] [inst_4 : CategoryTheory.CartesianMonoidalCategory E]
  (F G : CategoryTheory.Functor D C) (H : CategoryTheory.Functor C E)
  [inst_5 : CategoryTheory.Limits.PreservesFiniteProducts H] (X : D),
  (CategoryTheory.Functor.Monoidal.tensorObjComp F G H).hom.app X =
    CategoryTheory.CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {a k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getKey? a = if compare k a = Ordering.eq then some k else t.getKey? a
-- Mathlib.Control.Monad.Writer
WriterT.run_pure : ∀ {M : Type u → Type v} {α ω : Type u} [inst : Monad M] (empty : ω) (append : ω → ω → ω) (a : α),
  (pure a).run = pure (a, empty)
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.EMatchTheoremPtr.mk : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatchTheoremPtr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.TreeSet.ofList l cmp).size = l.length
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
/-- **Alias** of `MeasureTheory.projectiveFamilyContent_sdiff`. -/
MeasureTheory.projectiveFamilyContent_diff : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s t : Set ((i : ι) → α i)}
  (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α →
      (MeasureTheory.projectiveFamilyContent hP) s - (MeasureTheory.projectiveFamilyContent hP) t ≤
        (MeasureTheory.projectiveFamilyContent hP) (s \ t)