mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.mk : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {c : NNReal}
  {μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasSubgaussianMGF._auto_1},
  (∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ) →
    (∀ (t : ℝ), ProbabilityTheory.mgf X μ t ≤ Real.exp (↑c * t ^ 2 / 2)) → ProbabilityTheory.HasSubgaussianMGF X c μ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.instNonemptySMulCandidate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [CategoryTheory.Presheaf.IsLocallyInjective J φ] [CategoryTheory.Presheaf.IsLocallySurjective J φ] {X : Cᵒᵖ}
  (r : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)), Nonempty (PresheafOfModules.Sheafify.SMulCandidate α φ r m)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Shared state for non-commutative and commutative semirings.  -/
Lean.Meta.Grind.Arith.CommRing.Semiring : Type
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.WF →
    t.getKey? k = some k' → (Std.TreeMap.Raw.filterMap f t).getD k fallback = (t[k]?.bind fun x => f k' x).getD fallback
-- Mathlib.RingTheory.KrullDimension.Zero
le_isUnit_iff_zero_notMem : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R] {M : Submonoid R},
  M ≤ IsUnit.submonoid R ↔ 0 ∉ M
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsWeakLimit t) {W : C} (h : W ⟶ X)
  (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C}
  (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w)
      (CategoryTheory.CategoryStruct.comp t.snd h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.nontrivial_of_not_isIsolated : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, ¬G.IsIsolated v → Nontrivial V
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.id_apply : ∀ {α : Type u_2} [inst : Max α] [inst_1 : Bot α] (a : α), (SupBotHom.id α) a = a
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The associator as a bimodule isomorphism.  -/
Bimod.associatorBimod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {W X Y Z : CategoryTheory.Mon C} →
              (L : Bimod W X) →
                (M : Bimod X Y) → (N : Bimod Y Z) → (L.tensorBimod M).tensorBimod N ≅ L.tensorBimod (M.tensorBimod N)
-- Mathlib.RingTheory.Localization.Pi
/-- Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote
the projection of `M` onto each corresponding factor. Given a ring homomorphism from the direct
product `Π i, R i` to the product of the localizations of each `R i` at `M' i`, every `y : M`
maps to a unit under this homomorphism.  -/
IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom : ∀ {ι : Type u_1} (R : ι → Type u_2) (S : ι → Type u_3) [inst : (i : ι) → CommSemiring (R i)]
  [inst_1 : (i : ι) → CommSemiring (S i)] [inst_2 : (i : ι) → Algebra (R i) (S i)] (M : Submonoid ((i : ι) → R i))
  [∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)] (y : ↥M),
  IsUnit ((RingHom.pi fun i => (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i)) ↑y)
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.ext : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  ⦃f g : AbsoluteValue R S⦄, (∀ (x : R), f x = g x) → f = g
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_tfae : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ},
  IsOpen C →
    C.Nonempty →
      ConvexOn ℝ C f →
        [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
            ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) f,
            ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) f,
            ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) |f|].TFAE
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg : ∀ {x y : ℝ*}, ¬x.Infinitesimal → x < 0 → y.InfiniteNeg → (x * y).InfinitePos
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.subgroup_iff : ∀ {G : Type u_1} {K : Type u_3} {L : Type u_4} [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] {H : Subgroup G} {F : IntermediateField K L}
  [hGKL : IsGaloisGroup G K L], IsGaloisGroup (↥H) (↥F) L ↔ FixedPoints.intermediateField ↥H = F
-- Init.Data.Order.Ord
Std.OrientedCmp.gt_iff_lt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.gt ↔ cmp b a = Ordering.lt
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- **Alias** of `Metric.closedBall_sdiff_ball`. -/
Metric.closedBall_diff_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
-- Mathlib.CategoryTheory.Limits.Connected
/-- If `J` is connected, `F : J ⥤ C` and `c` is a cone on `F`, then to check that `c` is a
limit it is sufficient to check that `limMap c.π` is an isomorphism. The converse is also
true, see `Cone.isLimit_iff_isIso_limMap_π`.  -/
CategoryTheory.Limits.Cone.isLimitOfIsIsoLimMapπ : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        [inst_2 : CategoryTheory.IsConnected J] →
          {F : CategoryTheory.Functor J C} →
            [inst_3 : CategoryTheory.Limits.HasLimit F] →
              (c : CategoryTheory.Limits.Cone F) →
                [CategoryTheory.IsIso (CategoryTheory.Limits.limMap c.π)] → CategoryTheory.Limits.IsLimit c
-- Init.Data.BitVec.Bitblast
/-- Adding bitvectors that are zero in complementary positions equals concatenation.
We add a `no_index` annotation to `HAppend.hAppend` such that the width `v + w`
does not act as a key in the discrimination tree.
This is important to allow matching, when the type of the result of append
`x : BitVec 3` and `y : BitVec 4` has been reduced to `x ++ y : BitVec 7`.
 -/
BitVec.append_zero_add_zero_append : ∀ {v w : ℕ} {x : BitVec v} {y : BitVec w}, x ++ 0#w + (0#v ++ y) = x ++ y
-- Std.Http.Data.Chunk
Std.Http.Chunk.mk.injEq : ∀ (data : ByteArray) (extensions : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue))
  (data_1 : ByteArray) (extensions_1 : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)),
  ({ data := data, extensions := extensions } = { data := data_1, extensions := extensions_1 }) =
    (data = data_1 ∧ extensions = extensions_1)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.count_associates_factors_eq`.

---

The number of times an ideal `I` occurs as normalized factor of another ideal `J` is stable
when regarding these ideals as associated elements of the monoid of ideals.  -/
count_associates_factors_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I J : Ideal R},
  I ≠ 0 →
    J.IsPrime →
      J ≠ ⊥ →
        (Associates.mk J).count (Associates.mk I).factors =
          Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)
-- Lean.Parser.Extra
Lean.Parser.withForbidden.parenthesizer : Lean.Parser.Token → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.comap_toSubsemiring : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B),
  (Subalgebra.comap f S).toSubsemiring = Subsemiring.comap (↑f) S.toSubsemiring
-- Mathlib.CategoryTheory.Localization.Triangulated
/-- Given `W` is a class of morphisms in a pretriangulated category `C`, this is the condition
that `W` is compatible with the triangulation on `C`.  -/
CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.MorphismProperty C → Prop
-- Aesop.Script.UScriptToSScript
_private.Aesop.Script.UScriptToSScript.0.Aesop.Script.orderedUScriptToSScript.go : Aesop.Script.UScript →
  Std.HashMap Lean.MVarId ℕ →
    Std.HashMap Lean.MVarId ℕ →
      ℕ → ℕ → Aesop.Script.TacticState → Lean.CoreM (Aesop.Script.SScript × Aesop.Script.TacticState)
-- Mathlib.Topology.UniformSpace.Basic
Filter.HasBasis.uniformSpace_eq_bot : ∀ {α : Type ua} {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel α α} {u : UniformSpace α},
  (uniformity α).HasBasis p s → (u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y => (x, y) ∉ s i)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- If `x` specializes to `y`, then there is a natural map from the localization of `y` to the
localization of `x`.  -/
PrimeSpectrum.localizationMapOfSpecializes : {R : Type u} →
  [inst : CommSemiring R] →
    {x y : PrimeSpectrum R} → x ⤳ y → Localization.AtPrime y.asIdeal →+* Localization.AtPrime x.asIdeal
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
/-- This proof is by `inferInstance` and the argument goes through
`IsImmersion (diagonal f) → Mono (diagonal f) → IsIso (diagonal (diagonal f))`.  -/
AlgebraicGeometry.WeaklyEtale.instDiagonalScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.WeaklyEtale f],
  AlgebraicGeometry.WeaklyEtale (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.neg.injEq : ∀ (a a_1 : ℕ), (Sat.Literal.neg a = Sat.Literal.neg a_1) = (a = a_1)
-- Mathlib.Topology.Constructions.SumProd
Topology.IsOpenEmbedding.inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsOpenEmbedding Sum.inl
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- commutation with `i`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.commi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp self.φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.startsWith_prop_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String},
  s.startsWith P = true ↔ ∃ (h : s.startPos ≠ s.endPos), P (s.startPos.get h)
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_same : ∀ {α : Type u_1} (t s : Set α), t.ite s s = s
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isPushout_appTop_of_isPullback : ∀ {X Y Z P : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
  [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine Z],
  CategoryTheory.IsPullback fst snd f g →
    CategoryTheory.IsPushout (AlgebraicGeometry.Scheme.Hom.appTop f) (AlgebraicGeometry.Scheme.Hom.appTop g)
      (AlgebraicGeometry.Scheme.Hom.appTop fst) (AlgebraicGeometry.Scheme.Hom.appTop snd)
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.div_closedBall_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → s / Metric.closedBall 1 δ = Metric.cthickening δ s
-- Mathlib.Order.UpperLower.Closure
UpperSet.upperClosure_inf_sdiff : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {t : Set α},
  t ⊆ ↑s → (∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) → upperClosure t ⊓ s.sdiff t = s
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_injective : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B], Function.Injective DFunLike.coe
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.eq_C_of_natDegree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree ≤ 0 → p = Polynomial.C (p.coeff 0)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_3.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    (motive : Turing.TM0to1.Λ' Γ Λ → Sort u_3) →
      (x : Turing.TM0to1.Λ' Γ Λ) →
        ((q : Λ) → motive (Turing.TM0to1.Λ'.normal q)) →
          ((d : Turing.Dir) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q)) →
            ((a : Γ) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q)) → motive x
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- **Alias** of `LinearMap.IsAlt.eq_iff`. -/
LinearMap.IsAlt.ortho_comm : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsAlt → ∀ {x y : M₁}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Topology.Algebra.Module.Star
/-- The self-adjoint part of an element of a star module, as a continuous linear map.  -/
selfAdjointPartL : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] →
              [inst_5 : StarAddMonoid A] →
                [inst_6 : StarModule R A] →
                  [Invertible 2] →
                    [inst_8 : TopologicalSpace A] →
                      [ContinuousAdd A] → [ContinuousStar A] → [ContinuousConstSMul R A] → A →L[R] ↥(selfAdjoint A)
-- Std.Time.Zoned.RecurringRule
/-- DST abbreviation.
 -/
Std.Time.TimeZone.DaylightSavingRule.name : Std.Time.TimeZone.DaylightSavingRule → String
-- Init.Data.Order.Lemmas
Std.instReflLeOfIsPreorder : ∀ {α : Type u} [inst : LE α] [Std.IsPreorder α], Std.Refl fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mulAction : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] →
                        [inst_7 : Module R₂ M₂] →
                          {S₂ : Type u_9} →
                            [inst_8 : Monoid S₂] →
                              [inst_9 : DistribMulAction S₂ M₂] →
                                [SMulCommClass R₂ S₂ M₂] → [ContinuousConstSMul S₂ M₂] → MulAction S₂ (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Data.Finset.Grade
Finset.wcovBy_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s ⩿ insert a s
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrLeft_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D),
  e.congrLeft.functor = (CategoryTheory.Functor.whiskeringLeft D C E).obj e.inverse
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.iSup_eq_closure : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (p : ι → Submonoid M), ⨆ i, p i = Submonoid.closure (⋃ i, ↑(p i))
-- Init.Data.Nat.Fold
Nat.fold_add : ∀ {α : Type u_1} {n m : ℕ} (f : (i : ℕ) → i < n + m → α → α) (init : α),
  (n + m).fold f init = m.fold (fun i h => f (n + i) ⋯) (n.fold (fun i h => f i ⋯) init)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.IsLimit.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I}
  (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a)
  (hk :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b))
  (a : J.L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (K.ι a) = k a
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore.match_1.eq_1 : ∀ (motive : ℕ → ℕ → List Char → Sort u_1) (x : ℕ) (ds : List Char) (h_1 : (x : ℕ) → (ds : List Char) → motive 0 x ds)
  (h_2 : (fuel n : ℕ) → (ds : List Char) → motive fuel.succ n ds),
  (match 0, x, ds with
    | 0, x, ds => h_1 x ds
    | fuel.succ, n, ds => h_2 fuel n ds) =
    h_1 x ds
-- Lean.Parser.Command
Lean.Parser.Command.instance.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.abelianImageToKernel.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  S.abelianImageToKernel = CategoryTheory.Limits.kernel.lift S.g (CategoryTheory.Abelian.image.ι S.f) ⋯
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.checkMotiveResultType : Lean.Name → Array Lean.Expr → Lean.Expr → Array Lean.Expr → Lean.MetaM Unit
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Given a morphism property `P` on a category `T` and an object `X : T`, this is the
subcategory of `Over X` defined by `P` where morphisms satisfy `Q`.  -/
CategoryTheory.MorphismProperty.Over : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    CategoryTheory.MorphismProperty T → CategoryTheory.MorphismProperty T → T → Type (max v_1 u_1)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent.mk : Lean.Lsp.DocumentUri → Lean.Lsp.FileChangeType → Lean.Lsp.FileEvent
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.tsum_add : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot],
  Summable f L → Summable g L → ∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.skip?_char_eq_none_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos}, pos.skip? c = none ↔ ∀ (h : pos ≠ s.endPos), pos.get h ≠ c
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration : ∀ {X Y : SSet} (f : X ⟶ Y) [hf : HomotopicalAlgebra.Fibration f] {n : ℕ} (i : Fin (n + 2)),
  CategoryTheory.HasLiftingProperty (SSet.horn (n + 1) i).ι f
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddGrpCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections],
  Small.{u, max u v}
    ↑((F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat)).comp (CategoryTheory.forget AddMonCat)).sections
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry.induct_unfolding : ∀ {α : Type u} {β : Type v} (motive : (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.isEmpty = false → α × β → Prop),
  (∀ (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β)
      (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false),
      (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x (k, v)) →
    (∀ (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
        (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β)
        (h :
          (Std.DTreeMap.Internal.Impl.inner size k v l
                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
            false),
        (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
            false →
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) ⋯
              (Std.DTreeMap.Internal.Impl.Const.maxEntry (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              h (Std.DTreeMap.Internal.Impl.Const.maxEntry (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) ⋯)) →
      ∀ (t : Std.DTreeMap.Internal.Impl α fun x => β) (h : t.isEmpty = false),
        motive t h (Std.DTreeMap.Internal.Impl.Const.maxEntry t h)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco_continuous : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  {p a : 𝕜} [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  [inst_6 : TopologicalSpace B] {f : 𝕜 → B},
  f a = f (a + p) → ContinuousOn f (Set.Icc a (a + p)) → Continuous (AddCircle.liftIco p a f)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.triangle : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ f₃ : α → E}
  {g : α → F} {l : Filter α}, (f₁ - f₂) =o[𝕜; l] g → (f₂ - f₃) =o[𝕜; l] g → (f₁ - f₃) =o[𝕜; l] g
-- Mathlib.ModelTheory.LanguageMap
/-- The identity language homomorphism.  -/
FirstOrder.Language.LHom.id : (L : FirstOrder.Language) → L →ᴸ L
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- The continuous semilinear map obtained by applying a continuous semilinear map at a given
vector.

This is the continuous version of `LinearMap.applyₗ`.  -/
ContinuousLinearMap.apply' : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      (F : Type u_6) →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜₂ F] →
                    (σ₁₂ : 𝕜 →+* 𝕜₂) → [RingHomIsometric σ₁₂] → E →SL[σ₁₂] (E →SL[σ₁₂] F) →L[𝕜₂] F