mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Level
Lean.Level.PP.Result.quote : Lean.Level.PP.Result → ℕ → Lean.Syntax.Level
-- Std.Do.WP.SimpLemmas
Std.Do.WP.lift_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ε : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)}
  [inst : Std.Do.WP m ps] [inst_1 : Monad m] (x : m α),
  (Std.Do.wp (ExceptT.lift x)).apply Q = (Std.Do.wp (MonadLift.monadLift x)).apply Q
-- Mathlib.Algebra.Order.Monovary
Antivary.sub_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Antivary f g₁ → Monovary f g₂ → Antivary f (g₁ - g₂)
-- Aesop.Stats.Basic
Aesop.GoalKind.postNorm.sizeOf_spec : sizeOf Aesop.GoalKind.postNorm = 1
-- Mathlib.Data.Nat.Cast.Basic
Pi.instNatCast : {α : Type u_1} → {π : α → Type u_3} → [(a : α) → NatCast (π a)] → NatCast ((a : α) → π a)
-- Mathlib.CategoryTheory.Limits.Final
/-- A functor `F : C ⥤ D` is initial if for every `d : D`, the comma category of morphisms
`F.obj c ⟶ d` is connected.
 -/
CategoryTheory.Functor.Initial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedQueryString.mk.sizeOf_spec : ∀ {r : UInt8 → Bool} (toByteArray : ByteArray) (valid : Std.Http.URI.IsAllowedEncodedQueryChars r toByteArray),
  sizeOf { toByteArray := toByteArray, valid := valid } = 1 + sizeOf toByteArray + sizeOf valid
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - equality condition**: This theorem provides the equality condition for the
*positive* weighted version of the AM-GM inequality for real-valued nonnegative functions.

The condition is that all elements of `z` are equal to their center of mass `∑ i ∈ s, w i * z i`;
see `geom_mean_eq_arith_mean_weighted_iff_of_pos` for a version that compares the elements to each
other instead.  -/
Real.geom_mean_eq_arith_mean_weighted_iff_of_pos' : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 < w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.DocM.exec.getNames : Lean.Syntax → Lean.Elab.TermElabM (Array (Option Lean.Syntax))
-- Mathlib.Algebra.Lie.Character
/-- For an Abelian Lie algebra, characters are just linear forms.  -/
LieAlgebra.lieCharacterEquivLinearDual : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → [IsLieAbelian L] → LieAlgebra.LieCharacter R L ≃ Module.Dual R L
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The naturality of `coind₁ι` with respect to `coind₁ResMap`.  -/
ContRepresentation.coind₁ResMap_comp_coind₁ι_restrict : ∀ {R : Type u_1} {V : Type u_3} {W : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] [inst_5 : AddCommGroup W] [inst_6 : TopologicalSpace W]
  [inst_7 : IsTopologicalAddGroup W] [inst_8 : Module R W] {G : Type u_7} {H : Type u_8} [inst_9 : Group G]
  [inst_10 : TopologicalSpace G] [inst_11 : TopologicalSpace R] [inst_12 : ContinuousSMul R V]
  [inst_13 : ContinuousSMul R W] [inst_14 : Group H] [inst_15 : TopologicalSpace H] {π : ContRepresentation R G V}
  [inst_16 : IsTopologicalGroup G] [inst_17 : IsTopologicalGroup H] {π' : ContRepresentation R H W} (φ : H →ₜ* G)
  (f : ContIntertwiningMap (π.restrict ↑φ) π'),
  (ContRepresentation.coind₁ResMap φ f).comp (ContIntertwiningMap.restrict (↑φ) π.coind₁ι) = π'.coind₁ι.comp f
-- Mathlib.ModelTheory.Algebra.Field.Basic
/-- The first-order theory of fields, as a theory over the language of rings  -/
FirstOrder.Language.Theory.field : FirstOrder.Language.ring.Theory
-- Mathlib.Combinatorics.Additive.Corner.Roth
/-- The **corners theorem** for `ℕ`.

The maximum density of a corner-free set in `{1, ..., n} × {1, ..., n}` goes to zero as `n` tends to
infinity.  -/
corners_theorem_nat : ∀ {n : ℕ} {ε : ℝ},
  0 < ε →
    cornersTheoremBound (ε / 9) ≤ n → ∀ A ⊆ Finset.range n ×ˢ Finset.range n, ε * ↑n ^ 2 ≤ ↑A.card → ¬IsCornerFree ↑A
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
  (x : (CategoryTheory.Pairwise ι)ᵒᵖ),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).π.app x =
    CategoryTheory.Pairwise.rec
      (fun a =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c)
          (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) a))
      (fun a a_1 =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c)
          (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U)
            (CategoryTheory.Limits.Pi.π (fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1))))
      (Opposite.unop x)
-- Mathlib.Logic.Equiv.Defs
Equiv.symmEquiv_apply_symm_apply : ∀ (α : Sort u_1) (β : Sort u_2) (e : α ≃ β) (a : α), ((Equiv.symmEquiv α β) e).symm a = e.toFun a
-- Mathlib.Algebra.Ring.Fin
RingEquiv.piFinTwo_symm_apply : ∀ (R : Fin 2 → Type u_1) [inst : (i : Fin 2) → Semiring (R i)] (a : R 0 × R 1) (i : Fin 2),
  (RingEquiv.piFinTwo R).symm a i = (piFinTwoEquiv R).invFun a i
-- Mathlib.GroupTheory.Coprod.Basic
/-- Extensionality lemma for monoid homomorphisms `M ∗ N →* P`.
If two homomorphisms agree on the ranges of `Monoid.Coprod.inl` and `Monoid.Coprod.inr`,
then they are equal.  -/
Monoid.Coprod.hom_ext : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  {f g : Monoid.Coprod M N →* P},
  f.comp Monoid.Coprod.inl = g.comp Monoid.Coprod.inl → f.comp Monoid.Coprod.inr = g.comp Monoid.Coprod.inr → f = g
-- Batteries.Data.List.Perm
/-- Weaker version of `Subperm.cons_left`  -/
List.cons_subperm_of_not_mem_of_mem : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, a ∉ l₁ → a ∈ l₂ → l₁.Subperm l₂ → (a :: l₁).Subperm l₂
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.abs_norm : ∀ {d : ℤ}, d ≤ 0 → ∀ (n : ℤ√d), |n.norm| = n.norm
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_preimage_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {s : Set β},
  MeasurableSet s →
    ∀ (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel κ]
      [ProbabilityTheory.IsMarkovKernel η] (x : α), ((κ.compProd η) x) (Prod.fst ⁻¹' s) = (κ x) s
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.id.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : MulOneClass α],
  OrderMonoidHom.id α = { toMonoidHom := MonoidHom.id α, monotone' := ⋯ }
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_same_then' : ∀ {w : ℕ} (c : Bool) (t e : BitVec w), (t == bif c then t else e) = (c || t == e)
-- Mathlib.Probability.BorelCantelli
ProbabilityTheory.iIndepFun.condExp_natural_ae_eq_of_lt : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {β : Type u_3}
  [inst : LinearOrder ι] [mβ : MeasurableSpace β] [inst_1 : NormedAddCommGroup β] [inst_2 : BorelSpace β]
  {f : ι → Ω → β} {i j : ι} [SecondCountableTopology β] [CompleteSpace β] [inst_5 : NormedSpace ℝ β]
  (hf : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)),
  ProbabilityTheory.iIndepFun f μ →
    i < j → μ[f j | ↑(MeasureTheory.Filtration.natural f hf) i] =ᵐ[μ] fun x => ∫ (x : Ω), f j x ∂μ
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence pairwise preserves distance. Forward direction of
`congruent_iff_pairwise_dist_eq`.  -/
Congruent.pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], Congruent v₁ v₂ → Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.tateNorm.eq_1 : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  M.tateNorm =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ M).hom
      (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom M.norm) (groupCohomology.cochainsIso₀ M).inv)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.contMDiff_num : ∀ {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ),
  ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun τ => UpperHalfPlane.num g ↑τ
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp (F'.map ((CategoryTheory.Functor.commShiftIso L a).inv.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
          ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app X))))
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_lieSubalgebra_mk_right : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (L' : LieSubalgebra R L) {x : ↥L'} {y : L} (hy : y ∈ L'),
  ((LieModule.traceForm R (↥L') M) x) ⟨y, hy⟩ = ((LieModule.traceForm R L M) ↑x) y
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.add : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α β : E),
  IsSolvableByRad F α → IsSolvableByRad F β → IsSolvableByRad F (α + β)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_def : ∀ {X Y : TopCat} (f : X ⟶ Y),
  TopologicalSpace.Opens.map f =
    { obj := fun U => { carrier := ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ },
      map := fun {X_1 Y_1} i => { down := { down := ⋯ } }, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioo_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioo (a + n • b) (a + (n + 1) • b))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKey? k = m.getKey? k
-- Mathlib.RingTheory.AdjoinRoot
/-- If `S` is an extension of `R` with power basis `pb` and `g` is a monic polynomial over `R`
such that `pb.gen` has a minimal polynomial `g`, then `S` is isomorphic to `AdjoinRoot g`.

Compare `PowerBasis.equivOfRoot`, which would require
`h₂ : aeval pb.gen (minpoly R (root g)) = 0`; that minimal polynomial is not
guaranteed to be identical to `g`.  -/
AdjoinRoot.equiv' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (g : Polynomial R) →
            (pb : PowerBasis R S) →
              (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0 →
                (Polynomial.aeval pb.gen) g = 0 → AdjoinRoot g ≃ₐ[R] S
-- Mathlib.FieldTheory.Separable
AlgHom.natCard_of_powerBasis : ∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} {L : Type u_5} [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K S] [inst_4 : Algebra K L] (pb : PowerBasis K S),
  IsSeparable K pb.gen → (Polynomial.map (algebraMap K L) (minpoly K pb.gen)).Splits → Nat.card (S →ₐ[K] L) = pb.dim
-- Init.Data.String.Pattern.Basic
/-- A strict backward pattern is one which never drops an empty suffix.

This condition ensures that the default searcher derived from the backward pattern is a finite
iterator.
 -/
String.Slice.Pattern.StrictBackwardPattern : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Prop
-- Std.Data.HashSet.Lemmas
Std.HashSet.all_eq_true_iff_forall_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {p : α → Bool},
  m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p (m.get a h) = true
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_naturality_left_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X' X : C} {Y : D} (f : X' ⟶ X)
  (g : X ⟶ G.obj Y),
  (adj.homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (F.map f) ((adj.homEquiv X Y).symm g)
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.conjTranspose_circulant : ∀ {α : Type u_1} [inst : Star α] {n : ℕ} (v : Fin n → α),
  (Matrix.circulant v).conjTranspose = Matrix.circulant (star fun i => v (-i))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.liftTruncLT_aux : ∀ {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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ [t.IsLE X n₀], ∃ f', f = CategoryTheory.CategoryStruct.comp f' ((t.truncLTι n₁).app Y)
-- Mathlib.Analysis.RCLike.Basic
/-- The imaginary unit.  -/
RCLike.I_re : ∀ {K : Type u_1} [inst : RCLike K], RCLike.re RCLike.I = 0
-- Init.Data.Rat.Lemmas
Rat.inv_mul_rev : ∀ (a b : ℚ), (a * b)⁻¹ = b⁻¹ * a⁻¹
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Monoid R} {inst_1 : Monoid S}
  {φ : outParam (R →* S)} {A : outParam (Type u_4)} {B : outParam (Type u_5)} {inst_2 : NonUnitalNonAssocSemiring A}
  {inst_3 : NonUnitalNonAssocSemiring B} {inst_4 : DistribMulAction R A} {inst_5 : DistribMulAction S B}
  {inst_6 : FunLike F A B} [self : NonUnitalAlgSemiHomClass F φ A B], DistribMulActionSemiHomClass F (⇑φ) A B
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.mem_unop : ∀ {M : Type u_2} [inst : AddZeroClass M] {x : M} {S : AddSubmonoid Mᵃᵒᵖ}, x ∈ S.unop ↔ AddOpposite.op x ∈ S
-- Mathlib.Data.Stream.Init
Stream'.eta : ∀ {α : Type u} (s : Stream' α), Stream'.cons s.head s.tail = s
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.returnsPi : Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_eq_universallySpecializing : @AlgebraicGeometry.UniversallyClosed =
  (AlgebraicGeometry.topologically @SpecializingMap).universally ⊓ @AlgebraicGeometry.QuasiCompact
-- Lean.DocString.Extension
/-- A deferred check that lacked sufficient information when it was used (e.g. a forward references to
a name in a downstream module). The `index` identifies it among the docstring's deferred checks
that are stored in an environment extension. Inline and block deferred checks use the same
counter.
 -/
Lean.ElabBlock.deferred : ℕ → Lean.ElabBlock
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.instDecompositionFiniteArchimedeanClassSubtypeMemSubmoduleBaseDomainStratum' : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      (u : HahnEmbedding.ArchimedeanStrata K M) → DirectSum.Decomposition u.stratum'
-- Mathlib.Topology.NhdsWithin
Set.MapsTo.preimage_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} {s : Set α} {t : Set β} {x : α},
  Set.MapsTo f s t → f ⁻¹' t ∈ nhdsWithin x s
-- Init.Data.UInt.Lemmas
UInt64.ofNat_uInt8ToNat : ∀ (n : UInt8), UInt64.ofNat n.toNat = n.toUInt64
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Technical lemma to prove that candidates are Lipschitz  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_lipschitz_aux : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y}
  {x y z t : X ⊕ Y},
  f ∈ GromovHausdorff.candidates X Y → f (x, y) - f (z, t) ≤ 2 * ↑(GromovHausdorff.maxVar✝ X Y) * dist (x, y) (z, t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.add_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N)
  [CategoryTheory.IsAddMonHom g],
  CategoryTheory.CategoryStruct.comp (f₁ + f₂) g =
    CategoryTheory.CategoryStruct.comp f₁ g + CategoryTheory.CategoryStruct.comp f₂ g
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (K : CochainComplex C ℤ),
  HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ↔
    HomologicalComplex.Acyclic K
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_iInf : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (s : Set (Submodule R E)), ↑(⨅ S ∈ s, S) = ⨅ S ∈ s, ↑S
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.Iso.asOver_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (e : X ≅ Y) [inst_3 : CategoryTheory.HomIsOver e.hom S],
  (CategoryTheory.Iso.asOver S e).inv = CategoryTheory.OverClass.asOverHom S e.inv
-- Mathlib.Order.SuccPred.Basic
Order.bot_lt_succ : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : OrderBot α] [Nontrivial α] (a : α),
  ⊥ < Order.succ a
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (iso₁ iso₁_1 : A.obj₁ ≅ B.obj₁) (e_iso₁ : iso₁ = iso₁_1)
  (iso₂ iso₂_1 : A.obj₂ ≅ B.obj₂) (e_iso₂ : iso₂ = iso₂_1) (iso₃ iso₃_1 : A.obj₃ ≅ B.obj₃) (e_iso₃ : iso₃ = iso₃_1)
  (comm₁ : CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁)
  (comm₂ : CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂)
  (comm₃ :
    CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) =
      CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃),
  A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃ = A.isoMk B iso₁_1 iso₂_1 iso₃_1 ⋯ ⋯ ⋯
-- Std.Sync.Broadcast
/-- Subscribes a new `Receiver` from the `Broadcast` channel.
 -/
Std.Broadcast.subscribe : {α : Type} → Std.Broadcast α → IO (Std.Broadcast.Receiver α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The chain complex associated to a simplicial set, with coefficients in `R : C`.
It computes the simplicial homology of a simplicial sets with coefficients
in `R`. One can recover the ordinary simplicial chain complex when `C := Ab`
and `X := ℤ`.
 -/
SSet.chainComplexFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        CategoryTheory.Functor C (CategoryTheory.Functor SSet (ChainComplex C ℕ))
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `c` is limiting  -/
CategoryTheory.EquivalenceRelation.isLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} →
      {p₁ p₂ : R ⟶ X} → (self : CategoryTheory.EquivalenceRelation p₁ p₂) → CategoryTheory.Limits.IsLimit self.c
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (x : Lean.Grind.CommRing.Expr) →
    ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k)) →
      ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) →
        ((k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k)) →
          ((x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x)) →
            ((a b : Lean.Grind.CommRing.Expr) → motive (a.add b)) →
              ((a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) →
                ((a : Lean.Grind.CommRing.Expr) → motive a.neg) →
                  ((a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) →
                    ((a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) → motive x
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.tryCur : {m : Type → Type} → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Bool
-- Mathlib.Data.Finset.Insert
List.toFinset_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α}, (a :: l).toFinset = insert a l.toFinset
-- Mathlib.Algebra.Category.BoolRing
BoolAlg.hasForgetToBoolRing : CategoryTheory.HasForget₂ BoolAlg BoolRing
-- Lean.AuxRecursor
Lean.NoConfusionInfo.regular.sizeOf_spec : ∀ (arity lhs rhs : ℕ), sizeOf (Lean.NoConfusionInfo.regular arity lhs rhs) = 1 + sizeOf arity + sizeOf lhs + sizeOf rhs
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCommandInfo : Lean.Elab.CommandInfo → Lean.Elab.Info
-- Mathlib.Data.DFinsupp.Submonoid
/-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
`DFinsupp.sumAddHom` composed with `DFinsupp.filterAddMonoidHom`; that is, every element in the
bounded `iSup` can be produced from taking a finite number of non-zero elements from the `S i` that
satisfy `p i`, coercing them to `γ`, and summing them.  -/
AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] (p : ι → Prop) [inst_1 : DecidablePred p] [inst_2 : AddCommMonoid γ]
  (S : ι → AddSubmonoid γ),
  ⨆ i, ⨆ (_ : p i), S i =
    AddMonoidHom.mrange
      ((DFinsupp.sumAddHom fun i => (S i).subtype).comp (DFinsupp.filterAddMonoidHom (fun i => ↥(S i)) p))
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionOptions.toJson : Lean.Lsp.CodeActionOptions → Lean.Json