mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiable.sum_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9}
  {s : Finset ι} {t : ι → (x : B) → E x}, (∀ i ∈ s, MDiff (T% t)) → MDiff fun x => ⟨x, ∑ i ∈ s, t i x⟩
-- Init.Data.List.Basic
List.append.eq_1 : ∀ {α : Type u_1} (x : List α), [].append x = x
-- Mathlib.Data.PNat.Find
PNat.find_lt_iff : ∀ {p : ℕ+ → Prop} [inst : DecidablePred p] (h : ∃ n, p n) (n : ℕ+), PNat.find h < n ↔ ∃ m < n, p m
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.all_eq_false_iff_exists_mem_getKey_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool},
  m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Const.get m a h) = false
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Lean.Parser.Command
Lean.Parser.Command.declaration : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_mem_one : ∀ {α : Type u_2} [inst : One α], 1 ∈ 1
-- Mathlib.CategoryTheory.Widesubcategory
/-- **Alias** of `CategoryTheory.WideSubcategory.isoMk`.

---

Build an isomorphism in `WideSubcategory P` from an isomorphism in `C`.  -/
CategoryTheory.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.MorphismProperty C} →
      [inst_1 : P.IsMultiplicative] →
        {X Y : CategoryTheory.WideSubcategory P} → (e : X.obj ≅ Y.obj) → P e.hom → P e.inv → (X ≅ Y)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The image and coimage of an arrow are naturally isomorphic.  -/
CategoryTheory.Abelian.coimIsoIm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian.coim ≅ CategoryTheory.Abelian.im
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_toUSize : ∀ (n : UInt8), n.toUSize.toUInt64 = n.toUInt64
-- Mathlib.Data.FinEnum
List.pfunFinEnum : (p : Prop) → [Decidable p] → (α : p → Type) → [(hp : p) → FinEnum (α hp)] → FinEnum ((hp : p) → α hp)
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- `Summable` over `Nat.Primes` iff over `ℕ` extending `f` by `0`.  -/
Nat.Primes.summable_iff_summable_ite : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M),
  (Summable fun p => f ↑p) ↔ Summable fun n => if Nat.Prime n then f n else 0
-- Batteries.Data.Array.Match
Array.Matcher.modifyStep.eq_2 : ∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (it' : Std.IterM n α)
  (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')),
  m.modifyStep it ⟨Std.IterStep.skip it', property⟩ =
    Std.IterStep.skip
      {
        internalState :=
          have __src := it.internalState;
          { inner := it', state := __src.state } }
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.FGModuleCatEvaluation_apply : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V),
  (CategoryTheory.ConcreteCategory.hom (FGModuleCat.FGModuleCatEvaluation K V).hom) (f ⊗ₜ[K] x) = f.toFun x
-- Mathlib.Order.Lattice.Nat
Set.biInter_le_succ : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋂ k, ⋂ (_ : k ≤ n + 1), u k = (⋂ k, ⋂ (_ : k ≤ n), u k) ∩ u (n + 1)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ι_μ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X Y : P.FullSubcategory),
  CategoryTheory.Functor.LaxMonoidal.μ P.ι X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (P.ι.obj X) (P.ι.obj Y))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {km : α}, t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.Context.mk.sizeOf_spec : ∀ (env : Lean.Environment) (checkReducible checkProj : Bool),
  sizeOf { env := env, checkReducible := checkReducible, checkProj := checkProj } =
    1 + sizeOf env + sizeOf checkReducible + sizeOf checkProj
-- Mathlib.Data.Matrix.Basis
Matrix.sum_single_eq_diagonal : ∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : AddCommMonoid α] [inst_2 : Fintype m] (f : m → α),
  ∑ i, Matrix.single i i (f i) = Matrix.diagonal f
-- Mathlib.Algebra.Algebra.Hom
AlgHom.comp_id : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ.comp (AlgHom.id R A) = φ
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.SymbolPriorities.mk.inj : ∀ {map map_1 : Lean.PHashMap Lean.Name ℕ}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrp_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (G : CategoryTheory.Grp C), CategoryTheory.yonedaGrp.obj G = CategoryTheory.yonedaGrpObj G.X
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorObj.congr_simp : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₁_1 : CategoryTheory.GradedObject I C) (e_X₁ : X₁ = X₁_1)
  (X₂ X₂_1 : CategoryTheory.GradedObject I C) (e_X₂ : X₂ = X₂_1) [inst_3 : X₁.HasTensor X₂] (a a_1 : I),
  a = a_1 →
    CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ a =
      CategoryTheory.GradedObject.Monoidal.tensorObj X₁_1 X₂_1 a_1
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.card_support_mul_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p * q).support.card ≤ p.support.card * q.support.card
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instModule_1 : {𝕜 : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommMonoid F] → [inst_4 : Module 𝕜 F] → (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Module 𝕜 (WeakBilin B)
-- Init.Data.Ord.SInt
Int64.instTransOrd : Std.TransOrd Int64
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
/-- Implementation, see `leftExactFunctorForgetEquivalence`.  -/
AddCommGrpCat.leftExactFunctorForgetEquivalence.unitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] →
        CategoryTheory.Functor.id (C ⥤ₗ AddCommGrpCat) ≅
          ((CategoryTheory.LeftExactFunctor.whiskeringRight C AddCommGrpCat (Type v)).obj
                (CategoryTheory.LeftExactFunctor.of (CategoryTheory.forget AddCommGrpCat))).comp
            AddCommGrpCat.leftExactFunctorForgetEquivalence.inverse
-- Batteries.Data.List.Basic
List.tailsTR.eq_1 : ∀ {α : Type u_1} (l : List α), l.tailsTR = List.tailsTR.go l #[]
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.liftFromOver_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (X_1 : CategoryTheory.Functor J (CategoryTheory.Over X)) (X_2 : CategoryTheory.WithTerminal J),
  (CategoryTheory.WithTerminal.liftFromOver.obj X_1).obj X_2 =
    match X_2 with
    | CategoryTheory.WithTerminal.of x => (X_1.obj x).left
    | CategoryTheory.WithTerminal.star => X
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {q : ENNReal},
  1 ≤ q → ∀ {f : α → ε} [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.MemLp f q μ → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Module.CharacterModule
/-- For an abelian group `A` and an element `a ∈ A`, there is a character `c : ℤ ∙ a → ℚ ⧸ ℤ` given by
`m • a ↦ m / n` where `n` is the smallest positive integer such that `n • a = 0` and when such `n`
does not exist, `c` is defined by `m • a ↦ m / 2`.
 -/
CharacterModule.ofSpanSingleton : {A : Type uA} → [inst : AddCommGroup A] → (a : A) → CharacterModule ↥(ℤ ∙ a)
-- Mathlib.Analysis.Distribution.DerivNotation
Laplacian.mk : {E : Type v} → {F : outParam (Type w)} → (E → F) → Laplacian E F
-- Init.Data.Array.Lemmas
Array.getElem_swapIfInBounds_of_size_le_right : ∀ {α : Type u_1} {xs : Array α} {i j k : ℕ},
  xs.size ≤ j → ∀ (hk : k < (xs.swapIfInBounds i j).size), (xs.swapIfInBounds i j)[k] = xs[k]
-- Mathlib.RingTheory.Fintype
Finset.univ_of_card_le_three : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : Fintype R] [inst_2 : DecidableEq R],
  Fintype.card R ≤ 3 → Finset.univ = {0, 1, -1}
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.algHomUnitsEquiv_apply_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (f : (S →ₐ[R] S)ˣ)
  (a : S), ((AlgEquiv.algHomUnitsEquiv R S) f).symm a = ↑↑f⁻¹ a
-- Std.Time.Zoned.ZoneRules
/-- Represents the rules for a time zone.
 -/
Std.Time.TimeZone.ZoneRules : Type
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- A quasi-compact morphism is a (locally-closed) immersion if and only if it can be factored into
an open immersion followed by a closed immersion.
 -/
AlgebraicGeometry.IsImmersion.isImmersion_iff_exists_of_quasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.IsImmersion f ↔
    ∃ Z g₁ g₂,
      AlgebraicGeometry.IsOpenImmersion g₁ ∧
        AlgebraicGeometry.IsClosedImmersion g₂ ∧ CategoryTheory.CategoryStruct.comp g₁ g₂ = f
-- Mathlib.Analysis.Normed.Algebra.Spectrum
quasispectrum.isCompact_nnreal : ∀ {B : Type u_3} [inst : NonUnitalNormedRing B] [inst_1 : NormedSpace ℝ B] [IsScalarTower ℝ B B] [SMulCommClass ℝ B B]
  (a : B) [CompactSpace ↑(quasispectrum ℝ a)], IsCompact (quasispectrum NNReal a)
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR.eq_1 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool), n.anyLTTR f = Nat.anyLTTR.loop✝ n f n ⋯
-- Batteries.Recycling.RBTree.WF
/-- The `del` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.del : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered cmp (RBTree.RBNode.del cut t)
-- Mathlib.GroupTheory.Coset.Basic
rightCoset_one : ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), MulOpposite.op 1 • s = s
-- Lean.Elab.Do.Basic
/-- Return `true` if the given `letDecl` contains binders.  -/
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.letDeclHasBinders : Lean.Syntax → Bool
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.IsClosedUnderCokernels.cokernels_le : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsClosedUnderCokernels],
  (CategoryTheory.MorphismProperty.ofObjectProperty P P).cokernels ≤ P
-- Mathlib.Topology.EMetricSpace.Defs
edist_ofDual : ∀ {X : Type u_1} [inst : EDist X] (a b : Xᵒᵈ), edist (OrderDual.ofDual a) (OrderDual.ofDual b) = edist a b
-- Mathlib.Analysis.Calculus.TangentCone.Prod
/-- The tangent cone of a product contains the tangent cone of its right factor.  -/
subset_tangentConeAt_prod_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {x : E} {s : Set E}
  {y : F} {t : Set F}, x ∈ closure s → ⇑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.re_sqrt_ofReal : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {a : ℝ}, RCLike.re (RCLike.sqrt ↑a) = √a
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_comp_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {P : CategoryTheory.Subobject Y}
  (f : X ⟶ CategoryTheory.Subobject.underlying.obj P), P.Factors (CategoryTheory.CategoryStruct.comp f P.arrow)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContIntertwiningMap_mk' : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (e : V ≃L[R] W)
  (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e),
  ↑(ContRepresentation.Equiv.mk e he) = { toContinuousLinearMap := ↑e, isIntertwining' := he }
-- Mathlib.Topology.ContinuousOn
Set.MapsTo.closure_of_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, Set.MapsTo f s t → ContinuousOn f (closure s) → Set.MapsTo f (closure s) (closure t)
-- Mathlib.Topology.Order.Basic
nhdsLE_eq_iInf_inf_principal : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderTopology α] (a : α),
  nhdsWithin a (Set.Iic a) = (⨅ u, ⨅ (_ : u < a), Filter.principal (Set.Ioi u)) ⊓ Filter.principal (Set.Iic a)
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.comp.match_1.eq_2 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : (x x_1 x_2 : CategoryTheory.Join C D) → x.Hom x_1 → x_1.Hom x_2 → Sort u_5) (_x _y : C) (_z : D)
  (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y))
  (x_1 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z))
  (h_1 :
    (_x _y _z : C) →
      (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
        (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)) →
          motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.left _z) f g)
  (h_2 :
    (_x _y : C) →
      (_z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
          (x_2 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.right _z) x x_2)
  (h_3 :
    (_x : C) →
      (_y _z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
          (x_2 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) x x_2)
  (h_4 :
    (_x _y _z : D) →
      (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y)) →
        (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
          motive (CategoryTheory.Join.right _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) f g),
  (match CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_1 with
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.left _z, f, g => h_1 _x _y _z f g
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_2 =>
      h_2 _x _y _z x x_2
    | CategoryTheory.Join.left _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, x, x_2 =>
      h_3 _x _y _z x x_2
    | CategoryTheory.Join.right _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, f, g =>
      h_4 _x _y _z f g) =
    h_2 _x _y _z x x_1
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.coe_eval₂Hom : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] (hφ : Continuous ⇑φ) (ha : PowerSeries.HasEval a),
  ⇑(PowerSeries.eval₂Hom hφ ha) = PowerSeries.eval₂ φ a
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.bounded_below : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ},
  IsCoercive B → ∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖(InnerProductSpace.continuousLinearMapOfBilin B) v‖
-- Mathlib.Condensed.Light.AB
LightCondensed.instCountableAB4StarLightCondMod : ∀ {R : Type u} [inst : Ring R], CategoryTheory.CountableAB4Star (LightCondMod R)
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Ioo a b) = Set.Ioo a b
-- Init.Data.String.Basic
String.next : String → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_inl_inr : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₁)
  (b : β₂), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inl a) (Sum.inr b) = (g₁ a b).disjSum (g₂ a b)
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The primitive part of `Φ'`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial (Polynomial K)
-- Init.Data.UInt.Lemmas
USize.mul_two : ∀ {a : USize}, a * 2 = a + a
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instMonoFunctorOppositeHomFullSubcategoryIsSheafOfHasWeakSheafifyOfSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} [CategoryTheory.HasWeakSheafify J A]
  (f : F ⟶ G) [CategoryTheory.Mono f], CategoryTheory.Mono f.hom
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheaf.eval_germ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] {N : Type u}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (U : TopologicalSpace.Opens M) (x : M) (hx : x ∈ U)
  (f : (smoothSheaf IM I M N).presheaf.obj (Opposite.op U)),
  smoothSheaf.eval IM I N x ((CategoryTheory.ConcreteCategory.hom ((smoothSheaf IM I M N).presheaf.germ U x hx)) f) =
    ↑f ⟨x, hx⟩
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.response.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID), sizeOf (Lean.JsonRpc.MessageMetaData.response id) = 1 + sizeOf id
-- Init.Data.Vector.Nat
Vector.sum_append_nat : ∀ {n m : ℕ} {as₁ : Vector ℕ n} {as₂ : Vector ℕ m}, (as₁ ++ as₂).sum = as₁.sum + as₂.sum
-- Mathlib.Data.Finset.Image
Finset.surjOn_iff_subset_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Set.SurjOn f ↑s ↑t ↔ t ⊆ Finset.image f s
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.nontrivial : Nontrivial Ordinal.{u}
-- Mathlib.NumberTheory.Real.Irrational
instDecidableIrrationalSqrtCastReal : (n : ℕ) → Decidable (Irrational √↑n)
-- Mathlib.Algebra.Group.Action.Pi
/-- Non-dependent version of `Pi.vadd`. Lean gets confused by the dependent instance
if this is not present.  -/
Function.hasVAdd : {ι : Type u_1} → {M : Type u_2} → {α : Type u_7} → [VAdd M α] → VAdd M (ι → α)
-- Mathlib.Topology.Constructions
isOpenMap_ofDual : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpenMap ⇑OrderDual.ofDual
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.trivial_apply : ∀ (R : Type u_1) [inst : CommMonoid R] (R' : Type u_2) [inst_1 : CommMonoidWithZero R'] (x : R),
  (MulChar.trivial R R') x = if IsUnit x then 1 else 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' S'' : D} {T : CategoryTheory.Functor C D} {f : S ⟶ S'} {f' : S' ⟶ S''}
  {h : CategoryTheory.StructuredArrow S'' T},
  (CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h =
    (CategoryTheory.StructuredArrow.map f).obj ((CategoryTheory.StructuredArrow.map f').obj h)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_compContinuousLinearMap_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [Nontrivial F] (p : FormalMultilinearSeries 𝕜 F G)
  (u : E ≃L[𝕜] F), (p.compContinuousLinearMap ↑u).radius ≤ ‖↑u.symm‖ₑ * p.radius
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.instNonemptyQuotient : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [I.IsTwoSided], Nonempty (R ⧸ I)
-- Mathlib.Analysis.Normed.Group.Uniform
uniformContinuous_nnnorm' : ∀ {E : Type u_2} [inst : SeminormedGroup E], UniformContinuous fun a => ‖a‖₊
-- Mathlib.LinearAlgebra.QuadraticForm.Complex
QuadraticForm.equivalent_sum_squares : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module ℂ M] [FiniteDimensional ℂ M] (Q : QuadraticForm ℂ M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q) → QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℂ 1)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.mem_support_of_reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ≠ v → G.Reachable u v → u ∈ G.support
-- Mathlib.CategoryTheory.Simple
/-- Any simple object in a preadditive category is indecomposable.  -/
CategoryTheory.indecomposable_of_simple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) [CategoryTheory.Simple X],
  CategoryTheory.Indecomposable X
-- Std.Http.Protocol.H1
/-- Resets per-message reader/writer state for the next pipelined message when
keep-alive remains enabled.

Unconsumed input and already-produced output are preserved. If keep-alive is
disabled, closes reader/writer and emits `.close` instead.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.resetForNextMessage : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_le_nilradical : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, pNilradical R p ≤ nilradical R
-- Mathlib.Logic.Equiv.Defs
/-- Equivalence between `Fin 0` and `Empty`.  -/
finZeroEquiv : Fin 0 ≃ Empty
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_sup : ∀ {N : Type u_4} [inst : CommMonoid N] {s t : Submonoid N} {x : N}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x