mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.Data
Aesop.tree : Aesop.TreeSpec
-- Lean.Elab.Command.Scope
Lean.Elab.Command.Scope.mk.inj : ∀ {header : String} {opts : Lean.Options} {currNamespace : Lean.Name} {openDecls : List Lean.OpenDecl}
  {levelNames : List Lean.Name} {varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)}
  {varUIds : Array Lean.Name} {includedVars omittedVars : List Lean.Name} {isNoncomputable isPublic isMeta : Bool}
  {attrs : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)} {header_1 : String} {opts_1 : Lean.Options}
  {currNamespace_1 : Lean.Name} {openDecls_1 : List Lean.OpenDecl} {levelNames_1 : List Lean.Name}
  {varDecls_1 : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)} {varUIds_1 : Array Lean.Name}
  {includedVars_1 omittedVars_1 : List Lean.Name} {isNoncomputable_1 isPublic_1 isMeta_1 : Bool}
  {attrs_1 : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)},
  { header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls, levelNames := levelNames,
        varDecls := varDecls, varUIds := varUIds, includedVars := includedVars, omittedVars := omittedVars,
        isNoncomputable := isNoncomputable, isPublic := isPublic, isMeta := isMeta, attrs := attrs } =
      { header := header_1, opts := opts_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        levelNames := levelNames_1, varDecls := varDecls_1, varUIds := varUIds_1, includedVars := includedVars_1,
        omittedVars := omittedVars_1, isNoncomputable := isNoncomputable_1, isPublic := isPublic_1, isMeta := isMeta_1,
        attrs := attrs_1 } →
    header = header_1 ∧
      opts = opts_1 ∧
        currNamespace = currNamespace_1 ∧
          openDecls = openDecls_1 ∧
            levelNames = levelNames_1 ∧
              varDecls = varDecls_1 ∧
                varUIds = varUIds_1 ∧
                  includedVars = includedVars_1 ∧
                    omittedVars = omittedVars_1 ∧
                      isNoncomputable = isNoncomputable_1 ∧ isPublic = isPublic_1 ∧ isMeta = isMeta_1 ∧ attrs = attrs_1
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instLE : {M : Type u_1} → [Group M] → [Lattice M] → LE (MulArchimedeanOrder M)
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrRight_trans : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} {A₃ : ι → Type u_7} [inst : CommSemiring R]
  [inst_1 : (i : ι) → Semiring (A₁ i)] [inst_2 : (i : ι) → Semiring (A₂ i)] [inst_3 : (i : ι) → Semiring (A₃ i)]
  [inst_4 : (i : ι) → Algebra R (A₁ i)] [inst_5 : (i : ι) → Algebra R (A₂ i)] [inst_6 : (i : ι) → Algebra R (A₃ i)]
  (e₁ : (i : ι) → A₁ i ≃ₐ[R] A₂ i) (e₂ : (i : ι) → A₂ i ≃ₐ[R] A₃ i),
  (AlgEquiv.piCongrRight e₁).trans (AlgEquiv.piCongrRight e₂) = AlgEquiv.piCongrRight fun i => (e₁ i).trans (e₂ i)
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Equiv.Perm.not_isSolvable_fin_5`. -/
Equiv.Perm.fin_5_not_solvable : ¬Group.IsSolvable (Equiv.Perm (Fin 5))
-- Mathlib.Topology.Connected.PathConnected
Joined.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x y : X), Joined x y = Nonempty (Path x y)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor is said to preserve finite colimits, if it preserves all colimits of
shape `J`, where `J : Type` is a finite category.
 -/
CategoryTheory.Limits.PreservesFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β) (h : ∀ {a b : α}, (↑f).toFun a ≤ (↑f).toFun b ↔ a ≤ b), { toAddEquiv := ↑f, map_le_map_iff' := h } = f
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left_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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  [inst_5 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : CategoryTheory.LocalizedMonoidal L W ε}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
            ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y Z)
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y Z))
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Localization.Monoidal.braidingNatIso L W ε).hom.app
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)).app
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
        h)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.sum_mk : ∀ {α : Type u} {L : List (α × Bool)} [inst : AddGroup α],
  (FreeGroup.mk L).sum = (List.map (fun x => bif x.2 then x.1 else -x.1) L).sum
-- Lean.Environment
/-- Environment fields that are not used often.  -/
Lean.EnvironmentHeader : Type
-- Mathlib.SetTheory.Cardinal.Basic
/-- To prove an inequality between the lifts to a common universe of two different supremums,
it suffices to show that the lift of each cardinal from the smaller supremum
if bounded by the lift of some cardinal from the larger supremum.
 -/
Cardinal.lift_iSup_le_lift_iSup : ∀ {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{w}} {f' : ι' → Cardinal.{w'}},
  BddAbove (Set.range f) →
    BddAbove (Set.range f') →
      ∀ {g : ι → ι'},
        (∀ (i : ι), Cardinal.lift.{w', w} (f i) ≤ Cardinal.lift.{w, w'} (f' (g i))) →
          Cardinal.lift.{w', w} (iSup f) ≤ Cardinal.lift.{w, w'} (iSup f')
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
CategoryTheory.Bicategory.isRightAdjoint_TFAE : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (u : b ⟶ a),
  [CategoryTheory.Bicategory.IsRightAdjoint u,
      CategoryTheory.Bicategory.HasAbsLeftKanLift u (CategoryTheory.CategoryStruct.id a),
      ∃ (x : CategoryTheory.Bicategory.HasLeftKanLift u (CategoryTheory.CategoryStruct.id a)),
        CategoryTheory.Bicategory.LanLift.CommuteWith u (CategoryTheory.CategoryStruct.id a) u].TFAE
-- Lean.Meta.Tactic.Grind.CollectParams
Lean.Meta.Grind.TParam : Type
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The morphism between the midpoints of the factorizations.  -/
CategoryTheory.Factorisation.Hom.h : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → {d e : CategoryTheory.Factorisation f} → d.Hom e → (d.mid ⟶ e.mid)
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- Formal multilinear series associated to the iterated derivative, defined by iterating
`p ↦ p.derivSeries` and currying suitably. It is defined so that, if a function has `p` as a power
series, then its iterated derivative of order `k` has `p.iteratedFDerivSeries k` as a power
series.  -/
FormalMultilinearSeries.iteratedFDerivSeries : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                FormalMultilinearSeries 𝕜 E F → (k : ℕ) → FormalMultilinearSeries 𝕜 E (E [×k]→L[𝕜] F)
-- Lean.Parser.Command
Lean.Parser.Command.evalBang.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionHomologyIso_hom_homologyι : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom
      (K.homologyι j') =
    CategoryTheory.CategoryStruct.comp ((K.restriction e).homologyι j)
      (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.mk.sizeOf_spec : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A}
  [inst_2 : SizeOf ι] [inst_3 : SizeOf A] [inst_4 : SizeOf σ] (deg : ι) (num den : ↥(𝒜 deg)) (den_mem : ↑den ∈ x),
  sizeOf { deg := deg, num := num, den := den, den_mem := den_mem } =
    1 + sizeOf deg + sizeOf num + sizeOf den + sizeOf den_mem
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_iSup : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_7} (S : ι → AddSubmonoid G), -⨆ i, S i = ⨆ i, -S i
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `N` is flat,
if any two elements of `↥(M ⊓ N)` are commutative, then the rank of `↥(M ⊓ N)` is at most one.  -/
Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ [Module.Flat R ↥N], (∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n) → Module.rank R ↥(M ⊓ N) ≤ 1
-- Mathlib.RingTheory.Congruence.Hom
/-- The homomorphism induced on the quotient of a ring by the kernel of a ring homomorphism.  -/
RingCon.kerLiftₐ : {M : Type u_1} →
  {P : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring M] →
          [inst_2 : Algebra R M] →
            [inst_3 : Semiring P] →
              [inst_4 : Algebra R P] → (f : M →ₐ[R] P) → (RingCon.ker f.toRingHom).Quotient →ₐ[R] P
-- Init.Data.Fin.Fold
Fin.foldl_succ : ∀ {α : Sort u_1} {n : ℕ} (f : α → Fin (n + 1) → α) (x : α),
  Fin.foldl (n + 1) f x = Fin.foldl n (fun x i => f x i.succ) (f x 0)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- The logarithmic Mahler measure of a polynomial `p` defined as
`(2 * π)⁻¹ * ∫ x ∈ (0, 2 * π), log ‖p (e ^ (i * x))‖`  -/
Polynomial.logMahlerMeasure : Polynomial ℂ → ℝ
-- Mathlib.Tactic.Convert
Convert.CheapConfig.mk.sizeOf_spec : ∀ (toConfig : Congr!.Config), sizeOf { toConfig := toConfig } = 1 + sizeOf toConfig
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- **Alias** of `LipschitzWith.mapsTo_eball`. -/
LipschitzWith.mapsTo_emetric_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → K ≠ 0 → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.eball x r) (Metric.eball (f x) (↑K * r))
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- The power of a point is nonpositive if and only if the point lies inside or on the sphere.  -/
EuclideanGeometry.Sphere.power_nonpos_iff_dist_center_le_radius : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P},
  0 ≤ s.radius → (s.power p ≤ 0 ↔ dist p s.center ≤ s.radius)
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.instDecidableEqPairwise : {ι : Type u_1} → [DecidableEq ι] → DecidableEq (CategoryTheory.Pairwise ι)
-- Std.Http.Protocol.H1.Reader
/-- Resets the reader to parse a new message on the same connection.
 -/
Std.Http.Protocol.H1.Reader.reset : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.mem_filter_iff : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α},
  U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U
-- Std.Http.Internal.IndexMultiMap
_private.Std.Http.Internal.IndexMultiMap.0.Std.Internal.IndexMultiMap.insert.match_1.eq_2 : ∀ (motive : Option (Array ℕ) → Sort u_1) (h_1 : (idxs : Array ℕ) → motive (some idxs)) (h_2 : Unit → motive none),
  (match none with
    | some idxs => h_1 idxs
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.Flat.Equalizer
/-- A property `P` of ring homomorphisms is said to have stable equalizers, if the equalizer
of algebra maps between algebras with structure morphisms satisfying `P`, is preserved by
arbitrary base change.
 -/
RingHom.HasStableEqualizers : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Data.ENat.Lattice
ENat.natCast_iSup : ∀ {ι : Sort u_1} {f : ι → ℕ}, BddAbove (Set.range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dHomologyData_right_p : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7),
  (X.dHomologyData f₁ f₂ f₃ f₄ f₅ f₆ f₇ f₂₃ h₂₃ f₅₆ h₅₆ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).right.p =
    X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ h₅₆) n₁ n₂ n₃ ⋯ ⋯
-- Mathlib.Algebra.Order.Ring.Idempotent
mul_eq_zero_add_eq_one_ext_right : ∀ {R : Type u_1} [inst : CommSemiring R] {a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }}, (↑a).2 = (↑b).2 → a = b
-- Mathlib.MeasureTheory.VectorMeasure.Prod
/-- The product of two vector measures when the first one has finite variation, obtained by
integrating the measure of the fibers, as in the definition of the product of positive measures.
*Do not use*: This is only used to instantiate the typeclass `HasProd`. Instead, use `μ.prod ν B`,
which uses the typeclass instance.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.Prod.0.MeasureTheory.VectorMeasure.prodOfIsFiniteMeasureLeft : {X : Type u_2} →
  {Y : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          {mX : MeasurableSpace X} →
            {mY : MeasurableSpace Y} →
              [inst : NormedAddCommGroup E] →
                [inst_1 : NormedSpace ℝ E] →
                  [inst_2 : NormedAddCommGroup F] →
                    [inst_3 : NormedSpace ℝ F] →
                      [inst_4 : NormedAddCommGroup G] →
                        [inst_5 : NormedSpace ℝ G] →
                          (μ : MeasureTheory.VectorMeasure X E) →
                            MeasureTheory.VectorMeasure Y F →
                              (E →L[ℝ] F →L[ℝ] G) →
                                [MeasureTheory.IsFiniteMeasure μ.variation] → MeasureTheory.VectorMeasure (X × Y) G
-- Init.Data.UInt.Bitwise
UInt64.ofFin_and : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a &&& b) = UInt64.ofFin a &&& UInt64.ofFin b
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_add_cons : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α),
  Matrix.vecCons x v + Matrix.vecCons y w = Matrix.vecCons (x + y) (v + w)
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- If `it` is an iterator, then `it.map f` is another iterator that applies a
function `f` to all values emitted by `it` and emits the result.

In situations where `f` is monadic, use `mapM` instead.

**Marble diagram:**

```text
it         ---a --b --c --d -e ----⊥
it.map     ---a'--b'--c'--d'-e'----⊥
```

(given that `f a = a'`, `f b = b'` etc.)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.IterM.map : {α β γ : Type w} →
  {m : Type w → Type w'} → [Std.Iterator α m β] → [inst : Monad m] → (f : β → γ) → Std.IterM m β → Std.IterM m γ
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The whole `R`-module `M` (viewed as the top convex cone) is generating.  -/
ConvexCone.isGenerating_top : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ⊤.IsGenerating
-- Init.Data.String.Pattern.Basic
/-- The start position of a `SearchStep`.  -/
String.Slice.Pattern.SearchStep.startPos : {s : String.Slice} → String.Slice.Pattern.SearchStep s → s.Pos
-- Mathlib.Data.Rat.Defs
Rat.divInt_one : ∀ (n : ℤ), Rat.divInt n 1 = ↑n
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Ici_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ici ↑a = WithTop.some '' Set.Ici a ∪ {⊤}
-- Mathlib.NumberTheory.Dioph
Dioph.dom_dioph : ∀ {α : Type u} {f : (α → ℕ) →. ℕ}, Dioph.DiophPFun f → Dioph f.Dom
-- Mathlib.Order.SuccPred.Basic
succ_notMem_iff_isMax : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α} [s.OrdConnected] [inst_2 : SuccOrder α] [NoMaxOrder α] {a : ↑s},
  Order.succ ↑a ∉ s ↔ IsMax a
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.neg_mulExpNegMulSq_neg : ∀ (ε x : ℝ), -ε.mulExpNegMulSq (-x) = ε.mulExpNegMulSq x
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Iio_add_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∑ i < a + 1, f i = ∑ i < a, f i + f a
-- Mathlib.Data.Num.ZNum
ZNum.succ.eq_2 : ∀ (a : PosNum), (ZNum.pos a).succ = ZNum.pos a.succ
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- The initial object of `Top` is `PEmpty`.  -/
TopCat.isInitialPEmpty : CategoryTheory.Limits.IsInitial (TopCat.of PEmpty.{u + 1})
-- Mathlib.Order.Lattice
instIdempotentOpMin_mathlib : ∀ {α : Type u} [inst : SemilatticeInf α], Std.IdempotentOp fun x1 x2 => x1 ⊓ x2
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listEncode.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (i : α)
  (h_1 : (i : α) → motive (FirstOrder.Language.var i))
  (h_2 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.var i with
    | FirstOrder.Language.var i => h_1 i
    | FirstOrder.Language.func f ts => h_2 l f ts) =
    h_1 i
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_1.eq : ∀ {motive_1 : Lean.Widget.MsgEmbed → Sort u} {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u}
  {motive_3 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
      Sort u}
  {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) (F_1 : (t : Lean.Widget.MsgEmbed) → t.below → motive_1 t)
  (F_2 : (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t)
  (F_3 :
    (t :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
          (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
      Lean.Widget.MsgEmbed.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_4 t → motive_5 t),
  Lean.Widget.MsgEmbed.brecOn_1 t F_1 F_2 F_3 F_4 F_5 = F_2 t (Lean.Widget.MsgEmbed.brecOn_1.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.Data.ENat.Lattice
ENat.add_sInf : ∀ {a : ℕ∞} {s : Set ℕ∞}, a + sInf s = ⨅ b ∈ s, a + b
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.Nonsingular.mono : ∀ {X : SSet} [self : X.Nonsingular] {n : ℕ} (x : ↑(X.nonDegenerate n)), CategoryTheory.Mono (SSet.yonedaEquiv.symm ↑x)
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- A left adjoint functor `L : C ⥤ D` is *comonadic* if the comparison functor `Comonad.comparison L`
from `C` to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.
 -/
CategoryTheory.ComonadicLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + (i + 1) = m) CategoryTheory.SimplicialObject.σ₀Iter_succ._auto_1),
  X.σ₀Iter (i + 1) h = CategoryTheory.CategoryStruct.comp (X.σ 0) (X.σ₀Iter i ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- A term of type `HomComplex.Triplet n` consists of two integers `p` and `q`
such that `p + n = q`. (This type is introduced so that the instance
`AddCommGroup (Cochain F G n)` defined below can be found automatically.)  -/
CochainComplex.HomComplex.Triplet : ℤ → Type
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n) {x : M}, ContMDiffAt I I' n (⇑h) x