mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Combinators.FlatMap
/-- Let `it₁` and `it₂` be iterators and `f` a function mapping `it₁`'s outputs to iterators
of the same type as `it₂`. Then `it₁.flatMapAfter f it₂` first goes over `it₂` and then over
`it₁.flatMap f it₂`, emitting all their values.

The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator
that is currently iterating over one of the inner iterators.

**Marble diagram:**

```text
it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfter  f it₂   a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
* `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
iterator.

For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
Std.Iter.flatMapAfter : {α β α₂ γ : Type w} →
  [Std.Iterator α Id β] → [Std.Iterator α₂ Id γ] → (f : β → Std.Iter γ) → Std.Iter β → Option (Std.Iter γ) → Std.Iter γ
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_zero_iff_hasNoetherianRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {u : V →ₗ[K] V₂}, u ≈ 0 ↔ u.HasNoetherianRange
-- Mathlib.Topology.Spectral.ConstructibleTopology
isCompact_of_mem_constructibleTopologySubbasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] {s : Set X},
  s ∈ constructibleTopologySubbasis X → IsCompact s
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.Pattern.Model.posFind?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {σ : String.Slice → Type}
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id]
  [inst_4 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_6 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat] {s : String.Slice} {pos : s.Pos},
  pos.find? pat = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ¬String.Slice.Pattern.Model.MatchesAt pat pos'
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_bounded : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → β} {C : ℝ},
  (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Combinatorics.Hindman
Hindman.FS_iter_tail_sub_FS : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (n : ℕ), Hindman.FS (Stream'.drop n a) ⊆ Hindman.FS a
-- Mathlib.Analysis.Complex.Norm
Complex.lim_conj : ∀ (f : CauSeq ℂ fun x => ‖x‖), (Complex.cauSeqConj f).lim = (starRingEnd ℂ) f.lim
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.PostShape.args.match_1.splitter : (motive : Std.Do.PostShape → Sort u_2) →
  (x : Std.Do.PostShape) →
    (Unit → motive Std.Do.PostShape.pure) →
      ((σ : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.arg σ s)) →
        ((ε : Type u_1) → (s : Std.Do.PostShape) → motive (Std.Do.PostShape.except ε s)) → motive x
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instPartialOrder : {α : Type u_1} → PartialOrder (MeasureTheory.OuterMeasure α)
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.L.congr_simp : ∀ {Γ Γ_1 : Subgroup (GL (Fin 2) ℝ)} (e_Γ : Γ = Γ_1) [inst : Γ.IsArithmetic] {k k_1 : ℤ} (e_k : k = k_1) (hk : 0 < k)
  {F : Type u_1} [inst_1 : FunLike F UpperHalfPlane ℂ] (f f_1 : F),
  f = f_1 → ∀ [inst_2 : ModularFormClass F Γ k] (s s_1 : ℂ), s = s_1 → ModularForm.L hk f s = ModularForm.L ⋯ f_1 s_1
-- Mathlib.Algebra.Group.Ext
CancelCommMonoid.mk.hcongr_3 : ∀ (M M' : Type u),
  M = M' →
    ∀ (toCommMonoid : CommMonoid M) (toCommMonoid' : CommMonoid M'),
      toCommMonoid ≍ toCommMonoid' →
        ∀ (toIsLeftCancelMul : IsLeftCancelMul M) (toIsLeftCancelMul' : IsLeftCancelMul M'),
          toIsLeftCancelMul ≍ toIsLeftCancelMul' →
            { toCommMonoid := toCommMonoid, toIsLeftCancelMul := toIsLeftCancelMul } ≍
              { toCommMonoid := toCommMonoid', toIsLeftCancelMul := toIsLeftCancelMul' }
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
isQuasiregular_zero : IsQuasiregular 0
-- Mathlib.Order.Closure
ClosureOperator.monotone : ∀ {α : Type u_1} [inst : Preorder α] (c : ClosureOperator α), Monotone ⇑c
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `not_covBy_iff`.

---

If `a < b`, then `b` does not cover `a` iff there's an element in between.  -/
exists_lt_lt_of_not_covBy : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → ¬a ⋖ b → ∃ c, a < c ∧ c < b
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.setFunIndInfo : Lean.Meta.FunIndInfo → Lean.CoreM Unit
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.WithWF.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {γ : Type x}
  {PlausibleForInStep : β → γ → ForInStep γ → Prop} {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep}
  {it : Std.IterM m β} {acc : γ} {it_1 : Std.IterM m β} {acc_1 : γ},
  { it := it, acc := acc } = { it := it_1, acc := acc_1 } → it = it_1 ∧ acc = acc_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false → ∀ {k fallback : α}, (cmp k (t.minD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_zero_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i j : Set α},
  MeasurableSet i →
    j ⊆ i →
      v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i → v.restrict j ≤ MeasureTheory.VectorMeasure.restrict 0 j
-- Init.Data.Nat.Lcm
Nat.dvd_lcm_right : ∀ (m n : ℕ), n ∣ m.lcm n
-- Mathlib.Order.RelClasses
Prod.wellFoundedLT : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [WellFoundedLT α] [inst_2 : Preorder β] [WellFoundedLT β],
  WellFoundedLT (α × β)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- If `α` and `β` are two equal natural transformations, then the functors of algebras induced by them
are isomorphic.
We define it like this as opposed to using `eq_to_iso` so that the components are nicer to prove
lemmas about.
 -/
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      {α β : F ⟶ G} →
        α = β →
          (CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α ≅
            CategoryTheory.Endofunctor.Algebra.functorOfNatTrans β)
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFacAux_has_prop : ∀ {n : ℕ}, 2 ≤ n → ∀ (k i : ℕ), k = 2 * i + 3 → (∀ (m : ℕ), 2 ≤ m → m ∣ n → k ≤ m) → Nat.minFacProp✝ n (n.minFacAux k)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- If a free module is of finite rank, then the cardinality of any basis is equal to its
`finrank`.  -/
Module.mk_finrank_eq_card_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {ι : Type w} (h : Module.Basis ι R M), ↑(Module.finrank R M) = Cardinal.mk ι
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.Raw.getKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α → α
-- Lean.Setup
Lean.instToJsonModuleHeader.toJson : Lean.ModuleHeader → Lean.Json
-- Mathlib.CategoryTheory.Limits.Creates
/-- A helper to show a functor creates limits. In particular, if we can show
that for any limit cone `c` for `K ⋙ F`, there is a lift of it which is
a limit and `F` reflects isomorphisms, then `F` creates limits.
Usually, `F` creating limits says that _any_ lift of `c` is a limit, but
here we only need to show that our particular lift of `c` is a limit.
 -/
CategoryTheory.LiftsToLimit : {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) →
                (c : CategoryTheory.Limits.Cone (K.comp F)) →
                  CategoryTheory.Limits.IsLimit c → Type (max (max (max u₁ v₁) v₂) w)
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm_one : ∀ {α : Type u_4} (p : α → Prop) (h : optParam (∀ (x : α), p (1 x) ↔ p (1 x)) ⋯), Equiv.Perm.subtypePerm 1 h = 1
-- Init.Data.Iterators.Basic
/-- This structure provides a more convenient way to define `Productive α m` instances using
`Productive.of_productivenessRelation : ProductivenessRelation α m → Productive α m`.
 -/
Std.Iterators.ProductivenessRelation : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Type w
-- Mathlib.Algebra.Category.CommBialgCat
/-- Forgetting to the underlying type and then building the bundled object returns the original
bialgebra.  -/
CommBialgCat.ofIsoSelf : {R : Type u} → [inst : CommRing R] → (M : CommBialgCat R) → CommBialgCat.of R ↑M ≅ M
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.comp_continuousOn : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ},
  IsLocalMin f (g b) → ContinuousOn g s → b ∈ s → IsLocalMinOn (f ∘ g) s b
-- Mathlib.RingTheory.IsTensorProduct
_private.Mathlib.RingTheory.IsTensorProduct.0.IsTensorProduct.assocAux_tmul : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] (f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (hg : IsTensorProduct g)
  (x₁ : M₁) (x₂ : M₂) (x₃ : M₃), (IsTensorProduct.assocAux✝ f hf g hg) ((f x₁) x₂ ⊗ₜ[S] x₃) = x₁ ⊗ₜ[R] (g x₂) x₃
-- Mathlib.GroupTheory.Schreier
card_dvd_exponent_nsmul_rank' : ∀ (G : Type u_1) [inst : AddCommGroup G] [inst_1 : AddGroup.FG G] {n : ℕ},
  (∀ (g : G), n • g = 0) → Nat.card G ∣ n ^ AddGroup.rank G
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A).obj x = A.X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv s.fst = t.snd
-- Mathlib.Algebra.Field.Basic
add_self_div_two : ∀ {K : Type u_1} [inst : DivisionSemiring K] [NeZero 2] (a : K), (a + a) / 2 = a
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} (hk : k < n) (hk' : k' < n) (j : (X k hk).fst) (j' : (X k' hk').fst)
  (a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j') (k_1 k'_1 : ℕ) (hk_1 : k_1 < n) (hk'_1 : k'_1 < n)
  (j_1 : (X k_1 hk_1).fst) (j'_1 : (X k'_1 hk'_1).fst) (a_2 a_3 : (X k_1 hk_1).snd j_1 ⟶ (X k'_1 hk'_1).snd j'_1),
  (CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq✝ hk hk' j j' a a_1 =
      CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq✝ hk_1 hk'_1 j_1 j'_1 a_2 a_3) =
    (k = k_1 ∧ k' = k'_1 ∧ j ≍ j_1 ∧ j' ≍ j'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3)
-- Lean.Environment
Lean.Environment.displayStats : Lean.Environment → IO Unit
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.continuous_map : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} {Y : Type u_3} [inst_2 : Fintype X]
  [inst_3 : Fintype Y] [inst_4 : IsOrderedRing S] [inst_5 : TopologicalSpace S] [IsTopologicalSemiring S] (f : X → Y),
  Continuous (stdSimplex.map f)
-- Mathlib.Order.Filter.Lift
Filter.lift_lift'_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Set β} {h : Set β → Filter γ},
  Monotone g → Monotone h → (f.lift' g).lift h = f.lift fun s => h (g s)
-- Lean.Util.Diff
/-- Add an element from the right array to a histogram  -/
Lean.Diff.Histogram.addRight : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {lsize rsize : ℕ} → Lean.Diff.Histogram α lsize rsize → Fin rsize → α → Lean.Diff.Histogram α lsize rsize
-- Mathlib.Data.Int.Cast.Defs
/-- The canonical map `ℕ → R` sends `0 : ℕ` to `0 : R`.  -/
AddCommGroupWithOne.natCast_zero : ∀ {R : Type u} [self : AddCommGroupWithOne R], ↑0 = 0
-- Mathlib.Data.Set.Image
Set.preimage_subtype_coe_eq_compl : ∀ {α : Type u_1} {s u v : Set α}, s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ
-- Aesop.Options.Public
/-- Depth-first search. Whenever a rule is applied, Aesop immediately tries to
solve each of its subgoals (from left to right), up to the maximum rule
application depth. Goal and rule priorities are ignored, except to decide
which rule is applied first.
 -/
Aesop.Strategy.depthFirst : Aesop.Strategy
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.map_neg : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂},
  IsLinearMap R f → ∀ (x : M), f (-x) = -f x
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.smulConst_symm_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalTorsor P] (p p' : P), (Homeomorph.smulConst p).symm p' = p' /ₛ p
-- Mathlib.Algebra.GradedMonoid
/-- The homogeneous multiplication map `mul`  -/
GradedMonoid.GMul.mul : {ι : Type u_1} → {A : ι → Type u_2} → {inst : Add ι} → [self : GradedMonoid.GMul A] → {i j : ι} → A i → A j → A (i + j)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.EqOnSource.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β),
  e.EqOnSource e' = (e.source = e'.source ∧ Set.EqOn (↑e) (↑e') e.source)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α},
  t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Order.Hom.Set
OrderIso.preimage_image : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set α), ⇑e ⁻¹' ⇑e '' s = s
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.inducedFunctor_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] (F : C → D) (a : C),
  (CategoryTheory.inducedFunctor F).obj a = F a
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_eq_floor : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a b = ⌊(b - a) / p⌋
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.signatures : Lean.Lsp.SignatureHelp → Array Lean.Lsp.SignatureInformation
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.hasSum_sub : ∀ {𝕜 : 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 : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ∀ {y : E}, y ∈ insert x s ∩ Metric.eball x r → HasSum (fun n => (p n) fun x_1 => y - x) (f y)
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- Construct the left adjoint to `R`, with object map `constructLeftAdjointObj`.  -/
CategoryTheory.LiftLeftAdjoint.constructLeftAdjoint : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor B C} →
              {F : CategoryTheory.Functor C B} →
                (R : CategoryTheory.Functor A B) →
                  (F' : CategoryTheory.Functor C A) →
                    (adj₁ : F ⊣ U) →
                      (F' ⊣ R.comp U) →
                        [CategoryTheory.Limits.HasReflexiveCoequalizers A] →
                          ((X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) → CategoryTheory.Functor B A
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.indepNum.eq_1 : ∀ {α : Type u_3} (G : SimpleGraph α), G.indepNum = sSup {n | ∃ s, G.IsNIndepSet n s}
-- Mathlib.Algebra.Regular.Basic
/-- A product is regular if and only if the factors are.  -/
isRegular_mul_iff : ∀ {R : Type u_1} [inst : CommSemigroup R] {a b : R}, IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.constantCommuteCompose_hom_app_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (X : D),
  ((CategoryTheory.constantCommuteCompose J U).hom.app X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.sheafifyComposeIso J U ((CategoryTheory.Functor.const Cᵒᵖ).obj X)).inv
      (CategoryTheory.sheafifyMap J (CategoryTheory.Functor.constComp Cᵒᵖ X U).hom)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomHomLeftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.AddMonObj X],
  CategoryTheory.IsAddMonHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Iso_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B}
  (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse)
  (hα'α :
    CategoryTheory.CategoryStruct.comp S.leftUnitor.hom
        (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv
          (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S)
        (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom
          (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α')
            (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv
              (CategoryTheory.Functor.whiskerRight α G.inverse)))))
  (hαα' :
    CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor)
            (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom
              (U.whiskerLeft G.counitIso.hom)))) =
      CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U)
          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv)))
  (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T)
  (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T)
  (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V),
  (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).inverse =
    CategoryTheory.CostructuredArrow.map₂ α' β'
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_right_inj_of_comparable : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] {a b c : α},
  b ≤ c ∨ c ≤ b → (a + c = a + b ↔ c = b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.ofList l cmp) k' fallback = v
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.hasPullback_of_left : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.HasPullback f g
-- Batteries.Data.Float.Basic
/-- The floating point value "not a number", used to represent erroneous numerical computations
such as `0 / 0`. Using `nan` in any float operation will return `nan`, and all comparisons
involving `nan` return `false`, including in particular `nan == nan`.
 -/
Float32.nan : Float32
-- Aesop.Rule.Name
Aesop.BuilderName.instToString : ToString Aesop.BuilderName
-- Mathlib.Lean.Expr.Basic
/-- If `e` has a structure as type with field `fieldName` (either directly or in a parent
structure), `mkProjection e fieldName` creates the projection expression `e.fieldName`  -/
Lean.Expr.mkProjection : Lean.Expr → Lean.Name → Lean.MetaM Lean.Expr