mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Linter.UnnecessarySeqFocus
Batteries.Linter.UnnecessarySeqFocus.Entry.mk.inj : ∀ {stx : Lean.Syntax} {used : Bool} {stx_1 : Lean.Syntax} {used_1 : Bool},
  { stx := stx, used := used } = { stx := stx_1, used := used_1 } → stx = stx_1 ∧ used = used_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.maxKey?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.CategoryTheory.Elements
/-- Natural transformations are mapped to functors between categories of elements.  -/
CategoryTheory.NatTrans.mapElements : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → (F ⟶ G) → CategoryTheory.Functor F.Elements G.Elements
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Unfold all of the auxiliary functions that were inserted as unfold boundaries.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.unfoldInsertions : Lean.Expr → Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.CoreM Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Bool.instMeasurableSpace : MeasurableSpace Bool
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the kernel condition for `ι`  -/
CategoryTheory.ShortComplex.RightHomologyData.wι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData),
  CategoryTheory.CategoryStruct.comp self.ι (self.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBy_isTorsion_nonZeroDivisor : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ∀ a ∈ nonZeroDivisors R, Module.IsTorsion R ↥(Submodule.torsionBy R M a)
-- Mathlib.CategoryTheory.Opposites
/-- If `f.op` is an isomorphism `f` must be too.
(This cannot be an instance as it would immediately loop!)
 -/
CategoryTheory.isIso_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f.op],
  CategoryTheory.IsIso f
-- Init.Data.Float.Float32
/-- Converts a 32-bit floating-point number to a 64-bit floating-point number.

This function does not reduce in the kernel.
 -/
Float32.toFloat : Float32 → Float
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_zpow' : ∀ (x : ENNReal) (n : ℤ), x⁻¹ ^ n = x ^ (-n)
-- Mathlib.Probability.Independence.ZeroOne
/-- **Kolmogorov's 0-1 law** : any event in the tail σ-algebra of an independent sequence of
sub-σ-algebras has probability 0 or 1.
The tail σ-algebra `limsup s atTop` is the same as `⋂ n, ⋃ i ≥ n, s i`.  -/
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) → ProbabilityTheory.iIndep s μ → ∀ {t : Set Ω}, MeasurableSet t → μ t = 0 ∨ μ t = 1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function has a limit on its left within a set.  -/
BoundedVariationOn.exists_tendsto_left : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∀ (x : α), ∃ l, Filter.Tendsto f (nhdsWithin x (s ∩ Set.Iio x)) (nhds l)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- A non-unital subalgebra over a ring is also a `Subring`.  -/
NonUnitalSubalgebra.toNonUnitalSubring : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalNonAssocRing A] → [inst_2 : Module R A] → NonUnitalSubalgebra R A → NonUnitalSubring A
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.comapRight_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : γ → β} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) (a : α)
  {t : Set γ}, MeasurableSet t → ((κ.comapRight hf) a) t = (κ a) (f '' t)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cycles₁IsoOfIsTrivial_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial]
  (x : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).hom) x = ↑x
-- Mathlib.NumberTheory.RamificationInertia.Inertia
_private.Mathlib.NumberTheory.RamificationInertia.Inertia.0.Ideal.termF : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.faceSingletonComplIso_inv_ι : ∀ {n : ℕ} (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso i).inv (SSet.boundary.ι i) =
    SSet.boundary.faceι i
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.c₂_nonneg : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)], 0 ≤ NumberField.house.c₂✝ K
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.lhom_ext' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R N] [inst_4 : Module R S] ⦃f g : AddMonoidAlgebra S M →ₗ[R] N⦄,
  (∀ (x : M), f ∘ₗ AddMonoidAlgebra.lsingle x = g ∘ₗ AddMonoidAlgebra.lsingle x) → f = g
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.not_coe_le_zero : ∀ {α : Type u_1} [inst : LE α] (a : α), ¬↑a ≤ 0
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the constant sequence `1` equals the Riemann Zeta Function on its
domain of convergence `1 < re s`.  -/
LSeries_one_eq_riemannZeta : ∀ {s : ℂ}, 1 < s.re → LSeries 1 s = riemannZeta s
-- Init.Data.UInt.Bitwise
UInt16.ofFin_rev : ∀ (a : Fin UInt16.size), UInt16.ofFin a.rev = ~~~UInt16.ofFin a
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Iso.prod_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T), (f.prod g).hom = CategoryTheory.Prod.mkHom f.hom g.hom
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- `LinearMap.finiteRange` is the submodule of `V →ₗ[K] W` consisting of linear maps satisfying
`LinearMap.HasNoetherianRange`. We allow ourself this slightly abusive name because the set of
linear maps satisfying `LinearMap.HasFiniteRange` is only a submodule over a noetherian ring,
in which case the two notions agree.  -/
LinearMap.finiteRange : (K : Type u_1) →
  (V : Type u_2) →
    (V₂ : Type u_4) →
      [inst : CommRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module K V] → [inst_3 : AddCommGroup V₂] → [inst_4 : Module K V₂] → Submodule K (V →ₗ[K] V₂)
-- Mathlib.Logic.Equiv.Defs
Equiv.psigmaEquivSigmaPLift_symm_apply : ∀ {α : Sort u_2} (β : α → Sort u_1) (a : (i : PLift α) × PLift (β i.down)),
  (Equiv.psigmaEquivSigmaPLift β).symm a = ⟨a.fst.down, a.snd.down⟩
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.of_forall_exists_mul_mem_range : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Algebra.QuasiFinite R S] (f : S →ₐ[R] T),
  (∀ (x : T), ∃ s, IsUnit (f s) ∧ x * f s ∈ f.range) → Algebra.QuasiFinite R T
-- Init.Data.String.Basic
String.Slice.Pos.isUTF8FirstByte_byte : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos}, (pos.byte h).IsUTF8FirstByte
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- If `π` is a prepartition of `I`, then `π.compl` is a prepartition of `I`
such that `π.compl.iUnion = I \ π.iUnion`.  -/
BoxIntegral.Prepartition.compl : {ι : Type u_1} → {I : BoxIntegral.Box ι} → [Finite ι] → BoxIntegral.Prepartition I → BoxIntegral.Prepartition I
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.findSomeRevM?.find.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m (Option β)) (as : Array α) (i : ℕ)
  (a : i ≤ as.size),
  Array.findSomeRevM?.find✝ f as i a =
    match i, a with
    | 0, x => pure none
    | i.succ, h =>
      have this := ⋯;
      do
      let r ← f as[i]
      match r with
        | some val => pure r
        | none =>
          have this := ⋯;
          Array.findSomeRevM?.find✝ f as i this
-- Init.Data.Sum.Lemmas
Sum.isRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (val : α), (Sum.inl val).isRight = false
-- Init.Data.List.Zip
List.unzip_fst : ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip.1 = List.map Prod.fst l
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.measurable_fun_prod : ∀ {M : Type u_2} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} (s : Multiset (α → M)),
  (∀ f ∈ s, Measurable f) → Measurable fun x => (Multiset.map (fun f => f x) s).prod
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.norm_const_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E),
  ‖(MeasureTheory.Lp.const p μ) c‖ ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
-- Mathlib.Topology.Sheaves.Skyscraper
/-- If `y ∈ closure {p₀}`, then the stalk of `skyscraperPresheaf p₀ A` at `y` is `A`.
 -/
skyscraperPresheafStalkOfSpecializes : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] →
                {y : ↑X} → p₀ ⤳ y → ((skyscraperPresheaf p₀ A).stalk y ≅ A)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.indep_generateFrom_le : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Preorder ι]
  {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.iIndepSet s μ →
      ∀ (i : ι) {k : ι},
        i < k →
          ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s k})
            (MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) μ
-- Mathlib.Geometry.Manifold.Bordism
/-- A smooth manifold induces a singular manifold on the one-point space.  -/
SingularManifold.toPUnit : {k : WithTop ℕ∞} →
  {E : Type u_4} →
    {H : Type u_5} →
      (M : Type u_6) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : FiniteDimensional ℝ E] →
              [inst_3 : TopologicalSpace H] →
                (I : ModelWithCorners ℝ E H) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      [IsManifold I k M] →
                        [CompactSpace M] → [BoundarylessManifold I M] → SingularManifold PUnit.{u_9 + 1} k I
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.eraseList.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (toErase : List α),
  Std.Internal.List.eraseList l toErase =
    match toErase with
    | [] => l
    | k :: toErase => Std.Internal.List.eraseList (Std.Internal.List.eraseKey k l) toErase
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
isBigO_riemannZeta_sub_one_div : ∀ {F : Type u_1} [inst : Norm F] [inst_1 : One F] [NormOneClass F],
  (fun s => riemannZeta s - 1 / (s - 1)) =O[nhds 1] fun x => 1
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instTop : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Top (LieSubalgebra R L)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_smul : ∀ {𝕜 : 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] (r : 𝕜)
  (X : LeftInvariantDerivation I G), ⇑(r • X) = r • ⇑X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.hashCode : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → UInt64
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_mk' : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (p : P₁) (direction : Submodule k V₁),
  AffineSubspace.map f (AffineSubspace.mk' p direction) = AffineSubspace.mk' (f p) (Submodule.map f.linear direction)
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement : Type
-- Mathlib.Data.Nat.ChineseRemainder
_private.Mathlib.Data.Nat.ChineseRemainder.0.Nat.chineseRemainderOfList.match_1.splitter : {ι : Type u_1} →
  (s : ι → ℕ) →
    (motive : (x : List ι) → List.Pairwise (Function.onFun Nat.Coprime s) x → Sort u_2) →
      (x : List ι) →
        (x_1 : List.Pairwise (Function.onFun Nat.Coprime s) x) →
          ((x : List.Pairwise (Function.onFun Nat.Coprime s) []) → motive [] x) →
            ((i : ι) →
                (l : List ι) → (co : List.Pairwise (Function.onFun Nat.Coprime s) (i :: l)) → motive (i :: l) co) →
              motive x x_1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- A morphism in `P.Comma L R Q W` is a morphism in `Comma L R` where the left
hom satisfies `Q` and the right one satisfies `W`.  -/
CategoryTheory.MorphismProperty.Comma.Hom : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      CategoryTheory.MorphismProperty.Comma L R P Q W →
                        CategoryTheory.MorphismProperty.Comma L R P Q W → Type (max v_1 v_2)
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_isoOfHom_inv : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C} (f : Y ⟶ X) (hf : W f),
  (CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.Localization.isoOfHom L₁ W f hf).inv =
    (CategoryTheory.Localization.isoOfHom L₂ W f hf).inv
-- Lean.DocString.Parser
Lean.Doc.Parser.UnorderedListType.plus.sizeOf_spec : sizeOf Lean.Doc.Parser.UnorderedListType.plus = 1
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.congr_simp : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f f_1 : Set X → ENNReal) (e_f : f = f_1)
  (hf : MeasureTheory.IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0),
  MeasureTheory.preVariation f hf hf' = MeasureTheory.preVariation f_1 ⋯ ⋯
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedSearchState : Inhabited Lean.Meta.Grind.EMatch.SearchState
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  ↑(TensorProduct.tensorQuotEquivQuotSMul M I) ∘ₗ LinearMap.lTensor M (Submodule.mkQ I) =
    (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.rid R M)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h)
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.compCreatesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {E : Type u₃} →
                [ℰ : CategoryTheory.Category.{v₃, u₃} E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor D E) →
                      [CategoryTheory.CreatesLimit K F] →
                        [CategoryTheory.CreatesLimit (K.comp F) G] → CategoryTheory.CreatesLimit K (F.comp G)
-- Lean.Server.Requests
/-- Checks whether `r` contains `hoverPos`, taking into account EOF according to `text`.  -/
Lean.FileMap.rangeContainsHoverPos : Lean.FileMap → Lean.Syntax.Range → String.Pos.Raw → optParam Bool false → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multicospan associated to `I : MulticospanIndex`.  -/
CategoryTheory.Limits.MulticospanIndex.multicospan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      CategoryTheory.Limits.MulticospanIndex J C → CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instNatCast : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → NatCast (CauSeq β abv)
-- Mathlib.Data.Set.Function
Set.MapsTo.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
  Set.MapsTo f₁ s t → Set.EqOn f₁ f₂ s → Set.MapsTo f₂ s t
-- Mathlib.Data.ZMod.Basic
ZMod.val_one : ∀ (n : ℕ) [Fact (1 < n)], ZMod.val 1 = 1
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.expandDiv : Lean.Meta.Simp.Simproc
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- A variant of `spread_out_unique_of_isGermInjective`
whose condition is an equality of scheme morphisms instead of ring homomorphisms.
 -/
AlgebraicGeometry.spread_out_unique_of_isGermInjective' : ∀ {X Y : AlgebraicGeometry.Scheme} {x : ↥X} [X.IsGermInjectiveAt x] (f g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) g →
    ∃ U, x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ι f = CategoryTheory.CategoryStruct.comp U.ι g
-- Mathlib.RingTheory.LocalRing.Defs
/-- in a local ring `R`, if `a + b = 1`, then either `a` is a unit or `b` is a unit. In another
word, for every `a : R`, either `a` is a unit or `1 - a` is a unit.  -/
IsLocalRing.isUnit_or_isUnit_of_add_one : ∀ {R : Type u_1} {inst : Semiring R} [self : IsLocalRing R] {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Compl.adjDecidable : (V : Type u) → (G : SimpleGraph V) → [DecidableRel G.Adj] → [DecidableEq V] → DecidableRel Gᶜ.Adj
-- Std.Http.Protocol.H1
/-- Parses next chunk-size line in chunked mode and transitions to chunk-data state.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseChunkSizeBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_eq_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m.get a h = m[a]
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Construct the lifted cone in `Coalgebra T` which will be limiting.  -/
CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          {D : CategoryTheory.Functor J T.Coalgebra} →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) →
              CategoryTheory.Limits.IsLimit c →
                [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] →
                  [CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] →
                    CategoryTheory.Limits.Cone D
-- Lean.Parser.Basic
Lean.Parser.hexDigitFn : Lean.Parser.ParserFn
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.map_comp_apply : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} {Y : Type u_3} {Z : Type u_4}
  [inst_2 : Fintype X] [inst_3 : Fintype Y] [inst_4 : Fintype Z] [inst_5 : IsOrderedRing S] (f : X → Y) (g : Y → Z)
  (x : ↑(stdSimplex S X)), stdSimplex.map g (stdSimplex.map f x) = stdSimplex.map (g ∘ f) x
-- Init.Data.Dyadic.Basic
Dyadic.ofIntWithPrec.eq_1 : ∀ (i prec : ℤ),
  Dyadic.ofIntWithPrec i prec =
    if h : i = 0 then Dyadic.zero else Dyadic.ofOdd (i >>> i.trailingZeros) (prec - ↑i.trailingZeros) ⋯
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colim_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.colim.obj F = CategoryTheory.Limits.colimit F
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRiiSlice : {α : Type u} →
  {β : Type v} →
    Std.Rii.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RiiSlice α β)
-- Mathlib.CategoryTheory.GuitartExact.Opposite
/-- Auxiliary definition for `structuredArrowRightwardsOpEquivalence`.  -/
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₃ : C₃ᵒᵖ} →
                            {X₂ : C₂ᵒᵖ} →
                              (g : B.op.obj X₃ ⟶ R.op.obj X₂) →
                                CategoryTheory.Functor (w.CostructuredArrowDownwards g.unop)
                                  (w.op.StructuredArrowRightwards g)ᵒᵖ
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- `Path.map` respects subintervals of paths.  -/
SSet.Path.map_interval : ∀ {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (j l : ℕ) (h : j + l ≤ n),
  (f.map σ).interval j l h = (f.interval j l h).map σ
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.exists_mem_sup : ∀ {C : Type u_2} [inst : AddCommGroup C] {s t : AddSubgroup C} {P : C → Prop},
  (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ + x₂)