mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const_sorted : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {c : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.const basis_hd basis_tl c).Sorted
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Given a constant, compute what needs to be added to the various discrimination trees.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.addConst : Mathlib.Tactic.ClickSuggestions.Choice →
  Lean.Environment →
    Mathlib.Tactic.ClickSuggestions.Entries✝ →
      Lean.Name → Lean.ConstantInfo → Lean.MetaM Mathlib.Tactic.ClickSuggestions.Entries✝
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.coeff_modOf_of_exists_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g g' : G),
  (∃ d, g' = g + d) → (x.modOf g).coeff g' = 0
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The morphism into the factorisation midpoint.  -/
CategoryTheory.Factorisation.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Factorisation f) → X ⟶ self.mid
-- Init.Data.SInt.Lemmas
Int8.div_zero : ∀ {a : Int8}, a / 0 = 0
-- Mathlib.Data.Sigma.Basic
/-- Interpret a dependent function with two arguments as a function on `Σ x : α, β x`.

This also exists as an `Equiv` as `(Equiv.piCurry γ).symm`.  -/
Sigma.uncurry : {α : Type u_1} →
  {β : α → Type u_4} → {γ : (a : α) → β a → Type u_7} → ((x : α) → (y : β x) → γ x y) → (x : Sigma β) → γ x.fst x.snd
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- This condition `eq_bot_or_top` is equivalent to being a field. However,
`Ideal.spanNorm_spanNorm_of_field` would be harder to apply since we'd need to upgrade
a `CommRing R` instance to a `Field R` instance.
 -/
Ideal.spanNorm_spanNorm_of_bot_or_top : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (T : Type u_4) [inst_9 : CommRing T] [inst_10 : IsDomain T]
  [inst_11 : IsIntegrallyClosed T] [inst_12 : Algebra R T] [inst_13 : Algebra T S] [inst_14 : Module.Finite R T]
  [inst_15 : Module.Finite T S] [inst_16 : Module.IsTorsionFree R T] [inst_17 : Module.IsTorsionFree T S]
  [IsScalarTower R T S],
  (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) → ∀ (I : Ideal S), Ideal.spanNorm R (Ideal.spanNorm T I) = Ideal.spanNorm R I
-- Mathlib.Algebra.GroupWithZero.Hom
/-- The proposition that the function preserves 1  -/
MonoidWithZeroHom.map_one' : ∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (self : α →*₀ β),
  (↑self).toFun 1 = 1
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] {F G : CategoryTheory.Functor W₁ W₂}
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι)
  (C : HomologicalComplex W₁ c) (x : ι),
  ((CategoryTheory.NatIso.mapHomologicalComplex α c).inv.app C).f x = α.inv.app (C.X x)
-- Mathlib.Order.CompleteLattice.Basic
iInf_iInf_eq_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = x → α},
  ⨅ x, ⨅ (h : b = x), f x h = f b ⋯
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- The action of a (pre)functor on vertices/objects.  -/
Prefunctor.obj : {V : Type u₁} → [inst : Quiver V] → {W : Type u₂} → [inst_1 : Quiver W] → V ⥤q W → V → W
-- Init.Data.SInt.Float
/-- Obtains the `Float` whose value is the same as the given `Int8`.

This function does not reduce in the kernel.
 -/
Int8.toFloat : Int8 → Float
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesLimitsOfSize_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [inst_3 : sInfHomClass F α β],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, v, u, v} (↑f).toFunctor
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The coercion from `lp E p` to `∀ i, E i` is uniformly continuous.  -/
lp.uniformContinuous_coe : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)],
  UniformContinuous Subtype.val
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resEquiv_functor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f : G ≃ₜ* H),
  (ContAction.resEquiv V f).functor = ContAction.res V ↑f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Var.denote : {α : Type u_1} → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Var → α
-- Mathlib.Algebra.Quaternion
Quaternion.instInv : {R : Type u_1} → [inst : Field R] → Inv (Quaternion R)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_comp : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p q : Polynomial R),
  Polynomial.map f (p.comp q) = (Polynomial.map f p).comp (Polynomial.map f q)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.addRight_symm : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Equiv.symm (Equiv.addRight a) = Equiv.addRight (-a)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ),
  IsScalarTower R ((AlgebraicGeometry.structureSheafInType R R).obj.obj U)
    ((AlgebraicGeometry.structureSheafInType R M).obj.obj U)
-- Mathlib.InformationTheory.Hamming
Hamming.instInhabited : {ι : Type u_2} → {β : ι → Type u_3} → [(i : ι) → Inhabited (β i)] → Inhabited (Hamming β)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RooSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsStableUnderRetractsInnerAnodyneExtensions : SSet.innerAnodyneExtensions.IsStableUnderRetracts
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getEntryLT? k = Std.DTreeMap.Internal.Impl.getEntryLT?.go k none
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- The type of bilinear maps which are accepted by `CliffordAlgebra.even.lift`.  -/
CliffordAlgebra.EvenHom : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          QuadraticForm R M → (A : Type u_3) → [inst_3 : Ring A] → [Algebra R A] → Type (max u_2 u_3)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse_apply : ∀ {M : Type u_2} {X : Type u_5} [inst : SMul M X] {Y₁ : Type u_8} [inst_1 : SMul M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁ → X)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : Y₁), (f.inverse g h₁ h₂) a = g a
-- Mathlib.Data.Set.Defs
Set.instFunctor : Functor Set
-- Init.Data.Array.Count
Array.count_filter : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {p : α → Bool} {a : α} {xs : Array α},
  p a = true → Array.count a (Array.filter p xs) = Array.count a xs
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.  -/
CategoryTheory.SymmetricCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- Any linear map that preserves the quadratic form lifts to an `AlgHom` between algebras.

See `CliffordAlgebra.equivOfIsometry` for the case when `f` is a `QuadraticForm.IsometryEquiv`.  -/
CliffordAlgebra.map : {R : Type u_1} →
  [inst : CommRing R] →
    {M₁ : Type u_4} →
      {M₂ : Type u_5} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {Q₁ : QuadraticForm R M₁} →
                  {Q₂ : QuadraticForm R M₂} → (Q₁ →qᵢ Q₂) → CliffordAlgebra Q₁ →ₐ[R] CliffordAlgebra Q₂
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toEquiv_toHomeomorphOfContinuousClosed : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (h₁ : Continuous ⇑e) (h₂ : IsClosedMap ⇑e), (e.toHomeomorphOfContinuousClosed h₁ h₂).toEquiv = e
-- Mathlib.RingTheory.Ideal.Defs
Ideal.mul_unit_mem_iff_mem : ∀ {α : Type u} [inst : CommSemiring α] (I : Ideal α) {x y : α}, IsUnit y → (x * y ∈ I ↔ x ∈ I)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forM_eq_forM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α × β → m PUnit.{w + 1}}, forM t f = forM t.toList f
-- Batteries.Data.List.Lemmas
List.filter.match_1.congr_eq_1 : ∀ (motive : Bool → Sort u_1) (x : Bool) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  x = true →
    (match x with
      | true => h_1 ()
      | false => h_2 ()) ≍
      h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_bot : ∀ {V : Type u} {G : SimpleGraph V}, ⊥.coe = ⊥
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.module' : {R' : Type u'} →
  {R : Type u} →
    {A : Type v} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [inst_3 : Star A] →
              (S : NonUnitalStarSubalgebra R A) →
                [inst_4 : Semiring R'] →
                  [inst_5 : SMul R' R] → [inst_6 : Module R' A] → [IsScalarTower R' R A] → Module R' ↥S
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The norm squared function for `PreInnerProductSpace.Core` structure.  -/
InnerProductSpace.Core.normSq : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] → [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [c : PreInnerProductSpace.Core 𝕜 F] → F → ℝ
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_le_div : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {n : ℕ},
  n ≠ 0 → schnirelmannDensity A ≤ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n
-- Init.Data.String.Lemmas.Basic
String.Pos.byte_eq_byte_toSlice : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p.byte h = p.toSlice.byte ⋯
-- Lean.Meta.Transform
Lean.TransformStep.done.inj : ∀ {e e_1 : Lean.Expr}, Lean.TransformStep.done e = Lean.TransformStep.done e_1 → e = e_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → Array.map Sigma.fst m.toArray = m.keysArray
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ≅ G) (β : G ≅ H),
  CategoryTheory.NatIso.unop (α ≪≫ β) = CategoryTheory.NatIso.unop β ≪≫ CategoryTheory.NatIso.unop α
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.whiskerRight_app_apply : ∀ {K K' : SSet} (f : K ⟶ K') (L : SSet) {Δ : SimplexCategoryᵒᵖ}
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.app Δ) (L.obj Δ))) x =
    ((CategoryTheory.ConcreteCategory.hom (f.app Δ)) x.1, x.2)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_le_floor_add_one : ∀ (r : ENNReal), ⌈r⌉ₑ ≤ ⌊r⌋ₑ + 1
-- Mathlib.FieldTheory.AxGrothendieck
/-- The **Ax-Grothendieck** theorem

If `K` is an algebraically closed field, and `S : Set (ι → K)` is the `zeroLocus` of an ideal
of the multivariable polynomial ring, then any injective polynomial map `S → S`  is also
surjective on `S`.  -/
ax_grothendieck_zeroLocus : ∀ {K : Type u_1} {ι : Type u_2} [inst : Field K] [IsAlgClosed K] [Finite ι] (I : Ideal (MvPolynomial ι K))
  (p : ι → MvPolynomial ι K),
  have S := MvPolynomial.zeroLocus K I;
  Set.MapsTo (fun v i => (MvPolynomial.eval v) (p i)) S S →
    Set.InjOn (fun v i => (MvPolynomial.eval v) (p i)) S → Set.SurjOn (fun v i => (MvPolynomial.eval v) (p i)) S S
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.not_mem_nil : ∀ {α : Type u_1} {v : α}, ¬Std.Sat.CNF.Clause.Mem v []
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- A `StrictSegal` structure on a simplicial set `X` restricts to a
`Truncated.StrictSegal` structure on the `n + 1`-truncation of `X`.  -/
SSet.StrictSegal.truncation : {X : SSet} → X.StrictSegal → (n : ℕ) → ((SSet.truncation (n + 1)).obj X).StrictSegal
-- Init.Data.UInt.Lemmas
USize.add_def : ∀ (a b : USize), a + b = { toBitVec := a.toBitVec + b.toBitVec }
-- Mathlib.Data.Nat.ModEq
/-- A variant of `modEq_iff_dvd` with `Nat` divisibility  -/
Nat.modEq_iff_dvd' : ∀ {n a b : ℕ}, a ≤ b → (a ≡ b [MOD n] ↔ n ∣ b - a)
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Context.mk.injEq : ∀ (letFVars letFVars_1 : List Lean.FVarId),
  ({ letFVars := letFVars } = { letFVars := letFVars_1 }) = (letFVars = letFVars_1)
-- Mathlib.Algebra.Category.Grp.Colimits
/-- If `c` is a cocone of `F` such that `Quot.desc F c` is bijective, then `c` is a colimit
cocone of `F`.
 -/
AddCommGrpCat.Colimits.isColimit_of_bijective_desc : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      (c : CategoryTheory.Limits.Cocone F) →
        [inst_1 : DecidableEq J] →
          Function.Bijective ⇑(AddCommGrpCat.Colimits.Quot.desc F c) → CategoryTheory.Limits.IsColimit c
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionObj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (d : C) (c : CategoryTheory.Functor C C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c = c.obj d
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.anodyneExtensions_pushoutObjObjι' : ∀ {X₁ X₂ Y₁ Y₂ : SSet} {i : X₁ ⟶ Y₁} {j : X₂ ⟶ Y₂}
  (sq₁₂ : (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj i j) [CategoryTheory.Mono j],
  SSet.anodyneExtensions i → SSet.anodyneExtensions sq₁₂.ι
-- Mathlib.Order.DirSupClosed
DirSupClosed.dirSupClosedOn : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupClosed s → DirSupClosedOn D s
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- The inclusion `Φ.ιIteration J` is a transfinite composition of
shape `J` of morphisms in `Φ.prop`.  -/
CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  Φ.prop.TransfiniteCompositionOfShape J (Φ.ιIteration J)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_ne_bot_iff : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {p : Submodule R M} [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_8 : RingHomInvPair σ₂₁ σ₁₂] {e : M ≃ₛₗ[σ₁₂] M₂}, Submodule.map (↑e) p ≠ ⊥ ↔ p ≠ ⊥
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_cnstr_nc_cert : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- The sum of a locally finite collection of sections is `C^k` on a set `u` iff each section is.  -/
ContMDiffOn.sum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) u) →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑' (i : ι), t i x⟩) u
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkPULiftDown : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.GroupTheory.CommutingProbability
/-- The commuting probability of a finite type with a multiplication operation.  -/
commProb : (M : Type u_1) → [Mul M] → ℚ
-- Lean.Elab.App
/-- Elaborate the given `Arg` and add it to the result. See `addNewArg`.
Recall that, `Arg` may be wrapping an already elaborated `Expr`.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.elabAndAddNewArg : Lean.Name → Lean.Elab.Term.Arg → Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- A partial linear map is called a "partial Hahn embedding" if it extends
`HahnEmbedding.Seed.baseEmbedding`, is strictly monotone, and is truncation-closed.  -/
HahnEmbedding.IsPartial : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              HahnEmbedding.Seed K M R → (M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)) → Prop
-- Lean.Data.Json.Parser
Lean.Json.Parser.numWithDecimals : Std.Internal.Parsec.String.Parser Lean.JsonNumber
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.not_mem_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, a ∉ ∅
-- Lean.Util.LeanOptions
Lean.instCoeBoolLeanOptionValue : Coe Bool Lean.LeanOptionValue
-- Mathlib.FieldTheory.Differential.Basic
/-- If `K` is a finite field extension of `F` then we can define a differential algebra on `K`, by
choosing a primitive element of `K`, `k` and then using the equivalence to `AdjoinRoot (minpoly k)`.
 -/
Differential.differentialFiniteDimensional : (F : Type u_2) →
  [inst : Field F] →
    [Differential F] →
      [CharZero F] →
        (K : Type u_3) → [inst_3 : Field K] → [inst_4 : Algebra F K] → [FiniteDimensional F K] → Differential K
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaIsoCoyoneda_inv_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{max w v₁, u₁} C] (X : Cᵒᵖ) (X_1 : C),
  (CategoryTheory.uliftCoyonedaIsoCoyoneda.inv.app X).app X_1 = Equiv.ulift.toIso.inv
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_unitIso_inv_app_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k k' : α},
  m.get? k = some k' → k' ∈ m
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.qsmul_of_nonpos : ∀ {M : Type u_2} [inst : AddCommGroup M] {a : ℚ} (h : a ≤ 0) (x : DivisibleHull M),
  a • x =
    -((have this := ⟨-a, ⋯⟩;
        this) •
        x)
-- Mathlib.Topology.Maps.Strict.Group
/-- A group homomorphism is strict if and only if the canonical isomorphism
`G ⧸ f.ker ≃ f.range` is a homeomorphism.  -/
MonoidHom.isStrictMap_iff_isHomeomorph_quotientKerEquivRange : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H], Topology.IsStrictMap ⇑f ↔ IsHomeomorph ⇑(QuotientGroup.quotientKerEquivRange f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} (h : m.WF) {hc : k' ∈ m.alter k f},
  (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_unitary_smul : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] (U : ↥(unitary E)) (A : E), ‖U • A‖ = ‖A‖
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings.  -/
four_mul_le_sq_add : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddLeftReflectLE R] [AddLeftMono R] (a b : R), 4 * a * b ≤ (a + b) ^ 2
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree `Polynomial.natSepDegree` of a polynomial is a natural number,
defined to be the number of distinct roots of it over its splitting field.
This is similar to `Polynomial.natDegree` but not to `Polynomial.degree`, namely, the separable
degree of `0` is `0`, not negative infinity.  -/
Polynomial.natSepDegree : {F : Type u} → [inst : Field F] → Polynomial F → ℕ
-- Lean.Expr
Lean.Expr.getRevArgD : Lean.Expr → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.mk_smul_mulDistribActionHom_apply : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : AddMonoid A] [inst_1 : DistribSMul M A]
  [inst_2 : Monoid N] [inst_3 : AddMonoid B] [inst_4 : DistribMulAction N A] [inst_5 : SMulCommClass M N A]
  [inst_6 : DistribMulAction N B] (c : M) (f : A →+[N] B) (a : A), (DomMulAct.mk c • f) a = f (c • a)
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map_map₂_antidistrib_right`.  -/
Filter.map_map₂_right_anticomm : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β}
  {m : α → β' → γ} {n : β → β'} {m' : β → α → δ} {n' : δ → γ},
  (∀ (a : α) (b : β), m a (n b) = n' (m' b a)) → Filter.map₂ m f (Filter.map n g) = Filter.map n' (Filter.map₂ m' g f)