mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousWithinAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {X : Type u_6} [inst_5 : TopologicalSpace X] {f : X → E →L[𝕜] F} {g : X → E} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun x => (f x) (g x)) s x
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A generalized continued fraction is a *simple continued fraction* if all partial numerators are
equal to one.
$$
  h + \dfrac{1}
            {b_0 + \dfrac{1}
                         {b_1 + \dfrac{1}
                                      {b_2 + \dfrac{1}
                                                   {b_3 + \dots}}}}
$$
 -/
GenContFract.IsSimpContFract : {α : Type u_1} → GenContFract α → [One α] → Prop
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.desc_inl : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5}
  (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i₁ : ι₁), ac.desc x₁ x₂ (e₁.f i₁) = x₁ i₁
-- Mathlib.Topology.SeparatedMap
Topology.IsEmbedding.toPullbackDiag : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] (f : X → Y), Topology.IsEmbedding (toPullbackDiag f)
-- Mathlib.Topology.MetricSpace.Bounded
/-- A singleton has zero diameter  -/
Metric.diam_singleton : ∀ {α : Type u} {x : α} [inst : PseudoMetricSpace α], Metric.diam {x} = 0
-- Lean.Elab.Do.Control
/-- Substack at which the early-return handler was installed, if any.  -/
Lean.Elab.Do.EffectForwarder.returnBase? : Lean.Elab.Do.EffectForwarder → Option Lean.Elab.Do.ControlStack
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.u_continuous : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E],
  Continuous ExistsContDiffBumpBase.u
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.isOpen_extend_preimage' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set E},
  IsOpen s → IsOpen ((f.extend I).source ∩ ↑(f.extend I) ⁻¹' s)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go.eq_1 : ∀ {α : Type u_1} (a : List α) (x_3 : α) (xs : List α) (n : ℕ),
  List.MergeSort.Internal.splitRevAt.go✝ (x_3 :: xs) n.succ a = List.MergeSort.Internal.splitRevAt.go✝ xs n (x_3 :: a)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_zero_length : ∀ {i : ℕ} (x : BitVec 0), x.getMsbD i = false
-- Mathlib.RingTheory.Congruence.Hom
RingCon.Quotient.hom_ext_iff : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M}
  {f g : c.Quotient →+* P}, f = g ↔ f.comp c.mk' = g.comp c.mk'
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.Iterators.Types.DropWhile.instIterator.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Currying functors in three variables gives a fully faithful functor.  -/
CategoryTheory.Functor.fullyFaithfulCurry₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] → CategoryTheory.Functor.curry₃.FullyFaithful
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.stepRet.match_1.eq_5 : ∀ (motive : Turing.ToPartrec.Cont → List ℕ → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (v : List ℕ) (h_1 : (v : List ℕ) → motive Turing.ToPartrec.Cont.halt v)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₁ fs as k) v)
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.cons₂ ns k) v)
  (h_4 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.comp f k) v)
  (h_5 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cont.fix f k) v),
  (match Turing.ToPartrec.Cont.fix f k, v with
    | Turing.ToPartrec.Cont.halt, v => h_1 v
    | Turing.ToPartrec.Cont.cons₁ fs as k, v => h_2 fs as k v
    | Turing.ToPartrec.Cont.cons₂ ns k, v => h_3 ns k v
    | Turing.ToPartrec.Cont.comp f k, v => h_4 f k v
    | Turing.ToPartrec.Cont.fix f k, v => h_5 f k v) =
    h_5 f k v
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (k : ℤ),
  x = Lean.Grind.CommRing.Expr.num k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_1 k
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.mapsTo_Ioi : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictMonoOn f (Set.Ici a) → Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
-- Mathlib.Data.Finset.Empty
/-- **Alias** of the reverse direction of `Finset.nonempty_coe_sort`. -/
Finset.Nonempty.coe_sort : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → Nonempty ↥s
-- Lean.Data.Lsp.Extra
Lean.Lsp.LineRange.mk.sizeOf_spec : ∀ (start «end» : ℕ), sizeOf { start := start, «end» := «end» } = 1 + sizeOf start + sizeOf «end»
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.function.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.function = 1
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Given a functor `F` and an equivalence of categories `e` such that `e.inverse` and `e.functor ⋙ F`
are monoidal functors, `F` is monoidal as well.
 -/
CategoryTheory.Equivalence.monoidalOfPrecompFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (e : C ≌ D) →
                    (F : CategoryTheory.Functor D E) →
                      {F' : CategoryTheory.Functor C E} →
                        (e.functor.comp F ≅ F') → [e.inverse.Monoidal] → [F'.Monoidal] → F.Monoidal
-- Mathlib.GroupTheory.Congruence.Defs
/-- Sometimes, a group is defined as a quotient of a monoid by a congruence relation.
Usually, the inverse operation is defined as `Setoid.map f _` for some `f`.
This lemma allows to avoid code duplication in the definition of the inverse operation:
instead of proving both `∀ x y, c x y → c (f x) (f y)` (to define the operation)
and `∀ x, c (f x * x) 1` (to prove the group laws), one can only prove the latter.  -/
Con.map_of_mul_left_rel_one : ∀ {M : Type u_1} [inst : Monoid M] (c : Con M) (f : M → M),
  (∀ (x : M), c (f x * x) 1) → ∀ {x y : M}, c x y → c (f x) (f y)
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_1.splitter : (n : ℕ) → (motive : n + 1 ≤ 0 → Sort u_1) → (a : n + 1 ≤ 0) → motive a
-- Init.Data.Float.Model.Float
Float.Model.instDecidableLT : DecidableLT Float.Model
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.condDistrib_ae_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F},
  AEMeasurable Y μ →
    MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
      ∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ,
        MeasureTheory.Integrable (fun ω => f (b, ω)) ((ProbabilityTheory.condDistrib Y X μ) b)
-- Std.Http.Data.URI.Basic
/-- Sets the host as an IPv6 address.
 -/
Std.Http.URI.Builder.setHostIPv6 : Std.Http.URI.Builder → Std.Net.IPv6Addr → Std.Http.URI.Builder
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.map_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), e 0 = 0
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.contract_delete_isMinor : ∀ {α : Type u_1} (M : Matroid α) (C D : Set α), (M.contract C).delete D ≤m M
-- Std.Time.Format.Basic
/-- The format of date and time string.
 -/
Std.Time.FormatString : Type
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_algebraMap : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (x : Polynomial K),
  { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) x } =
    (algebraMap (Polynomial K) (RatFunc K)) x
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.integralAgainstBilinCLM.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F₁]
  [inst_13 : NormedSpace ℝ F₃] [inst_14 : IsScalarTower ℝ 𝕜 F₃] (B B_1 : F₁ →L[𝕜] F₂ →L[𝕜] F₃),
  B = B_1 →
    ∀ (μ μ_1 : MeasureTheory.Measure E),
      μ = μ_1 →
        ∀ (φ φ_1 : E → F₂),
          φ = φ_1 → TestFunction.integralAgainstBilinCLM B μ φ = TestFunction.integralAgainstBilinCLM B_1 μ_1 φ_1
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- According to `UpwardEnumerable.LE`, `a` is less than or equal to `b` if `b` is `a` or a transitive
successor of `a`.
 -/
Std.PRange.UpwardEnumerable.LE : {α : Type u} → [Std.PRange.UpwardEnumerable α] → α → α → Prop
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.asq_pos : ∀ {a : ℕ}, 1 < a → 0 < a * a
-- Std.Sync.CancellationContext
Std.CancellationContext.State.mk.injEq : ∀ (tokens : Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare) (id : UInt64)
  (tokens_1 : Std.TreeMap UInt64 (Std.CancellationToken × Array UInt64) compare) (id_1 : UInt64),
  ({ tokens := tokens, id := id } = { tokens := tokens_1, id := id_1 }) = (tokens = tokens_1 ∧ id = id_1)
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The `LFunction` of the function `x ↦ e (j * x)`, where `e : ZMod N → ℂ` is the standard additive
character, agrees with `expZeta (j / N)` on `1 < re s`. Private since it is a stepping-stone to
the more general result `LFunction_stdAddChar_eq_expZeta` below.
 -/
_private.Mathlib.NumberTheory.LSeries.ZMod.0.ZMod.LFunction_stdAddChar_eq_expZeta_of_one_lt_re : ∀ {N : ℕ} [inst : NeZero N] (j : ZMod N) {s : ℂ},
  1 < s.re → ZMod.LFunction (fun k => ZMod.stdAddChar (j * k)) s = HurwitzZeta.expZeta (ZMod.toAddCircle j) s
-- Mathlib.Geometry.Manifold.Submersion
/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
Additionally, we demand that `f` map `φ.source` into `ψ.source`.

NB. We don't know the particular atlasses used for `M` and `N`, so asking for `φ` and `ψ` to be
in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.

This definition has a fixed parameter `F`, which is a choice of complement of `E''` in `E`:
being an submersion at `x` includes a choice of linear isomorphism between `E'' × F` and `E`.
While the particular choice of complement is often not important, choosing a complement is useful
in some settings, such as proving that embedded submanifolds are locally given either by an
immersion or a submersion.
Unless you have a particular reason, prefer to use `IsSubmersionAt` instead.
 -/
Manifold.IsSubmersionAtOfComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    (F : Type u_5) →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              ModelWithCorners 𝕜 E H →
                                ModelWithCorners 𝕜 E'' G →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst : TopologicalSpace M] →
                                        [ChartedSpace H M] →
                                          [inst : TopologicalSpace N] →
                                            [ChartedSpace G N] → WithTop ℕ∞ → (M → N) → M → Prop
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.sq_nonneg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, 0 ≤ a ^ 2
-- Mathlib.Order.Interval.Set.UnorderedInterval
AntitoneOn.image_uIcc_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  AntitoneOn f (Set.uIcc a b) → f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The inf of two affine subspaces, coerced to a set, is the intersection of the two sets of
points.  -/
AffineSubspace.coe_inf : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), ↑s₁ ⊓ ↑s₂ = ↑s₁ ∩ ↑s₂
-- Init.Data.RArray
Lean.RArray.leaf.inj : ∀ {α : Type u} {a a_1 : α}, Lean.RArray.leaf a = Lean.RArray.leaf a_1 → a = a_1
-- Mathlib.RingTheory.Ideal.Colon
Submodule.mem_colon' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {S : Set M} {r : R}, r ∈ N.colon S ↔ S ⊆ ↑(Submodule.comap (r • LinearMap.id) N)
-- Mathlib.Order.InitialSeg
PrincipalSeg.transInitial_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  (f : PrincipalSeg r s) (g : InitialSeg s t) (a : α), (f.transInitial g).toRelEmbedding a = g (f.toRelEmbedding a)
-- Lean.Server.Requests
Lean.Server.RequestHandler.mk.sizeOf_spec : ∀ (fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
  (handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)),
  sizeOf { fileSource := fileSource, handle := handle } = 1
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ioo' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Ioo (f b) (f a) ⊆ f '' Set.Ioo a b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.exists_nat_pow_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [Finite α], f.SameCycle x y → ∃ i, (f ^ i) x = y
-- Aesop.Search.ExpandSafePrefix
_private.Aesop.Search.ExpandSafePrefix.0.Aesop.expandSafePrefixMVarCluster : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.MVarClusterRef → Aesop.SafeExpansionM Q Unit
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_iff_le_maximalRealSubfield : ∀ {K : Type u_2} [inst : Field K] [inst_1 : CharZero K] [Algebra.IsAlgebraic ℚ K] {E : Subfield K},
  NumberField.IsTotallyReal ↥E ↔ E ≤ NumberField.maximalRealSubfield K
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedGroup.tendstoUniformlyOn_one : ∀ {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [inst : SeminormedGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι},
  TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.Raw.ofList l cmp).get? k = none
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
the arrow attached to the cosimplicial object is the one obtained by evaluation at the unique arrow
`star ⟶ of [0]`.  -/
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.comp
        CategoryTheory.SimplicialObject.Augmented.toArrow ≅
      (CategoryTheory.Functor.mapArrowFunctor AugmentedSimplexCategoryᵒᵖ C).comp
        ((CategoryTheory.evaluation (CategoryTheory.Arrow AugmentedSimplexCategoryᵒᵖ) (CategoryTheory.Arrow C)).obj
          (CategoryTheory.Arrow.mk (CategoryTheory.WithInitial.homTo { len := 0 }).op))
-- Mathlib.CategoryTheory.Galois.Examples
/-- The category of finite `G`-sets is a `PreGaloisCategory`.  -/
CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat : ∀ (G : Type u) [inst : Group G], CategoryTheory.PreGaloisCategory (Action FintypeCat G)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.isoMk_inv_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber),
  (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.fiber =
    CategoryTheory.CategoryStruct.comp ((F.map e₁.inv).toFunctor.map e₂.inv) (CategoryTheory.eqToHom ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Auxiliary lemma for `biproduct.uniqueUpToIso`.  -/
CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit),
  (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).hom =
    CategoryTheory.Limits.biproduct.lift b.π
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.one_tmul_mul_elem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.FormallyUnramified R S] [inst_4 : Algebra.EssFiniteType R S] (s : S),
  1 ⊗ₜ[R] s * Algebra.FormallyUnramified.elem R S = s ⊗ₜ[R] 1 * Algebra.FormallyUnramified.elem R S
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdComm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  (x : WithLp p (α × β)), (LinearIsometryEquiv.withLpProdComm p 𝕜 α β) x = WithLp.toLp p (x.snd, x.fst)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.mul_iInter_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Mul α] (s : Set α) (t : ι → Set α), s * ⋂ i, t i ⊆ ⋂ i, s * t i
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.mono_pushout_of_mono_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.Order.Interval.Finset.Basic
Finset.mem_uIcc_of_ge : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, b ≤ x → x ≤ a → x ∈ Finset.uIcc a b
-- Mathlib.Data.Finset.Lattice.Fold
/-- To rewrite from right to left, use `Finset.sup'_comp_eq_map`.  -/
Finset.sup'_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
  (hs : (Finset.map f s).Nonempty), (Finset.map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.snd_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (self : A × B), (ContinuousMonoidHom.snd A B) self = self.2