mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeftLinearMap_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N),
  AlternatingMap.curryLeftLinearMap f = f.curryLeft
-- Mathlib.Order.Filter.Extr
IsMinOn.iInf_eq : ∀ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLinearOrder α] {f : β → α} {s : Set β} {x₀ : β},
  x₀ ∈ s → IsMinOn f s x₀ → ⨅ x, f ↑x = f x₀
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_le_max : ∀ (R : Type u) [inst : CommSemiring R] (X : Type u),
  Cardinal.mk (FreeAlgebra R X) ≤ max (max (Cardinal.mk R) (Cardinal.mk X)) Cardinal.aleph0
-- Init.SimpLemmas
or_self_right : ∀ {a b : Prop}, (a ∨ b) ∨ b ↔ a ∨ b
-- Mathlib.MeasureTheory.Function.Jacobian
/-- If a function is differentiable and injective on a measurable set,
then the image is measurable.  -/
MeasureTheory.measurable_image_of_fderivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E],
  MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → Set.InjOn f s → MeasurableSet (f '' s)
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections],
  CommGrpCat.limitCone F =
    CategoryTheory.liftLimit (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)))
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.ae_eq : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : TopologicalSpace ε] {f g : α → ε}, f =ᵐ[μ] g → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → Std.DTreeMap.Raw.Const.getD (m₁ \ m₂) k fallback = fallback
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.pow_inv_comm' : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (m n : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_self_add : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] {a b : α}, a ≤ a + b
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.all_filterMapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Monad m] [inst_4 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → m (Option β')} {p : β' → Bool},
  Std.IterM.all p (Std.Iter.filterMapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        match __do_lift with
          | some fx => pure { down := p fx }
          | none => pure { down := true })
      (Std.Iter.mapM pure it)
-- Lean.Elab.Do.Legacy
/-- Helper method for annotating `term` with the raw syntax `ref`.
We use this method to implement finer-grained term infos for `do`-blocks.

We use `withRef term` to make sure the synthetic position for the `with_annotate_term` is equal
to the one for `term`. This is important for producing error messages when there is a type mismatch.
Consider the following example:
```
opaque f : IO Nat

def g : IO String := do
  f
```
There is at type mismatch at `f`, but it is detected when elaborating the expanded term
containing the `with_annotate_term .. f`. The current `getRef` when this `annotate` is invoked
is not necessarily `f`. Actually, it is the whole `do`-block. By using `withRef` we ensure
the synthetic position for the `with_annotate_term ..` is equal to `term`.
Recall that synthetic positions are used when generating error messages.
 -/
Lean.Elab.Term.Do.annotate : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → [Lean.MonadQuotation m] → Lean.Syntax → Lean.Syntax → m Lean.Syntax
-- Std.Http.Data.URI.Basic
/-- No `:` port separator is present (for example, `example.com`).
 -/
Std.Http.URI.Port.omitted : Std.Http.URI.Port
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.cmd : LeanSearchClient.SearchServer → String
-- Init.Meta.Defs
Lean.isLetterLike : Char → Bool
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.instSubalgebraToSubmodule : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] (A : Subalgebra R S)
  [Module.Flat R ↥A], Module.Flat R ↥(Subalgebra.toSubmodule A)
-- Mathlib.Algebra.GroupWithZero.TransferInstance
/-- Transfer `MulZeroClass` across an `Equiv`  -/
Equiv.mulZeroClass : {α : Type u} → {β : Type v} → α ≃ β → [MulZeroClass β] → MulZeroClass α
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_ne_bot_of_nontrivial : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M],
  Module.supportDim R M ≠ ⊥
-- Mathlib.Data.Int.Log
/-- `zpow b` and `Int.log b` (almost) form a Galois connection.  -/
Int.lt_zpow_iff_log_lt : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (r < ↑b ^ x ↔ Int.log b r < x)
-- Init.Data.SInt.Bitwise
Bool.toBitVec_toInt32 : ∀ {b : Bool}, b.toInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulSpanning.maximal_isMulPointed : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.IsMulPointed → M.IsMulSpanning → Maximal Submonoid.IsMulPointed M
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.le_mul_iff_one_le_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : MulOneClass α] [IsMulCommutative α] [MulLeftMono α] {a b : α},
  MulLECancellable a → (a ≤ b * a ↔ 1 ≤ b)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- This is a slightly more convenient method to verify that a pullback cone is a weak limit cone.
It only asks for a proof of facts that carry any mathematical content  -/
CategoryTheory.Limits.PullbackCone.isWeakLimitAux : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (t : CategoryTheory.Limits.PullbackCone f g) →
            (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ t.pt) →
              (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                  CategoryTheory.CategoryStruct.comp (lift s) t.fst = s.fst) →
                (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                    CategoryTheory.CategoryStruct.comp (lift s) t.snd = s.snd) →
                  CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.skeletonEquivalence_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.skeletonEquivalence C).unitIso =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.InducedCategory.isoMk (Nonempty.some ⋯).symm) ⋯
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (a : List α) (a_1 : β)
  (a_2 : List β),
  List.scanAuxM.go✝ f a a_1 a_2 =
    match a, a_1, a_2 with
    | [], last, acc => pure (last :: acc)
    | x :: xs, last, acc => do
      let __do_lift ← f last x
      List.scanAuxM.go✝ f xs __do_lift (last :: acc)
-- Lean.Elab.DocString
/-- Elaborates a sequence of blocks into a document.  -/
Lean.Doc.elabBlocks : Lean.TSyntaxArray `block →
  Lean.Doc.DocM
    (Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) × Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.factorThru.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P X E : C} [inst_1 : CategoryTheory.Projective P]
  (f f_1 : P ⟶ X),
  f = f_1 →
    ∀ (e e_1 : E ⟶ X) (e_e : e = e_1) [inst_2 : CategoryTheory.Epi e],
      CategoryTheory.Projective.factorThru f e = CategoryTheory.Projective.factorThru f_1 e_1
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.testTrueHelper : ∀ (p : ℕ), Nat.blt 1 p = true → LucasLehmer.norm_num_ext.sModNatTR (2 ^ p - 1) (p - 2) = 0 → LucasLehmerTest p
-- Mathlib.CategoryTheory.Comma.Basic
/-- A morphism between two objects in the comma category is a commutative square connecting the
morphisms coming from the two objects using morphisms in the image of the functors `L` and `R`.
 -/
CategoryTheory.CommaMorphism : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} → CategoryTheory.Comma L R → CategoryTheory.Comma L R → Type (max v₁ v₂)
-- Mathlib.Algebra.Exact.Basic
MonoidHom.mulExact_of_comp_eq_one_of_ker_le_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] {f : M →* N}
  {g : N →* P}, g.comp f = 1 → g.ker ≤ f.range → Function.MulExact ⇑f ⇑g
-- Mathlib.FieldTheory.Laurent
RatFunc.taylor_mem_nonZeroDivisors : ∀ {R : Type u} [inst : CommRing R] (r : R),
  ∀ p ∈ nonZeroDivisors (Polynomial R), (Polynomial.taylor r) p ∈ nonZeroDivisors (Polynomial R)
-- Mathlib.Tactic.Attr.Register
/-- A simp set for the `pnat_to_nat` tactic.  -/
Parser.Attr.pnat_to_nat_coe : Lean.ParserDescr
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily
distinct!), then the size of `s` divides the size of `s + t`.  -/
Finset.card_dvd_card_add_left : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
  ((fun b => Finset.image (fun a => a + b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s + t).card
-- Mathlib.LinearAlgebra.FreeProduct.Basic
_private.Mathlib.LinearAlgebra.FreeProduct.Basic.0.LinearAlgebra.FreeProduct.rel.match_1.splitter : (motive : Fin 2 → Sort u_1) → (x : Fin 2) → (Unit → motive 0) → (Unit → motive 1) → motive x
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.dotProduct_of_isEmpty : ∀ {α : Type u} {n' : Type uₙ} [inst : AddCommMonoid α] [inst_1 : Mul α] [inst_2 : Fintype n'] [IsEmpty n']
  (v w : n' → α), v ⬝ᵥ w = 0
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.symm_trans_self : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  e.symm.trans e = AddConstEquiv.refl b
-- Mathlib.RingTheory.LocalProperties.Projective
Module.projective_of_isLocalizedModule : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {Rₛ : Type u_4}
  {Mₛ : Type u_5} [inst_3 : AddCommGroup Mₛ] [inst_4 : Module R Mₛ] [inst_5 : CommRing Rₛ] [inst_6 : Algebra R Rₛ]
  [inst_7 : Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ]
  [IsLocalizedModule S f] [Module.Projective R M], Module.Projective Rₛ Mₛ
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.coe_embedding : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length) (j : Fin (c.blocksFun i)), ↑((c.embedding i) j) = c.sizeUpTo ↑i + ↑j
-- Mathlib.Algebra.Algebra.Bilinear
AlgHom.comp_mul' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  f.toLinearMap ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.toList_iter : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iter.toList = xs.toList
-- Mathlib.Data.List.Cycle
/-- A `s : Cycle α` that is at most one element.  -/
Cycle.Subsingleton : {α : Type u_1} → Cycle α → Prop
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.preprocess : Aesop.RuleTacDescr
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- We can turn `hσ` into a datum that can be passed to `nullHomotopicMap'`.  -/
AlgebraicTopology.DoldKan.hσ' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        ℕ →
          (n m : ℕ) →
            AlgebraicTopology.DoldKan.c.Rel m n →
              ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶
                (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X m)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeWhisker_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C}
  {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F},
  H.mapConeWhisker.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.id.eq_1 : ∀ (M : Type u_10) [inst : One M], OneHom.id M = { toFun := fun x => x, map_one' := ⋯ }
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.nat_lt : ∀ {c : Cardinal.{u_1}}, c.IsRegular → ∀ (n : ℕ), ↑n < c
-- Mathlib.GroupTheory.Generators
/-- A group is finitely generated if and only if it admits a finite generating family.  -/
Group.fg_iff_nonempty_finite_generators : ∀ {G : Type u_1} [inst : Group G], Group.FG G ↔ ∃ n, Nonempty (Group.Generators G (Fin n))
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_apply : ∀ {α : Type u_1} (f : α →₀ ℕ), Finsupp.toMultiset f = f.sum fun a n => n • {a}
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.toCompatible_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B) (s : P.obj (Opposite.op B)) (i : I),
  ↑(CategoryTheory.Presieve.Arrows.toCompatible P π s) i = (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) s
-- Lean.Meta.CtorRecognizer
/-- Returns `true` if `isConstructorApp e` or `isConstructorApp (← whnf e)`
 -/
Lean.Meta.isConstructorApp' : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.reduce_isReduced' : ∀ (u : PNat.XgcdType), u.reduce.IsReduced'
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.mk.injEq : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (toFun : E → F) (smooth' : ContDiff ℝ (↑⊤) toFun)
  (decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C) (toFun_1 : E → F)
  (smooth'_1 : ContDiff ℝ (↑⊤) toFun_1)
  (decay'_1 : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun_1 x‖ ≤ C),
  ({ toFun := toFun, smooth' := smooth', decay' := decay' } =
      { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 }) =
    (toFun = toFun_1)
-- Lean.ReducibilityAttrs
/-- Set the reducibility attribute for the given declaration.  -/
Lean.setReducibilityStatus : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → Lean.ReducibilityStatus → m Unit
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.doubleXIso₁.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁),
  HomologicalComplex.doubleXIso₁ f hi₀₁ h = HomologicalComplex.doubleXIso₁ f hi₀₁ h
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.mk.sizeOf_spec : ∀ (numDigits : ℕ) (anchor : UInt64) (ordinal : ℕ),
  sizeOf { numDigits := numDigits, anchor := anchor, ordinal := ordinal } =
    1 + sizeOf numDigits + sizeOf anchor + sizeOf ordinal
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.map_injective_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {I : Type u_3} {e : I → R}
  [inst_2 : Fintype I],
  Function.Injective ⇑f → (CompleteOrthogonalIdempotents (⇑f ∘ e) ↔ CompleteOrthogonalIdempotents e)
-- Mathlib.Data.Nat.Factorization.Defs
/-- **Alias** of `Nat.prod_factorization_pow_eq_self`. -/
Nat.factorization_prod_pow_eq_self : ∀ {n : ℕ}, n ≠ 0 → (n.factorization.prod fun x1 x2 => x1 ^ x2) = n
-- Mathlib.Topology.Algebra.GroupWithZero
/-- A type with `0` and `Inv` such that `fun x ↦ x⁻¹` is continuous at all nonzero points. Any
normed (semi)field has this property.  -/
ContinuousInv₀ : (G₀ : Type u_4) → [Zero G₀] → [Inv G₀] → [TopologicalSpace G₀] → Prop
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInTime.mk.sizeOf_spec : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : SizeOf αΓ] [inst_3 : SizeOf βΓ] (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ) (time : ℕ → ℕ)
  (outputsFun :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (time (ea a).length)),
  sizeOf { toTM2ComputableAux := toTM2ComputableAux, time := time, outputsFun := outputsFun } =
    1 + sizeOf toTM2ComputableAux
-- Mathlib.Topology.Algebra.ConstMulAction
instContinuousConstSMulOrderDual : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α],
  ContinuousConstSMul M αᵒᵈ
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_top : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α], ⊤.out = 0
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.isBoundedUnder_abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ},
  ConvexOn ℝ C f →
    ∀ {x₀ : E},
      C ∈ nhds x₀ →
        (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) |f| ↔
          Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) f)
-- Mathlib.FieldTheory.Normal.Basic
Normal.exists_isSplittingField : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [h : Normal F K]
  [FiniteDimensional F K], ∃ p, Polynomial.IsSplittingField F K p
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_neg : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Neg (f i)] [inst_1 : DecidableEq I] (f₁ : (i : I) → f i) (i : I)
  (x₁ : f i), Function.update (-f₁) i (-x₁) = -Function.update f₁ i x₁
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C], CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k : α} {h' : k ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l} (mem : k ∈ m),
      (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey k h' = m.getKey k mem
-- Std.Data.ExtDHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.ExtDHashMap.inner : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.ExtDHashMap α β → Quotient (Std.DHashMap.isSetoid α β)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.smul_right : ∀ {α : Type u_2} {M : Type u_7} {R : Type u_8} [inst : TopologicalSpace α] [inst_1 : Zero R] [inst_2 : Zero M]
  [inst_3 : SMulWithZero R M] {f : α → R} {f' : α → M}, HasCompactSupport f → HasCompactSupport (f • f')
-- Mathlib.FieldTheory.SeparableDegree
/-- If a monic polynomial of separable degree one splits, then it is of form `(X - C y) ^ m` for
some non-zero natural number `m` and some element `y` of `F`.  -/
Polynomial.Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits : ∀ {F : Type u} [inst : Field F] {f : Polynomial F},
  f.Monic → f.Splits → f.natSepDegree = 1 → ∃ m y, m ≠ 0 ∧ f = (Polynomial.X - Polynomial.C y) ^ m
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extendOfIsometry_symm_eq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : NormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : NormedAddCommGroup Eₗ] [inst_7 : NormedSpace 𝕜 Eₗ] [inst_8 : CompleteSpace Eₗ]
  [inst_9 : NormedAddCommGroup Fₗ] [inst_10 : NormedSpace 𝕜₂ Fₗ] [inst_11 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : F),
  (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm).symm (e₂ x) = e₁ (f.symm x)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mk.injEq : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_3} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_4} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (domain : Submodule R E)
  (toFun : ↥domain →ₛₗ[σ] F) (domain_1 : Submodule R E) (toFun_1 : ↥domain_1 →ₛₗ[σ] F),
  ({ domain := domain, toFun := toFun } = { domain := domain_1, toFun := toFun_1 }) =
    (domain = domain_1 ∧ toFun ≍ toFun_1)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq.match_1_6.splitter : {ι : Type u_1} →
  (motive : CategoryTheory.Pairwise ι → Sort u_2) →
    (x : CategoryTheory.Pairwise ι) →
      ((i : ι) → motive (CategoryTheory.Pairwise.single i)) →
        ((i j : ι) → motive (CategoryTheory.Pairwise.pair i j)) → motive x
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.exactFunctor_le_rightExactFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  CategoryTheory.exactFunctor C D ≤ CategoryTheory.rightExactFunctor C D
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.nonneg_op : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : α}, 0 ≤ AddOpposite.op a ↔ 0 ≤ a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompute.toRingCompare : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute BaseType sα → Mathlib.Tactic.Ring.Common.RingCompare BaseType
-- Lean.Elab.Command.Scope
/-- A `Scope` records the part of the `CommandElabM` state that respects scoping,
such as the data for `universe`, `open`, and `variable` declarations, the current namespace,
and currently enabled options.
The `CommandElabM` state contains a stack of scopes, and only the top `Scope`
on the stack is read from or modified. There is always at least one `Scope` on the stack,
even outside any `section` or `namespace`, and each new pushed `Scope`
starts as a modified copy of the previous top scope.
 -/
Lean.Elab.Command.Scope : Type
-- Mathlib.Algebra.Order.Round
round_neg_two_inv : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α],
  round (-2⁻¹) = 0
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_le_map_iff_of_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f → ∀ {H K : Subgroup G}, Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K