mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Bernstein
/-- The `n`-th approximation of a continuous function on `[0,1]` by Bernstein polynomials,
given by `∑ k, bernstein n k x • f (k/n)`.
 -/
bernsteinApproximation : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [inst_3 : Module ℝ E] → [ContinuousSMul ℝ E] → ℕ → C(↑unitInterval, E) → C(↑unitInterval, E)
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.mapA.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The limit cone on `spanFunctor` with point `C`.  -/
Profinite.NobelingProof.spanCone : {I : Type u} →
  {C : Set (I → Bool)} →
    [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] →
      (hC : IsCompact C) → CategoryTheory.Limits.Cone (Profinite.NobelingProof.spanFunctor hC)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator_assoc : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c₁ c₂ c₃ : C) (d : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c₁) c₂)
        c₃ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
        (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c₁
            (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c₁) c₂ c₃).hom
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
          (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c₁ c₂).hom c₃)
        h)
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toNatLinearEquiv_refl : ∀ {M : Type u_5} [inst : AddCommMonoid M], (AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M
-- Mathlib.Topology.Constructions.SumProd
frontier_prod_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
  frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
-- Mathlib.Combinatorics.Graph.Simple
Graph.Simple.toLoopless : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} [self : G.Simple], G.Loopless
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_5.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_6 t ×' Lean.Elab.Term.Do.Code.below_5 t
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_3 : Nat.Partrec.Code.left.eval = ↑fun n => (Nat.unpair n).1
-- Mathlib.Data.Set.Function
Set.SurjOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {p : Set γ} {f : α → β} {g : β → γ},
  Set.SurjOn g t p → Set.SurjOn f s t → Set.SurjOn (g ∘ f) s p
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.instNonempty : ∀ {V : Type u_1} [inst : Quiver V] [Nonempty V], Nonempty (Quiver.FreeGroupoid V)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsRightUniformAddGroup.toIsTopologicalAddGroup : ∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : AddGroup G} [self : IsRightUniformAddGroup G],
  IsTopologicalAddGroup G
-- Lean.DocString.Syntax
/-- A _directive_, which is an extension to the Verso language in block position.

Directives have the following syntax:
```
:::NAME ARGS*
CONTENT*
:::
```

The `NAME` is an identifier that determines which directive is being used, akin to a function name.
Each of the `ARGS` may have the following forms:
* A value, which is a string literal, natural number, or identifier
* A named argument, of the form `(NAME := VALUE)`
* A flag, of the form `+NAME` or `-NAME`

The `CONTENT` is a sequence of block content. Directives may be nested by using more colons in
the outer directive. For example:
```
::::outer +flag (arg := 5)
A paragraph.
:::inner "label"
* 1
* 2
:::
::::
```

 -/
Lean.Doc.Syntax.directive : Lean.ParserDescr
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R} [NoZeroDivisors R],
  p ∣ q → p.scaleRoots r ∣ q.scaleRoots r
-- Mathlib.Data.Sym.Basic
Sym.inhabitedSym' : {α : Type u_1} → [Inhabited α] → (n : ℕ) → Inhabited (Sym.Sym' α n)
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_comap' : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} {f : γ → β} {g : α → γ} [v : UniformSpace β] [u : UniformSpace α],
  UniformContinuous (f ∘ g) → UniformContinuous g
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.fromPreimage_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (p : F' ⟶ F) {Z : CategoryTheory.Functor C (Type w)} (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.fromPreimage p) (CategoryTheory.CategoryStruct.comp G.ι h) =
    CategoryTheory.CategoryStruct.comp (G.preimage p).ι (CategoryTheory.CategoryStruct.comp p h)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜' E F} {x : E},
  HasFPowerSeriesAt f p x → HasFPowerSeriesAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) x
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredLimit_of_isPredArchimedean : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α], ¬Order.IsPredLimit a
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finite_finsupp_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_1},
  Module.Finite R (ι →₀ M) ↔ IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f],
  IsOpen {x | (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallySmooth}
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- the map from the coproduct of two copies of `A` to `P.I`, when `P` is
a cylinder object for `A`. `P` shall be a *good* cylinder object
when this morphism is a cofibration.  -/
HomotopicalAlgebra.Precylinder.i : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (P : HomotopicalAlgebra.Precylinder A) → [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A] → A ⨿ A ⟶ P.I
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Show that `uliftYoneda.leftKanExtension A` is the unique colimit-preserving
functor which extends `A` to the presheaf category.

The second part of [MM92], Chapter I, Section 5, Corollary 4.
See Property 3 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.
 -/
CategoryTheory.Presheaf.uniqueExtensionAlongULiftYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        {A : CategoryTheory.Functor C ℰ} →
          [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] →
            (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ) →
              (A ≅ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) →
                [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
                        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
                      L] →
                  L ≅ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.leftKanExtension A
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).base = X.base
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.add : Nat.Primrec (Nat.unpaired fun x1 x2 => x1 + x2)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabNamedPattern : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_single_mul_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (a : Γ) (r : R),
  ((HahnSeries.single a) r * x).cardSupp ≤ x.cardSupp
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_toSupBotHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), ⇑f.toSupBotHom = ⇑f
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
ContinuousLinearMap.toLinearMap.hcongr_14 : ∀ (R R' : Type u_1),
  R = R' →
    ∀ (S S' : Type u_2),
      S = S' →
        ∀ (inst : Semiring R) (inst' : Semiring R'),
          inst ≍ inst' →
            ∀ (inst_1 : Semiring S) (inst'_1 : Semiring S'),
              inst_1 ≍ inst'_1 →
                ∀ (σ : R →+* S) (σ' : R' →+* S'),
                  σ ≍ σ' →
                    ∀ (M M' : Type u_3),
                      M = M' →
                        ∀ (inst_2 : TopologicalSpace M) (inst'_2 : TopologicalSpace M'),
                          inst_2 ≍ inst'_2 →
                            ∀ (inst_3 : AddCommMonoid M) (inst'_3 : AddCommMonoid M'),
                              inst_3 ≍ inst'_3 →
                                ∀ (M₂ M₂' : Type u_4),
                                  M₂ = M₂' →
                                    ∀ (inst_4 : TopologicalSpace M₂) (inst'_4 : TopologicalSpace M₂'),
                                      inst_4 ≍ inst'_4 →
                                        ∀ (inst_5 : AddCommMonoid M₂) (inst'_5 : AddCommMonoid M₂'),
                                          inst_5 ≍ inst'_5 →
                                            ∀ (inst_6 : Module R M) (inst'_6 : Module R' M'),
                                              inst_6 ≍ inst'_6 →
                                                ∀ (inst_7 : Module S M₂) (inst'_7 : Module S' M₂'),
                                                  inst_7 ≍ inst'_7 →
                                                    ∀ (self : M →SL[σ] M₂) (self' : M' →SL[σ'] M₂'),
                                                      self ≍ self' → ↑self ≍ ↑self'
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of `ne_top_of_lt`. -/
LT.lt.ne_top : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a ≠ ⊤
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.monicDegreeEq_coe : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  ↑(Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p) =
    Polynomial.map (algebraMap R (Polynomial.UniversalFactorizationRing m k hn p)) ↑p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) =
        (Std.DTreeMap.Internal.Impl.contains k t || (List.map Prod.fst l).contains k)
-- Mathlib.Data.Sum.Order
OrderIso.sumLexCongr_apply : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} [inst : LE α₁] [inst_1 : LE α₂] [inst_2 : LE β₁]
  [inst_3 : LE β₂] (ea : α₁ ≃o α₂) (eb : β₁ ≃o β₂) (a : α₁ ⊕ₗ β₁),
  (ea.sumLexCongr eb) a = toLex (Sum.map (⇑ea) (⇑eb) (ofLex a))
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Multiplicativity of leading coefficients  -/
MonomialOrder.coeff_mul_of_degree_add : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  MvPolynomial.coeff (m.degree f + m.degree g) (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.instInhabited : {R : Type u} → [inst : NonUnitalNonAssocRing R] → Inhabited (NonUnitalSubring R)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.mem_annihilator_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M)
  (r : R), r ∈ (Submodule.span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Lean.Elab.DocString
/-- Runs a `TermElabM` action, saving and restoring the term elaboration state so that metavariables
and other state changes do not leak. Messages produced by the action are preserved.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.withSaveRestoreTermState : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Order.BourbakiWitt
CompleteLattice.ωScottContinuous.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLinearOrder β] {f g : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f →
    OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous (f ⊓ g)
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {i : ℕ} (e : CategoryTheory.Abelian.Ext Y X i) (n : ℕ)
  [CategoryTheory.HasInjectiveDimensionLT X n], n ≤ i → e = 0
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The identity morphism of `X : Bipointed`.  -/
Bipointed.Hom.id : (X : Bipointed) → X.Hom X
-- Mathlib.Topology.Defs.Filter
/-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces
and `s : Set Y` is a neighbourhood of `f x`, `x : X`,
then there exists a compact neighbourhood `K` of `x` such that `f` maps `K` to `s`.  -/
LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo : ∀ {X : Type u_3} {Y : Type u_4} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  [self : LocallyCompactPair X Y] {f : X → Y} {x : X} {s : Set Y},
  Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s
-- Init.Control.Except
/-- Recovers from exceptions thrown in the `Except ε` monad. Typically used via the `<|>` operator.

`Except.tryCatch` is a related operator that allows the recovery procedure to depend on _which_
exception was thrown.
 -/
Except.orElseLazy : {ε : Type u} → {α : Type u_1} → Except ε α → (Unit → Except ε α) → Except ε α
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E}, (∀ (i : ι), AnalyticOnNhd 𝕜 (f i) s) → AnalyticOnNhd 𝕜 (fun x x_1 => f x_1 x) s
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakSpace.coe_map : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : ContinuousAdd 𝕜] [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E]
  [inst_6 : TopologicalSpace E] [inst_7 : AddCommMonoid F] [inst_8 : Module 𝕜 F] [inst_9 : TopologicalSpace F]
  (f : E →L[𝕜] F), ⇑(WeakSpace.map f) = ⇑f
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.indep_empty : ∀ {α : Type u_2} (self : IndepMatroid α), self.Indep ∅
-- Mathlib.Data.Quot
Quotient.mk_out' : ∀ {α : Sort u_1} {s₁ : Setoid α} (a : α), s₁ (Quotient.mk'' a).out a
-- Mathlib.RingTheory.ZMod.UnitsCyclic
/-- The multiplicative group of `ZMod p` is cyclic.  -/
ZMod.isCyclic_units_prime : ∀ {p : ℕ}, Nat.Prime p → IsCyclic (ZMod p)ˣ
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.mk'_tmul : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_9)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid R) [inst_5 : IsLocalization M A] (s : S) (x : R)
  (y : ↥M),
  IsLocalization.mk' A x y ⊗ₜ[R] s =
    IsLocalization.mk' (TensorProduct R A S) ((algebraMap R S) x * s) ⟨(algebraMap R S) ↑y, ⋯⟩
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.isCompleteMultipartite_iff : ∀ {α : Type u} {G : SimpleGraph α},
  G.IsCompleteMultipartite ↔
    ∃ ι V, ∃ (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g SimpleGraph.completeMultipartiteGraph V)
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.statsFn : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → σ → Std.Format
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The cache for evaluating lean expressions of 1-morphisms into `Mor₁` terms.  -/
Mathlib.Tactic.BicategoryLike.State.cache : Mathlib.Tactic.BicategoryLike.State → Lean.PersistentExprMap Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Data.Ordering.Basic
/-- Construct an `Ordering` from a type with a decidable `LT` instance,
assuming that incomparable terms are `Ordering.eq`.
 -/
cmp : {α : Type u} → [inst : LT α] → [DecidableLT α] → α → α → Ordering
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.equivYoneda_hom_app_hom_apply_hom_apply : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S) (X : Type uᵒᵖ)
  (x : S.obj (Opposite.op (Opposite.unop X))) (x_1 : Opposite.unop X),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.equivYoneda S hs).hom.app X)) x))
      x_1 =
    (CategoryTheory.ConcreteCategory.hom (S.map (TypeCat.ofHom fun x => x_1).op)) x
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isRightDescent_iff_not_isRightDescent_mul : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpProdComm_symm : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], (IsometryEquiv.withLpProdComm p α β).symm = IsometryEquiv.withLpProdComm p β α
-- Mathlib.Geometry.Manifold.Notation
/-- Try to find a `ModelWithCorners` instance on a type (represented by an expression `e`),
using the local context to infer the appropriate instance. This supports the following cases:
- the model with corners on the total space of a vector bundle
- the model with corners on the tangent space of a manifold
- a model with corners on a manifold, or on its underlying model space
- a closed interval of real numbers (including the unit interval)
- Euclidean space, Euclidean half-space and Euclidean quadrants
- a metric sphere in a real or complex inner product space
- the units of a normed algebra
- the complex upper half plane
- a space of continuous k-linear maps
- the trivial model `𝓘(𝕜, E)` on a normed space
- if the above are not found, try to find a `NontriviallyNormedField` instance on the type of `e`,
  and if successful, return `𝓘(𝕜)`.

Further cases can be added as necessary.
This method intentionally handles **neither** sums (disjoint unions) nor products of spaces,
nor an open subset of an existing manifold. These are handled in `findModel`.

Return an expression describing the found model with corners, together with information about
whether the model is the trivial model with corners on a normed space. (This is important for
forming products of models.)

Note that the matching on `e` does not see through reducibility (e.g. we distinguish the `abbrev`
`TangentBundle` from its definition), so `whnfR` should not be run on `e` prior to calling
`findModel` on it.

This implementation is not maximally robust yet.
 -/
Manifold.Elab.findModelInner : Lean.Expr → Lean.Elab.TermElabM (Option Manifold.Elab.FindModelResult)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Antitone.const_mul : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [PosMulMono M₀], Antitone f → 0 ≤ a → Antitone fun x => a * f x
-- Mathlib.Analysis.Analytic.CPolynomial
HasFiniteFPowerSeriesAt.add : ∀ {𝕜 : 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] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {n m : ℕ},
  HasFiniteFPowerSeriesAt f pf x n →
    HasFiniteFPowerSeriesAt g pg x m → HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)