mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
IsContMDiffRiemannianBundle.exists_contMDiff : ∀ {EB : Type u_1} {inst : NormedAddCommGroup EB} {inst_1 : NormedSpace ℝ EB} {HB : Type u_2}
  {inst_2 : TopologicalSpace HB} {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  {inst_3 : TopologicalSpace B} {inst_4 : ChartedSpace HB B} {F : Type u_4} {inst_5 : NormedAddCommGroup F}
  {inst_6 : NormedSpace ℝ F} {E : B → Type u_5} {inst_7 : TopologicalSpace (Bundle.TotalSpace F E)}
  {inst_8 : (x : B) → NormedAddCommGroup (E x)} {inst_9 : (x : B) → InnerProductSpace ℝ (E x)}
  {inst_10 : FiberBundle F E} {inst_11 : VectorBundle ℝ F E} [self : IsContMDiffRiemannianBundle IB n F E],
  ∃ g,
    (ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, g b⟩) ∧
      ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w
-- Mathlib.AlgebraicGeometry.Restrict
/-- The stalk map of `f.resLE U V` at `x : V` is the stalk map of `f` at `x`.  -/
AlgebraicGeometry.Scheme.Hom.resLEStalkMap : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    {U : Y.Opens} →
      {V : X.Opens} →
        (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) →
          (x : ↥V) →
            CategoryTheory.Arrow.mk
                (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Scheme.Hom.resLE f U V e) x) ≅
              CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f ↑x)
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.trivialCofibrations_over_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C],
  HomotopicalAlgebra.trivialCofibrations (CategoryTheory.Over S) = (HomotopicalAlgebra.trivialCofibrations C).over
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion.eq_1 : ∀ (h : ℝ) (f : UpperHalfPlane → ℂ),
  UpperHalfPlane.qExpansion h f =
    PowerSeries.mk fun m => (↑m.factorial)⁻¹ * iteratedDeriv m (UpperHalfPlane.cuspFunction h f) 0
-- Mathlib.Analysis.Meromorphic.Order
/-- The order is additive in products of meromorphic functions.
 -/
meromorphicOrderAt_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {ι : Type u_5} {s : Finset ι} {f : ι → 𝕜 → 𝕜'},
  (∀ i ∈ s, MeromorphicAt (f i) x) → meromorphicOrderAt (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instFunLikeContMDiffMonoidMorphism : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {n : WithTop ℕ∞} →
      {H : Type u_2} →
        [inst_1 : TopologicalSpace H] →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {I : ModelWithCorners 𝕜 E H} →
                  {G : Type u_4} →
                    [inst_4 : Monoid G] →
                      [inst_5 : TopologicalSpace G] →
                        [inst_6 : ChartedSpace H G] →
                          {H' : Type u_5} →
                            [inst_7 : TopologicalSpace H'] →
                              {E' : Type u_6} →
                                [inst_8 : NormedAddCommGroup E'] →
                                  [inst_9 : NormedSpace 𝕜 E'] →
                                    {I' : ModelWithCorners 𝕜 E' H'} →
                                      {G' : Type u_7} →
                                        [inst_10 : Monoid G'] →
                                          [inst_11 : TopologicalSpace G'] →
                                            [inst_12 : ChartedSpace H' G'] →
                                              FunLike (ContMDiffMonoidMorphism I I' n G G') G G'
-- Init.Data.Nat.Dvd
Nat.dvd_add_iff_left : ∀ {k m n : ℕ}, k ∣ n → (k ∣ m ↔ k ∣ m + n)
-- Std.Time.Internal.Bounded
/-- Convert a `Int` to a `Bounded` if it checks.
 -/
Std.Time.Internal.Bounded.ofInt? : {rel : ℤ → ℤ → Prop} → {lo hi : ℤ} → [DecidableRel rel] → ℤ → Option (Std.Time.Internal.Bounded rel lo hi)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF.induct_unfolding : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering → Prop),
  motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit Ordering.eq →
    (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
        motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m) Ordering.gt) →
      (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
          motive (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit Ordering.lt) →
        (∀ (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
            (m₂ : Lean.Grind.CommRing.Mon),
            (pw₁.x == pw₂.x) = true →
              motive m₁ m₂ (m₁.revlexWF m₂) →
                motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                  ((m₁.revlexWF m₂).then (Lean.Grind.CommRing.powerRevlex pw₁.k pw₂.k))) →
          (∀ (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
              (m₂ : Lean.Grind.CommRing.Mon),
              (pw₁.x == pw₂.x) = false →
                Nat.blt pw₁.x pw₂.x = true →
                  motive m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂) (m₁.revlexWF (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
                    motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                      ((m₁.revlexWF (Lean.Grind.CommRing.Mon.mult pw₂ m₂)).then Ordering.lt)) →
            (∀ (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
                (m₂ : Lean.Grind.CommRing.Mon),
                (pw₁.x == pw₂.x) = false →
                  Nat.blt pw₁.x pw₂.x = false →
                    motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂
                        ((Lean.Grind.CommRing.Mon.mult pw₁ m₁).revlexWF m₂) →
                      motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                        (((Lean.Grind.CommRing.Mon.mult pw₁ m₁).revlexWF m₂).then Ordering.gt)) →
              ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), motive m₁ m₂ (m₁.revlexWF m₂)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Initial application used to start E-matching  -/
Lean.Meta.Grind.EMatch.Context.initApp : Lean.Meta.Grind.EMatch.Context → Lean.Expr
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- The equivalence of categories `(C ⥤ D) ≌ (Karoubi C ⥤ Karoubi D)` when `D`
is idempotent complete.  -/
CategoryTheory.Idempotents.karoubiUniversal₂ : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.IsIdempotentComplete D] →
          CategoryTheory.Functor C D ≌
            CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_top : ∀ (R : Type u) [inst : CommSemiring R], ⊤.radical = ⊤
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.normedCommGroup : {E : Type u_1} →
  [inst : NormedCommGroup E] →
    {S : Type u_2} → [inst_1 : SetLike S E] → [SubgroupClass S E] → (s : S) → NormedCommGroup ↥s
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- The relative norm `Ideal.relNorm R (I : Ideal S)`, where `R` and `S` are Dedekind domains,
and `S` is an extension of `R` that is finite and free as a module.  -/
Ideal.relNorm : (R : Type u_1) →
  [inst : CommRing R] →
    [IsDomain R] →
      {S : Type u_3} →
        [inst_2 : CommRing S] →
          [IsDomain S] →
            [IsIntegrallyClosed R] →
              [IsIntegrallyClosed S] →
                [inst_6 : Algebra R S] →
                  [Module.Finite R S] →
                    [Module.IsTorsionFree R S] → [IsDedekindDomain R] → [IsDedekindDomain S] → Ideal S →*₀ Ideal R
-- Init.Sym.Lemmas
Lean.Sym.cond_cond_eq_false : ∀ {α : Sort u} (c : Bool) (a b : α), c = false → (bif c then a else b) = b
-- Mathlib.Algebra.Category.AlgCat.Symmetric
AlgCat.instBraidedModuleCatForget₂AlgHomCarrierLinearMapIdCarrier : {R : Type u} → [inst : CommRing R] → (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).Braided
-- Mathlib.Topology.ExtremallyDisconnected
/-- A (pre-)connected, extremally disconnected space is preirreducible.  -/
ExtremallyDisconnected.toPreirreducibleSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [h : ExtremallyDisconnected X] [h' : PreconnectedSpace X],
  PreirreducibleSpace X
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  [CategoryTheory.Limits.HasLimitsOfShape C E], CategoryTheory.Limits.HasLimitsOfShape D E
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, to show that `F` creates the limit for `K` it suffices to show that a
limit point is in the essential image of `F`.
 -/
CategoryTheory.createsLimitOfFullyFaithfulOfIso' : {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} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    {l : CategoryTheory.Limits.Cone (K.comp F)} →
                      CategoryTheory.Limits.IsLimit l → (X : C) → (F.obj X ≅ l.pt) → CategoryTheory.CreatesLimit K F
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_utf8EncodeChar_eq_oneMore : ∀ {c : Char},
  c.utf8Size = 2 →
    ByteArray.utf8DecodeChar?.parseFirstByte (String.utf8EncodeChar c)[0] = ByteArray.utf8DecodeChar?.FirstByte.oneMore
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₂_of_arrow : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2},
  CategoryTheory.Arrow.mk (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝) =
      CategoryTheory.Arrow.mk (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝) →
    CategoryTheory.Arrow.mk (f.map' 1 2 _proof_246✝ _proof_247✝) =
        CategoryTheory.Arrow.mk (g.map' 1 2 _proof_246✝ _proof_247✝) →
      f = g
-- Mathlib.Probability.Kernel.Category.SFinKer
/-- The property that the morphism satisfies.  -/
SFinKer.Hom.property : ∀ {X Y : SFinKer} (self : X.Hom Y), ProbabilityTheory.IsSFiniteKernel self.hom
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.tprod_equiv : ∀ {R ι : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : Equiv.Perm ι) (f : ι → M), (⨂ₛ[R] (i : ι), f (e i)) = ⨂ₛ[R] (i : ι), f i
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.consRecOn_empty : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {motive : Monoid.CoprodI.Word M → Sort u_4}
  (h_empty : motive Monoid.CoprodI.Word.empty)
  (h_cons :
    (i : ι) →
      (m : M i) →
        (w : Monoid.CoprodI.Word M) →
          (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Monoid.CoprodI.Word.cons m w h1 h2)),
  Monoid.CoprodI.Word.consRecOn Monoid.CoprodI.Word.empty h_empty h_cons = h_empty
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_openCover_source : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : X.OpenCover),
  Function.Injective ⇑f →
    (∀ (i : 𝒰.I₀), AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) →
      AlgebraicGeometry.IsOpenImmersion f
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressEnd.toJson : Lean.Lsp.WorkDoneProgressEnd → Lean.Json
-- Lean.LocalContext
Lean.instInhabitedLocalDecl.default : Lean.LocalDecl
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.exp_inl : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Module Rᵐᵒᵖ M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] [inst_5 : TopologicalSpace R] [inst_6 : TopologicalSpace M]
  [inst_7 : IsTopologicalRing R] [inst_8 : IsTopologicalAddGroup M] [inst_9 : ContinuousSMul R M]
  [inst_10 : ContinuousSMul Rᵐᵒᵖ M] [Algebra ℚ R] [Module ℚ M] [T2Space R] [T2Space M] (x : R),
  NormedSpace.exp (TrivSqZeroExt.inl x) = TrivSqZeroExt.inl (NormedSpace.exp x)
-- Mathlib.Topology.Bases
/-- There exists a countable dense set.  -/
TopologicalSpace.SeparableSpace.exists_countable_dense : ∀ {α : Type u} {t : TopologicalSpace α} [self : TopologicalSpace.SeparableSpace α], ∃ s, s.Countable ∧ Dense s
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_iff_forall_one_lt_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a b : α}, a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.pretrivializationAtlas : {B : Type u_2} →
  {F : Type u_3} →
    {E : B → Type u_5} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            FiberPrebundle F E → Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)
-- Init.Data.SInt.Lemmas
ISize.eq_iff_toBitVec_eq : ∀ {a b : ISize}, a = b ↔ a.toBitVec = b.toBitVec
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Category of refl quivers.  -/
CategoryTheory.ReflQuiv : Type (max (u + 1) u (v + 1))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙ_nnreal_eq_real : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Module ℝ A] [IsSemitopologicalRing A] [inst_7 : IsScalarTower ℝ A A]
  [inst_8 : SMulCommClass ℝ A A] [T2Space A] [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_11 : NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A),
  autoParam (0 ≤ a) cfcₙ_nnreal_eq_real._auto_1 → cfcₙ f a = cfcₙ (fun x => ↑(f x.toNNReal)) a
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.isoMk_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} (X Y : CategoryTheory.GradedObject β C)
  (e : (i : β) → X i ≅ Y i) (i : β), (X.isoMk Y e).inv i = (e i).inv
-- Lean.Data.Format
Lean.Std.Format.getIndent : Lean.Options → ℕ
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.comp : ∀ {f g : ℕ → ℕ}, Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun n => f (g n)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.ShiftSequence.shiftIso.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a'),
  CochainComplex.ShiftSequence.shiftIso C n a a' ha' = CochainComplex.ShiftSequence.shiftIso C n a a' ha'
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.comonadToFunctor_mapIso_comonad_iso_mk : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.ε.app X) = M.ε.app X)
  (f_δ :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (f.hom.app X) (N.δ.app X) =
        CategoryTheory.CategoryStruct.comp (M.δ.app X)
          (CategoryTheory.CategoryStruct.comp (f.hom.app (M.obj X)) (N.map (f.hom.app X)))),
  (CategoryTheory.comonadToFunctor C).mapIso (CategoryTheory.ComonadIso.mk f f_ε f_δ) = f
-- Std.Http.Data.Chunk
Std.Http.instInhabitedTrailer.default : Std.Http.Trailer
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.BoundedFormula.constantsVarsEquiv.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} {n : ℕ},
  FirstOrder.Language.BoundedFormula.constantsVarsEquiv =
    FirstOrder.Language.BoundedFormula.mapTermRelEquiv (fun x => FirstOrder.Language.Term.constantsVarsEquivLeft)
      fun x => Equiv.sumEmpty (L.Relations x) ((FirstOrder.Language.constantsOn γ).Relations x)
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.isStrictOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → PartialOrder (α i)], IsStrictOrder (Colex (Π₀ (i : ι), α i)) fun x1 x2 => x1 < x2
-- Lean.Meta.Match.Match
Lean.Meta.Match.MkMatcherInput.isSplitter : Lean.Meta.Match.MkMatcherInput → Option Lean.Meta.Match.Overlaps
-- Mathlib.Data.Finset.Density
/-- **Alias** of the reverse direction of `Finset.dens_pos`. -/
Finset.Nonempty.dens_pos : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α}, s.Nonempty → 0 < s.dens
-- Mathlib.Analysis.ODE.Transform
isIntegralCurveAt_comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ a : ℝ},
  a ≠ 0 → (IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v ∘ fun x => x * a) (t₀ / a) ↔ IsIntegralCurveAt γ v t₀)
-- Init.Prelude
instHashableSubtype : {α : Sort u_1} → [Hashable α] → {p : α → Prop} → Hashable (Subtype p)
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Measures can be pushed forward (`R`-linearly) along continuous maps.  -/
AbstractMeasure.map : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      {E : Type u_4} →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace Y] →
            [inst_2 : AddCommGroup E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : IsTopologicalAddGroup E] →
                  [inst_5 : CommRing R] →
                    [inst_6 : TopologicalSpace R] →
                      [inst_7 : IsTopologicalRing R] →
                        [inst_8 : Module R E] →
                          [inst_9 : ContinuousSMul R E] → C(X, Y) → AbstractMeasure X R E →ₗ[R] AbstractMeasure Y R E
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.withEqs : {α : Type} → Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Version of `hasProd_ite_div_hasProd` for `CommMonoid` rather than `CommGroup`.
Rather than showing that the `ite` expression has a specific product in terms of `HasProd`, it gives
a relationship between the products of `f` and `ite (n = b) 0 (f n)` given that both exist.  -/
eq_mul_of_hasProd_ite : ∀ {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [inst : TopologicalSpace α]
  [inst_1 : CommMonoid α] [T2Space α] [ContinuousMul α] [inst_4 : DecidableEq β] {f : β → α} {a : α},
  HasProd f a L → ∀ (b : β) (a' : α), HasProd (fun n => if n = b then 1 else f n) a' L → a = a' * f b
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgebra.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : CommSemiring R] [inst_4 : Semiring A] [inst_5 : Algebra R A] (𝒜 𝒜_1 : ι → Submodule R A),
  𝒜 = 𝒜_1 → GradedAlgebra 𝒜 = GradedAlgebra 𝒜_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.commSemigroup.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemigroup α],
  Finset.commSemigroup = Function.Injective.commSemigroup SetLike.coe ⋯ ⋯
-- Mathlib.Logic.Equiv.Finset
_private.Mathlib.Logic.Equiv.Finset.0.Denumerable.lower'.match_1.splitter : (motive : List ℕ → ℕ → Sort u_1) →
  (x : List ℕ) →
    (x_1 : ℕ) → ((x : ℕ) → motive [] x) → ((m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n) → motive x x_1
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcyclesIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j], (K.pOpcyclesIso i j hi h).hom = K.pOpcycles j
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.continuous_base : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] (F : TopCat.Presheaf C X)
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)],
  Continuous TopCat.Presheaf.EtaleSpace.base
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.eq_bot_iff_forall : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊥ ↔ ∀ x ∈ S, x = 0
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.HasCardinalFilteredColimits C Cardinal.aleph0 ↔
    CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basisSet.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.basisSet✝ hs = ⋯.extend ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum at a point `c` and `y` is
a vector on the same ray as `f c`, then the function `fun x => ‖f x + y‖` has a local maximum
at `c`.  -/
IsLocalMax.norm_add_sameRay : ∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : TopologicalSpace X] {f : X → E} {c : X} {y : E},
  IsLocalMax (norm ∘ f) c → SameRay ℝ (f c) y → IsLocalMax (fun x => ‖f x + y‖) c
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coe_smul`. -/
MeasureTheory.VectorMeasure.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- The normed field structure determined by a rank one valuation.  -/
Valued.toNormedField : (L : Type u_1) →
  [inst : Field L] →
    (Γ₀ : Type u_2) →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [val : Valued L Γ₀] → [hv : Valued.v.RankOne] → NormedField L
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.slice_lt_slice_iff : ∀ {s : String.Slice} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁},
  q.slice p₀ p₁ h₁ h₂ < r.slice p₀ p₁ h₁' h₂' ↔ q < r
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_eq_one_of_subsingleton : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_5} [Subsingleton ι] (x : ι → K),
  Height.mulHeight x = 1
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
_private.Mathlib.FieldTheory.IsAlgClosed.Spectrum.0.spectrum.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.op_vadd_eq_op_vadd_op : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (r : M) (a : α),
  AddOpposite.op (r +ᵥ a) = AddOpposite.op r +ᵥ AddOpposite.op a
-- Mathlib.Algebra.Polynomial.Degree.Defs
/-- **Alias** of `Polynomial.degree_sub_lt_left`. -/
Polynomial.degree_sub_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  p.degree = q.degree → p ≠ 0 → p.leadingCoeff = q.leadingCoeff → (p - q).degree < p.degree
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.contains k m₂ = true →
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff m₂ ⋯) k fallback = fallback