mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Prod
_private.Mathlib.MeasureTheory.VectorMeasure.Prod.0.MeasureTheory.VectorMeasure.prodOfIsFiniteMeasureLeft.eq_1 : ∀ {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  {mY : MeasurableSpace Y} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  (μ : MeasureTheory.VectorMeasure X E) (ν : MeasureTheory.VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G)
  [inst_6 : MeasureTheory.IsFiniteMeasure μ.variation],
  MeasureTheory.VectorMeasure.prodOfIsFiniteMeasureLeft✝ μ ν B =
    { measureOf' := fun s => if MeasurableSet s then ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ] else 0, empty' := ⋯,
      not_measurable' := ⋯, m_iUnion' := ⋯ }
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instSMulCommClass : ∀ {R : Type u_1} [inst : CommRing R] (R₁ : Type u_6) (R₂ : Type u_7) [inst_1 : DistribSMul R₁ R]
  [inst_2 : DistribSMul R₂ R] [inst_3 : IsScalarTower R₁ R R] [inst_4 : IsScalarTower R₂ R R] [SMulCommClass R₁ R₂ R]
  (f : Polynomial R), SMulCommClass R₁ R₂ (AdjoinRoot f)
-- Mathlib.Algebra.Ring.Int.Defs
Int.instCharZero : CharZero ℤ
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonShowDocumentClientCapabilities.toJson : Lean.Lsp.ShowDocumentClientCapabilities → Lean.Json
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.mk : {α : Type u_1} → {f : α → α} → ℕ → IterateMulAct f
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (i : ℕ)
  (f : ContDiffMapSupportedIn E F n K),
  (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f = ‖(ContDiffMapSupportedIn.structureMapCLM 𝕜 n i) f‖
-- Mathlib.Topology.Instances.Rat
NNRat.instContinuousInv₀ : ContinuousInv₀ ℚ≥0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.mem_comap : ∀ {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₂} {x : P₁} {s : AffineSubspace k P₂},
  x ∈ AffineSubspace.comap f s ↔ f x ∈ s
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atBot` then `f * g` tends to `atBot`.  -/
Filter.Tendsto.mul_atBot' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.head_map : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (l : Turing.ListBlank Γ), (Turing.ListBlank.map f l).head = f.f l.head
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.congr : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] (e : N ≃ₗ[R] M), IsSemisimpleModule R N
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.instInhabitedRecArgInfo.default : Lean.Elab.Structural.RecArgInfo
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.eq_pow_of_mul_eq_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b c : Associates α},
  a ≠ 0 → b ≠ 0 → (∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) → ∀ {k : ℕ}, a * b = c ^ k → ∃ d, a = d ^ k
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToTop_preservesPullback_of_left : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g)
    (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.comp (AlgebraicGeometry.SheafedSpace.forget CommRingCat))
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forM_loop_eq_forM_range' : ∀ {m : Type u_1 → Type u_2} {i : ℕ} [inst : Monad m] (r : Std.Legacy.Range) (f : ℕ → m PUnit.{u_1 + 1}),
  Std.Legacy.Range.forM.loop✝ r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f
-- Mathlib.Topology.Compactness.Lindelof
instNeBotCoclosedLindelofOfNonLindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [NonLindelofSpace X], (Filter.coclosedLindelof X).NeBot
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_one : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A], 1⁺ = 1
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- The category of types has all limits.

More specifically, when `UnivLE.{v, u}`, the category `Type u` has all `v`-small limits.  -/
CategoryTheory.Limits.Types.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} (Type u)
-- Init.Core
instDecidableDite : {c : Prop} →
  {t : c → Prop} →
    {e : ¬c → Prop} →
      [dC : Decidable c] →
        [dT : (h : c) → Decidable (t h)] → [dE : (h : ¬c) → Decidable (e h)] → Decidable (if h : c then t h else e h)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.sub_app : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {U : X.Opens} (φ ψ : M ⟶ N),
  AlgebraicGeometry.Scheme.Modules.Hom.app (φ - ψ) U =
    AlgebraicGeometry.Scheme.Modules.Hom.app φ U - AlgebraicGeometry.Scheme.Modules.Hom.app ψ U
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.smulAux'.eq_1 : ∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  UpperHalfPlane.smulAux' g z = (UpperHalfPlane.σ g) (UpperHalfPlane.num g z / UpperHalfPlane.denom g z)
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.instIsAccessibleObjConst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : C),
  CategoryTheory.Functor.IsAccessible.{w, v₁, v₁, u₁, u₁} ((CategoryTheory.Functor.const C).obj A)
-- Mathlib.Order.CompleteLattice.Basic
Prod.swap_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst_1 : InfSet β] (s : Set (α × β)),
  (sInf s).swap = sInf (Prod.swap '' s)
-- Mathlib.ModelTheory.ElementaryMaps
/-- The canonical elementary embedding of an `L`-structure into any model of its elementary diagram
 -/
FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram : (L : FirstOrder.Language) →
  (M : Type u_1) →
    [inst : L.Structure M] →
      (N : Type u_5) →
        [inst_1 : L.Structure N] →
          [inst_2 : (L.withConstants M).Structure N] →
            [(L.lhomWithConstants M).IsExpansionOn N] → [N ⊨ L.elementaryDiagram M] → L.ElementaryEmbedding M N
-- Std.Data.DHashMap.Basic
/-- Returns an array of all values present in the hash map in some order.  -/
Std.DHashMap.valuesArray : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → Array β
-- Init.MetaTypes
Lean.Meta.Simp.ConfigCtx.toConfig : Lean.Meta.Simp.ConfigCtx → Lean.Meta.Simp.Config
-- Std.Http.Data.Status
Std.Http.instBEqStatus : BEq Std.Http.Status
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.map_under`. -/
IsLocalization.map_comap : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (J : Ideal S), Ideal.map (algebraMap R S) (Ideal.under R J) = J
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.instNonemptyState : ∀ {α : Type}, Nonempty (Std.CloseableChannel.Unbounded.State✝ α)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instOne.eq_1 : ∀ {α : Type u}, FreeGroup.instOne = { one := FreeGroup.mk [] }
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofRingHom_symm_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (g : S →+* R)
  (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) (a : S), (RingEquiv.ofRingHom f g h₁ h₂).symm a = g a
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesAt.hasDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 𝕜 F} {f : 𝕜 → F} {x : 𝕜},
  HasFPowerSeriesAt f p x → HasDerivAt f ((p 1) fun x => 1) x
-- Lean.Meta.Basic
Lean.Meta.State.mk : Lean.MetavarContext →
  Lean.Meta.Cache →
    Lean.FVarIdSet → Lean.PersistentArray Lean.Meta.PostponedEntry → Lean.Meta.Diagnostics → Lean.Meta.State
-- Mathlib.CategoryTheory.Sites.Limits
/-- If every cocone on a diagram of sheaves which is a colimit on the level of presheaves satisfies
the condition that the cocone point is a sheaf, then the functor from sheaves to presheaves
creates colimits of the diagram.
Note: this almost never holds in sheaf categories in general, but it does for the extensive
topology (see `Mathlib/CategoryTheory/Sites/Coherent/ExtensiveColimits.lean`).
 -/
CategoryTheory.Sheaf.createsColimitOfIsSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {K : Type z} →
            [inst_2 : CategoryTheory.Category.{z', z} K] →
              (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) →
                (∀ (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D)))
                    (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Presheaf.IsSheaf J c.pt) →
                  CategoryTheory.CreatesColimit F (CategoryTheory.sheafToPresheaf J D)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  (RingCon.mkₐ R (TensorAlgebra.ringCon R M)) (FreeAlgebra.ι R m) = (TensorAlgebra.ι R) m
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
in a second-countable space.  -/
MeasureTheory.measure_null_of_locally_null : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  [inst_2 : TopologicalSpace α] [SecondCountableTopology α] (s : Set α),
  (∀ x ∈ s, ∃ u ∈ nhdsWithin x s, μ u = 0) → μ s = 0
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.List.unattach_filter_eq_if : ∀ {α : Type u} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool},
  (List.filter f l).unattach = List.filter (fun x => if h : p x then f ⟨x, h⟩ else false) l.unattach
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.δ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Grp.forget₂Mon C) G H =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Grp.forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H))
-- Lean.ErrorExplanation
Lean.ErrorExplanation.Metadata.sinceVersion : Lean.ErrorExplanation.Metadata → String
-- Mathlib.Algebra.Module.NatInt
AddCommMonoid.nat_isScalarTower : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsScalarTower ℕ R M
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.refl_toPartialEquiv : ∀ {α : Type u_1}, (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_of_dominated_convergence_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {F' : ℕ → α → ε} {f' : α → ε} {bound' : α → ENNReal},
  MeasureTheory.HasFiniteIntegral bound' μ →
    (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a) →
      (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F' n a) Filter.atTop (nhds (f' a))) →
        MeasureTheory.HasFiniteIntegral f' μ
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx?_go_cons : ∀ {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} {i : ℕ},
  List.findIdx?.go p (x :: xs) i = if p x = true then some i else List.findIdx?.go p xs (i + 1)
-- Mathlib.CategoryTheory.Quotient
/-- In order to define a natural transformation `F ⟶ G` with `F G : Quotient r ⥤ D`, it suffices
to do so after precomposing with `Quotient.functor r`.  -/
CategoryTheory.Quotient.natTransLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (r : HomRel C) →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          {F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D} →
            ((CategoryTheory.Quotient.functor r).comp F ⟶ (CategoryTheory.Quotient.functor r).comp G) → (F ⟶ G)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsCartesian f φ'],
  (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ').hom =
    CategoryTheory.Functor.IsCartesian.map p f φ φ'
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_mono_set_of_one_le : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R}, (∀ (x : ι), 1 ≤ f x) → Monotone fun s => ∏ x ∈ s, f x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.toClass.match_1.splitter : {F : Type u_1} →
  [inst : Field F] →
    {W : WeierstrassCurve.Affine F} →
      (motive : W.Point → Sort u_2) →
        (P : W.Point) →
          (Unit → motive WeierstrassCurve.Affine.Point.zero) →
            ((x y : F) → (h : W.Nonsingular x y) → motive (WeierstrassCurve.Affine.Point.some x y h)) → motive P
-- Init.Data.String.Iterator
String.Iterator.next : String.Legacy.Iterator → String.Legacy.Iterator
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `DistribMulActionSemiHomClass F φ A B` states that `F` is a type of morphisms
preserving the additive monoid structure and equivariant with respect to `φ`.
You should extend this class when you extend `DistribMulActionSemiHom`.  -/
DistribMulActionSemiHomClass : (F : Type u_10) →
  {M : outParam (Type u_11)} →
    {N : outParam (Type u_12)} →
      outParam (M → N) →
        (A : outParam (Type u_13)) →
          (B : outParam (Type u_14)) →
            [inst : Monoid M] →
              [inst_1 : Monoid N] →
                [inst_2 : AddMonoid A] →
                  [inst_3 : AddMonoid B] → [DistribMulAction M A] → [DistribMulAction N B] → [FunLike F A B] → Prop
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.eq_span_singleton_of_surjective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Submodule R M}
  {f : R →ₗ[R] ↥s}, Function.Surjective ⇑f → s = R ∙ ↑(f 1)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (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 => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_2 size k v r
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.add_iff_right : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : AddCommGroup β] [IsTopologicalAddGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    (MeasureTheory.AEStronglyMeasurable (f + g) μ ↔ MeasureTheory.AEStronglyMeasurable g μ)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.map_C : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] (f : R →+* R') (n : ℤ),
  Polynomial.map f (Polynomial.Chebyshev.C R n) = Polynomial.Chebyshev.C R' n
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLETransOpposite : {α : Type u_1} →
  {i : LE α} →
    [Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2] →
      Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_cast_addConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑A.card * ↑(A.addConst B) = ↑(A + B).card
-- Lean.Server.Rpc.Basic
Lean.Lsp.instFromJsonRpcWireFormat.fromJson : Lean.Json → Except String Lean.Lsp.RpcWireFormat
-- Init.Data.String.TakeDrop
String.trimRight : String → String
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRight_trans : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [inst : MulOneClass M] [inst_1 : CommMonoid N₁]
  [inst_2 : CommMonoid N₂] [inst_3 : CommMonoid N₃] (e₁₂ : N₁ ≃* N₂) (e₂₃ : N₂ ≃* N₃),
  (e₁₂.trans e₂₃).monoidHomCongrRight = e₁₂.monoidHomCongrRight.trans e₂₃.monoidHomCongrRight
-- Mathlib.Algebra.Group.AddChar
AddChar.toAddMonoidHomEquiv_symm_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : A →+ Additive M) (a : A),
  (AddChar.toAddMonoidHomEquiv.symm ψ) a = Additive.toMul (ψ a)
-- Mathlib.Algebra.Group.Invertible.Defs
/-- `⅟b * ⅟a` is the inverse of `a * b`  -/
invertibleMul : {α : Type u} → [inst : Monoid α] → (a b : α) → [Invertible a] → [Invertible b] → Invertible (a * b)
-- Aesop.Rule
Aesop.defaultSafePenalty : ℤ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I),
  (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
summable_iff_nat_tsum_vanishing : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] {f : ℕ → G},
  Summable f ↔ ∀ e ∈ nhds 0, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_tail : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.tail.IsPath
-- Mathlib.RingTheory.Congruence.Hom
RingCon.coe_liftₐ : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ RingCon.ker f.toRingHom),
  ⇑(c.liftₐ f H) = ⇑(c.lift (↑f) H)
-- Lean.Parser.Command
Lean.Parser.Command.quot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Order.Compact
/-- A continuous function is bounded below on a compact set.  -/
IsCompact.bddBelow_image : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [Nonempty α] {f : β → α} {K : Set β}, IsCompact K → ContinuousOn f K → BddBelow (f '' K)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
        ⟨k, v⟩ ∈ l → ∀ {h' : k' ∈ m.insertMany l}, (m.insertMany l).get k' h' = cast ⋯ v
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_iff_of_iso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' F'' : CategoryTheory.Functor D H} (e : F' ≅ F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') (α' : F ⟶ L.comp F''),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft e.hom) = α' →
    (F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α')
-- Std.Data.DHashMap.Basic
/-- Transforms the hash map into a list of mappings in some order.  -/
Std.DHashMap.Const.toList : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → List (α × β)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.maxEntry?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntry? = t₂.maxEntry?
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.of_discrete : ∀ {α : Type u_1} [inst : MeasurableSpace α] [DiscreteMeasurableSpace α] {s : Set α}, MeasurableSet s
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.coe_toCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (A : E →SWOT[σ] F), ⇑A.toCLM = ⇑A
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.desc.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f f_1 : Z ⟶ X} (e_f : f = f_1)
  {g g_1 : Z ⟶ Y} (e_g : g = g_1) {inl inl_1 : X ⟶ P} (e_inl : inl = inl_1) {inr inr_1 : Y ⟶ P} (e_inr : inr = inr_1)
  (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h h_1 : X ⟶ W) (e_h : h = h_1) (k k_1 : Y ⟶ W) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  hP.desc h k w = ⋯.desc h_1 k_1 ⋯
-- Lean.Parser.Types
/-- Opaque parser context updateable using `adaptCacheableContextFn` and `adaptUncacheableContextFn`.  -/
Lean.Parser.ParserContext : Type