mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesOfIsCocycle₂_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] {f : G × G → A} (hf : groupCohomology.IsCocycle₂ f)
  (a : G × G), ↑(groupCohomology.cocyclesOfIsCocycle₂ hf) a = f a
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
_private.Mathlib.Data.QPF.Multivariate.Constructions.Sigma.0.MvQPF.Sigma.instMvFunctor.match_1.splitter : {n : ℕ} →
  {A : Type u_1} →
    (F : A → TypeVec.{u_1} n → Type u_1) →
      {α : TypeVec.{u_1} n} →
        (motive : MvQPF.Sigma F α → Sort u_2) →
          (x : MvQPF.Sigma F α) → ((a : A) → (x : F a α) → motive ⟨a, x⟩) → motive x
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instVAddForall : {M : Type u_1} → {β : Type u_2} → {α : Type u_3} → [VAdd M α] → VAdd Mᵈᵃᵃ (α → β)
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLeftOrthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C), P.leftOrthogonal.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Group.AddChar
/-- The trivial additive character (sending everything to `1`).  -/
AddChar.instZero : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → Zero (AddChar A M)
-- Mathlib.Data.Set.Image
Set.image_preimage_inl_union_image_preimage_inr : ∀ {α : Type u_1} {β : Type u_2} (s : Set (α ⊕ β)), Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (ictx : Lean.Parser.InputContext) (stx : Lean.Syntax) (result? : Option Lean.Language.Lean.HeaderParsedState),
  sizeOf { toSnapshot := toSnapshot, metaSnap := metaSnap, ictx := ictx, stx := stx, result? := result? } =
    1 + sizeOf toSnapshot + sizeOf metaSnap + sizeOf ictx + sizeOf stx + sizeOf result?
-- Mathlib.RingTheory.Multiplicity
multiplicity_le_emultiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, ↑(multiplicity a b) ≤ emultiplicity a b
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.swap' : ∀ {f : ℕ → ℕ → ℕ}, Nat.Primrec (Nat.unpaired f) → Nat.Primrec (Nat.unpaired (Function.swap f))
-- Std.Internal.Do.Order.Basic
/-- Embedding of propositions into an CompleteLattice type. `⌜p⌝` embeds `p : Prop` as `⊤` if `p` holds
and `⊥` otherwise.  -/
Lean.Order.«term⌜_⌝» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Also see `Module.finrank_bot_le_finrank_of_isScalarTower`
for a version with different typeclass constraints.  -/
Module.finrank_bot_le_finrank_of_isScalarTower_of_free : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (S : Type u_2) (T : Type u_3) [inst_2 : Semiring S]
  [inst_3 : Semiring T] [inst_4 : Module R T] [inst_5 : Module S T] [inst_6 : Module R S] [IsScalarTower R S T]
  [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite S T] [Module.Free R S],
  Module.finrank R S ≤ Module.finrank R T
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.containsThenInsert_eq_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), (m.containsThenInsert a b).2 = m.insertₘ a b
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.conv_dirac : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] (x : M),
  μ.conv (MeasureTheory.Measure.dirac x) = MeasureTheory.Measure.map (fun y => y + x) μ
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
CovariantDerivative.torsion_apply_eq_extend : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} [inst_6 : CompleteSpace 𝕜]
  [inst_7 : CompleteSpace E] [inst_8 : FiniteDimensional 𝕜 E] [inst_9 : IsManifold I 2 M]
  (cov : CovariantDerivative I E (TangentSpace I)) (X₀ Y₀ : TangentSpace I x),
  ((cov.torsion x) X₀) Y₀ =
    (↑cov (FiberBundle.extend E Y₀) x) (FiberBundle.extend E X₀ x) -
        (↑cov (FiberBundle.extend E X₀) x) (FiberBundle.extend E Y₀ x) -
      VectorField.mlieBracket I (FiberBundle.extend E X₀) (FiberBundle.extend E Y₀) x
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear.eq_1 : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) (n : ℕ),
  f.toFormalMultilinearSeriesOfMultilinear n =
    if h : Fintype.card (Option ι) = n then
      ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq h) f.continuousMultilinearMapOption
    else 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Construct an instance of `CartesianMonoidalCategory C` given a terminal object and limit cones
over arbitrary pairs of objects.  -/
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C) →
      ((X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) →
        CategoryTheory.CartesianMonoidalCategory C
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.seq.eq_def : ∀ {α : Type u_1} {β : Type u_2} (x : ℕ) (x_1 : Fin x → α → β) (x_2 : Fin x → α),
  FinVec.seq x_1 x_2 =
    match (motive := (x : ℕ) → (Fin x → α → β) → (Fin x → α) → Fin x → β) x, x_1, x_2 with
    | 0, x, x_3 => ![]
    | n.succ, f, v => Matrix.vecCons (f 0 (v 0)) (FinVec.seq (Matrix.vecTail f) (Matrix.vecTail v))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
cfcₙ_norm_sq_nonneg : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A]
  [inst_2 : TopologicalSpace A] [inst_3 : Module 𝕜 A] [inst_4 : StarRing A] [inst_5 : PartialOrder A]
  [StarOrderedRing A] [inst_7 : IsScalarTower 𝕜 A A] [inst_8 : SMulCommClass 𝕜 A A]
  [inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A), 0 ≤ cfcₙ (fun z => star (f z) * f z) a
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.comap_id : ∀ {R : Type u_2} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid F] [inst_4 : TopologicalSpace F] [inst_5 : Module R F] (C : ProperCone R F),
  ProperCone.comap (ContinuousLinearMap.id R F) C = C
-- Batteries.Data.List.Lemmas
List.idxsOf_take : ∀ {α : Type u_1} {xs : List α} {n : ℕ} {x : α} {s : ℕ} [inst : BEq α],
  List.idxsOf x (List.take n xs) s = List.take (List.count x (List.take n xs)) (List.idxsOf x xs s)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.p : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Int.Internal.Linear.Poly
-- Mathlib.Data.NNRat.Defs
NNRat.coe_max : ∀ (x y : ℚ≥0), ↑(max x y) = max ↑x ↑y
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatTrans.naturality_1_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) {Z : D} (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map e.inv)
      (CategoryTheory.CategoryStruct.comp (α.app X) (CategoryTheory.CategoryStruct.comp (G.map e.hom) h)) =
    CategoryTheory.CategoryStruct.comp (α.app Y) h
-- Mathlib.Order.Filter.Map
Filter.bind_mono : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : α → Filter β},
  f₁ ≤ f₂ → g₁ ≤ᶠ[f₁] g₂ → f₁.bind g₁ ≤ f₂.bind g₂
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.of_norm_eventuallyEq : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} {g : α → ℝ},
  (fun x => ‖f' x‖) =ᶠ[l] g → f' =Θ[l] g
-- Plausible.DeriveShrinkable
/-- Creates a `mutual ... end` block containing the shrink function definitions  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkMutualBlock : Lean.Elab.Deriving.Context → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_univ : dimH Set.univ = 1
-- Init.Data.Nat.Lemmas
Nat.one_lt_two_pow : ∀ {n : ℕ}, n ≠ 0 → 1 < 2 ^ n
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The action of a natural isomorphism on pushforward functors of sheaves.  -/
CategoryTheory.Functor.sheafPushforwardContinuousIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} →
          (F ≅ F') →
            (A : Type u) →
              [inst_2 : CategoryTheory.Category.{t, u} A] →
                (J : CategoryTheory.GrothendieckTopology C) →
                  (K : CategoryTheory.GrothendieckTopology D) →
                    [inst_3 : F.IsContinuous J K] →
                      [inst_4 : F'.IsContinuous J K] →
                        F.sheafPushforwardContinuous A J K ≅ F'.sheafPushforwardContinuous A J K
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.tendsto_setIntegral_of_monotone : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [inst_2 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Monotone s →
      MeasureTheory.IntegrableOn f (⋃ n, s n) μ →
        Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ n, s n, f x ∂μ))
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.fst_comp_inl : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P),
  (QuadraticMap.Isometry.fst M₂ Q₁).comp (QuadraticMap.Isometry.inl Q₁ 0) = QuadraticMap.Isometry.id Q₁
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f f_1 : β k → β k),
  f = f_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β),
      t = t_1 → Std.DTreeMap.Internal.Impl.modify k f t = Std.DTreeMap.Internal.Impl.modify k f_1 t_1
-- Mathlib.Analysis.Complex.Circle
Real.fourierChar_apply : ∀ (x : ℝ), ↑(Real.fourierChar x) = Complex.exp (↑(2 * Real.pi * x) * Complex.I)
-- Mathlib.Data.Fin.SuccPred
Fin.forall_fin_succ' : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P i.castSucc) ∧ P (Fin.last n)
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- If a Gaussian measure is not a Dirac, then it has value zero on singletons.  -/
ProbabilityTheory.IsGaussian.nullSingletonClass : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  (∀ (x : E), μ ≠ MeasureTheory.Measure.dirac x) → MeasureTheory.NullSingletonClass μ
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonLogConfig : Lean.ToJson Lean.Lsp.LogConfig
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_cons_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.getValue k (⟨k, v⟩ :: l) ⋯ = v
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of adding a point to a set with a set with finite-dimensional
direction of the `affineSpan` is finite-dimensional.  -/
finiteDimensional_direction_affineSpan_insert_set : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P) [FiniteDimensional k ↥(affineSpan k s).direction] (p : P),
  FiniteDimensional k ↥(affineSpan k (insert p s)).direction
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_mul_cancel : ∀ {a b : ℤ}, b ∣ a → a.fdiv b * b = a
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- A morphism from the weak pullback of `W ⟶ S` and `X ⟶ S` to the weak pullback of
`Y ⟶ T` and `Z ⟶ T` given `S ⟶ T`.  -/
CategoryTheory.Limits.weakPullback.mapDesc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y S T : C} →
      (f : X ⟶ S) →
        (g : Y ⟶ S) →
          (i : S ⟶ T) →
            [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] →
              [inst_2 :
                  CategoryTheory.Limits.HasWeakPullback (CategoryTheory.CategoryStruct.comp f i)
                    (CategoryTheory.CategoryStruct.comp g i)] →
                CategoryTheory.Limits.weakPullback f g ⟶
                  CategoryTheory.Limits.weakPullback (CategoryTheory.CategoryStruct.comp f i)
                    (CategoryTheory.CategoryStruct.comp g i)
-- Mathlib.Algebra.Group.ULift
ULift.addZeroClass.eq_1 : ∀ {α : Type u} [inst : AddZeroClass α], ULift.addZeroClass = Function.Injective.addZeroClass ⇑Equiv.ulift ⋯ ⋯ ⋯
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁.eq_1 : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R),
  MvPolynomial.bind₁ f = MvPolynomial.aeval f
-- Lean.DeclarationRange
Lean.builtinDeclRanges : IO.Ref (Lean.NameMap Lean.DeclarationRanges)
-- Init.Grind.Interactive
/-- `simp` applies the structural simplifier to the goal target.
Only available in `sym =>` mode.

- `simp` — uses the default (identity) variant
- `simp myVariant` — uses a named variant registered via `register_sym_simp`
- `simp [thm₁, thm₂, ...]` — default variant with extra rewrite theorems appended to `post`
- `simp myVariant [thm₁, thm₂, ...]` — named variant with extra theorems
 -/
Lean.Parser.Tactic.Grind.symSimp : Lean.ParserDescr
-- Mathlib.Order.SupClosed
SemilatticeInf.toCompleteSemilatticeInf.eq_1 : ∀ {α : Type u_3} [inst : SemilatticeInf α] (sSup : Set α → α) (h : ∀ (s : Set α), InfClosed s → IsGLB s (sSup s)),
  SemilatticeInf.toCompleteSemilatticeInf sSup h =
    { toPartialOrder := inst.toPartialOrder, sInf := fun s => sSup (infClosure s), isGLB_sInf := ⋯ }
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instIsPredArchimedeanMultiplicative : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : PredOrder X] [h : IsPredArchimedean X],
  IsPredArchimedean (Multiplicative X)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
neg_of_mul_pos_right : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α] [MulPosMono α],
  0 < a * b → a ≤ 0 → b < 0
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isEmbedding_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsEmbedding SetLike.coe
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for finite sets of convex sets in its classical form.

If `F` is a finite set of convex sets in a vector space of finite dimension `d`, with `n ≥ d + 1`,
and any `d + 1` sets from `F` intersect nontrivially,
then all sets from `F` intersect nontrivially.  -/
Convex.helly_theorem_set : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : Finset (Set E)},
  Module.finrank 𝕜 E + 1 ≤ F.card →
    (∀ X ∈ F, Convex 𝕜 X) → (∀ G ⊆ F, G.card = Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) → (⋂₀ ↑F).Nonempty
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.refl : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.HashMap α β), m.Equiv m
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- Given a submodule `M ⊆ R` and a prime ideal `p` of `M⁻¹R`, with `f : R →+* S` the localization
map, then `(M⁻¹R)ₚ` is isomorphic (as an `R`-algebra) to the localization of `R` at `f⁻¹(p)`.
 -/
IsLocalization.localizationLocalizationAtPrimeIsoLocalization : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (p : Ideal (Localization M)) →
        [inst_1 : p.IsPrime] →
          Localization.AtPrime (Ideal.comap (algebraMap R (Localization M)) p) ≃ₐ[R] Localization.AtPrime p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
NonUnitalStarSubalgebra.ofClass.congr_simp : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : SetLike S A] [inst_5 : NonUnitalSubsemiringClass S A]
  [inst_6 : SMulMemClass S R A] [inst_7 : StarMemClass S A] (s s_1 : S),
  s = s_1 → NonUnitalStarSubalgebra.ofClass s = NonUnitalStarSubalgebra.ofClass s_1
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The monoid homomorphism from the colimit monoid to the cone point of any other cocone.  -/
MonCat.Colimits.descMorphism : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    (F : CategoryTheory.Functor J MonCat) → (s : CategoryTheory.Limits.Cocone F) → MonCat.Colimits.colimit F ⟶ s.pt
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_id : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.map LinearMap.id p = p
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  (X.restrict ⋯).presheaf =
    (TopCat.Presheaf.pushforward C (TopologicalSpace.Opens.inclusionTopIso ↑X).inv).obj X.presheaf
-- Init.Prelude
/-- The number of distinct values representable by `UInt32`, that is, `2^32 = 4294967296`.  -/
UInt32.size : ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C},
  sq₁.IsPushout → ∀ (e : sq₁ ≅ sq₂), sq₂.IsPushout
-- Lean.ResolveName
/-- Given a namespace identifier, return the unique interpretation or else fail.  -/
Lean.resolveUniqueNamespace : {m : Type → Type} →
  [Monad m] → [Lean.MonadResolveName m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Ident → m Lean.Name
-- Lean.Declaration
/-- List of all (including this one) declarations in the same mutual block.
See comment at `DefinitionVal.all`.  -/
Lean.OpaqueVal.all : Lean.OpaqueVal → List Lean.Name
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.add_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {x : X}, ContinuousAt f x → ∀ (b : M), ContinuousAt (fun x => f x + b) x
-- Lean.Elab.Tactic.Grind.Basic
/-- Execute `x` using the main goal local context and instances  -/
Lean.Elab.Tactic.Grind.withMainContext : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Given `h : toInt a = b`, if `b` is of the form `i.wrap b'`,
invokes `expandWrap a b' h`
 -/
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.expandIfWrap : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Combinatorics.SetFamily.FourFunctions
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.collapse.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] (𝒜 : Finset (Finset α)) (a : α)
  (f : Finset α → β) (s : Finset α), collapse✝ 𝒜 a f s = ∑ t ∈ 𝒜 with t.erase a = s, f t
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  [inst_8 : SizeOf 𝕜] [inst_9 : SizeOf E] [inst_10 : SizeOf H] [inst_11 : SizeOf G]
  (toDerivation :
    Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤))
  (left_invariant'' :
    ∀ (g : G), (hfdifferential ⋯) ((Derivation.evalAt 1) toDerivation) = (Derivation.evalAt g) toDerivation),
  sizeOf { toDerivation := toDerivation, left_invariant'' := left_invariant'' } = 1 + sizeOf toDerivation
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.splitAt.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → List α → Sort u_2) (x : ℕ) (x_1 : List α)
  (h_1 : (x : ℕ) → (x_2 : List α) → motive [] x x_2)
  (h_2 : (x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc)
  (h_3 : (xs : List α) → (x : ℕ) → (acc : List α) → motive xs x acc),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | x :: xs, n.succ, acc => h_2 x xs n acc
    | xs, x, acc => h_3 xs x acc) =
    h_1 x x_1
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagramIso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J),
  (D.diagramIso F).inv.app (CategoryTheory.Limits.WalkingMultispan.right i) =
    CategoryTheory.CategoryStruct.id
      ((D.mapGlueData F).diagram.multispan.obj (CategoryTheory.Limits.WalkingMultispan.right i))
-- Init.Data.List.Attach
List.foldr_attachWith : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {q : α → Prop} (H : ∀ a ∈ l, q a) {f : { x // q x } → β → β} {b : β},
  List.foldr f b (l.attachWith q H) = List.foldr (fun a acc => f ⟨↑a, ⋯⟩ acc) b l.attach
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.isUnsat : Nat.Internal.Linear.PolyCnstr → Bool
-- Init.Data.BitVec.Bitblast
/-- The sum of widths of the dividend and remainder is `w`.  -/
BitVec.DivModState.Lawful.hwrn : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → qr.wr + qr.wn = w
-- Init.Tactics
/-- Use this rewrite rule after entering the subterms  -/
Lean.Parser.Tactic.simpPost : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.AEDisjoint.of_absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t →
    ∀ {ν : MeasureTheory.Measure α}, ν.AbsolutelyContinuous μ → MeasureTheory.AEDisjoint ν s t
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under subtraction.  -/
Dioph.«term_D-_» : Lean.TrailingParserDescr
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.canonType.sizeOf_spec : sizeOf Lean.Meta.Sym.Canon.ShouldCanonResult.canonType✝ = 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  CategoryTheory.CategoryStruct.comp (groupCohomology.H1π A) (groupCohomology.H1IsoOfIsTrivial A).hom =
    (groupCohomology.cocycles₁IsoOfIsTrivial A).hom
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.isRadical_of_eq_jacobson : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.jacobson = I → I.IsRadical