mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Pi
Pi.isScalarTower' : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → SMul M (α i)]
  [inst_1 : (i : ι) → SMul (α i) (β i)] [inst_2 : (i : ι) → SMul M (β i)] [∀ (i : ι), IsScalarTower M (α i) (β i)],
  IsScalarTower M ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.Probability.Kernel.Composition.Lemmas
MeasureTheory.Measure.compProd_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ]
  [ProbabilityTheory.IsSFiniteKernel κ] {f : β → γ},
  Measurable f → μ.compProd (κ.map f) = MeasureTheory.Measure.map (Prod.map id f) (μ.compProd κ)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionOptions.mk : Lean.Lsp.WorkDoneProgressOptions → Option (Array Lean.Lsp.CodeActionKind) → Option Bool → Lean.Lsp.CodeActionOptions
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
/-- The pointwise product of two finsets `s` and `t`: `s • t = {x • y | x ∈ s, y ∈ t}`.  -/
Finset.smul : {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [SMul α β] → SMul (Finset α) (Finset β)
-- Mathlib.Algebra.Group.Submonoid.Units
ofAddUnits_addUnits_gci.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M], ofAddUnits_addUnits_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯
-- Lean.Parser.Attr
Lean.Parser.Attr.default_instance.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.ExtHashMap.Basic
/-- Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.ExtHashMap.filterMap : {α : Type u} →
  {β : Type v} →
    {γ : Type w} →
      {x : BEq α} →
        {x_1 : Hashable α} →
          [EquivBEq α] → [LawfulHashable α] → (α → β → Option γ) → Std.ExtHashMap α β → Std.ExtHashMap α γ
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.slice!.eq_1 : ∀ (s : String) (p₁ p₂ : s.Pos), s.slice! p₁ p₂ = s.toSlice.slice! p₁.toSlice p₂.toSlice
-- Mathlib.Order.Filter.Lift
Filter.monotone_lift' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder γ] {f : γ → Filter α} {g : γ → Set α → Set β},
  Monotone f → Monotone g → Monotone fun c => (f c).lift' (g c)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_foldl_reinsertAux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] (l : List ((a : α) × β a))
  (target : { d // 0 < d.size }),
  (Std.DHashMap.Internal.toListModel
        ↑(List.foldl (fun acc p => Std.DHashMap.Internal.Raw₀.reinsertAux hash acc p.fst p.snd) target l)).Perm
    (l ++ Std.DHashMap.Internal.toListModel ↑target)
-- Init.Data.ByteArray.Lemmas
ByteArray.size_push : ∀ {bs : ByteArray} {b : UInt8}, (bs.push b).size = bs.size + 1
-- Std.Http.Internal.Char
/-- Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are:
alphanumeric, hyphen, period, underscore, and tilde.
 -/
Std.Http.Internal.Char.isUnreserved : UInt8 → Bool
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.pointwise_smul_def : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] {a : α}
  (S : Subgroup G), a • S = Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.smul_τ₃ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (a : R) (φ : S₁ ⟶ S₂), (a • φ).τ₃ = a • φ.τ₃
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.toAddSubgroup_toIntSubmodule : ∀ {M : Type u_3} [inst : AddCommGroup M] (S : Submodule ℤ M), AddSubgroup.toIntSubmodule S.toAddSubgroup = S
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of a meromorphic function `f`, mapping a point `z` to the order of `f` at `z`, and to
zero if the order is infinite.
 -/
MeromorphicOn.divisor : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → (U : Set 𝕜) → Function.locallyFinsuppWithin U ℤ
-- Mathlib.Tactic.Linter.FlexibleLinter
Mathlib.Linter.Flexible.instInhabitedStained.default : Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_nsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoMod hp a (m • p + b) = toIcoMod hp a b
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.diagram.eq_1 : ∀ (P : ProfiniteAddGrp.{u}),
  P.diagram = P.toFiniteQuotientFunctor.comp (CategoryTheory.forget₂ FiniteAddGrp.{u} ProfiniteAddGrp.{u})
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_toArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ Std.DTreeMap.Const.toArray t₁ = Std.DTreeMap.Const.toArray t₂
-- Mathlib.Topology.Algebra.Group.Basic
Units.isClosedEmbedding_embedProduct : ∀ {α : Type u} [inst : Monoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousMul α],
  Topology.IsClosedEmbedding ⇑(Units.embedProduct α)
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ SemiRingCat AddCommMonCat
-- Mathlib.Data.Ordmap.Invariants
Ordnode.foldr.eq_1 : ∀ {α : Type u_1} {β : Sort u_2} (f : α → β → β) (x : β), Ordnode.foldr f Ordnode.nil x = x
-- Mathlib.CategoryTheory.Action.Monoidal
/-- The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on
each factor.  -/
Action.diagonalSuccIsoTensorDiagonal : (G : Type u) →
  [inst : Monoid G] →
    (n : ℕ) →
      Action.diagonal G (n + 1) ≅
        CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.diagonal G n)
-- Init.Tactics
/-- `dbg_trace "foo"` prints `foo` when elaborated.
Useful for debugging tactic control flow:
```
example : False ∨ True := by
  first
  | apply Or.inl; trivial; dbg_trace "left"
  | apply Or.inr; trivial; dbg_trace "right"
```
 -/
Lean.Parser.Tactic.dbgTrace : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap (φ - φ') =
    CategoryTheory.ShortComplex.leftHomologyMap φ - CategoryTheory.ShortComplex.leftHomologyMap φ'
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnriched_id_comp : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₁],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₁)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂))
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₁ F₂)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
-- Mathlib.Order.ZornAtoms
/-- **Zorn's lemma**: A partial order is coatomic if every nonempty chain `c`, `⊤ ∉ c`, has an upper
bound not equal to `⊤`.  -/
IsCoatomic.of_isChain_bounded : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α],
  (∀ (c : Set α), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c) → IsCoatomic α
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.isTable_buildTable : ∀ {pat : String.Slice},
  String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ pat.copy.toByteArray
    (String.Slice.Pattern.ForwardSliceSearcher.buildTable pat).toArray
-- Init.Data.Nat.Lemmas
Nat.decidableExistsLT : {p : ℕ → Prop} → [h : DecidablePred p] → DecidablePred fun n => ∃ m < n, p m
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The short complex `L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₂' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex C
-- Mathlib.Order.Category.Lat
Lat.hom_comp : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z),
  Lat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Lat.Hom.hom g).comp (Lat.Hom.hom f)
-- Mathlib.LinearAlgebra.Goursat
Submodule.goursatSnd.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (L : Submodule R (M × N)),
  L.goursatSnd = Submodule.map (LinearMap.snd R M N ∘ₗ L.subtype) (LinearMap.fst R M N ∘ₗ L.subtype).ker
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- We can infer `FiniteDimensional K V` in the presence of `[Fact (finrank K V = n + 1)]`.
Use `have : FiniteDimensional K V := .of_fact_finrank_eq_succ` when needed.

This is not an instance because `n` cannot be inferred.
 -/
FiniteDimensional.of_fact_finrank_eq_succ : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (n : ℕ)
  [hn : Fact (Module.finrank K V = n + 1)], FiniteDimensional K V
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ComonToMonOpOpObj_mon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Comon C), CategoryTheory.MonObj.mul = CategoryTheory.ComonObj.comul.op
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.inclusionMapIso_hom : ∀ {X Y : TopCat} (f : X ⟶ Y) (x : ↑X),
  (TopologicalSpace.OpenNhds.inclusionMapIso f x).hom =
    CategoryTheory.CategoryStruct.id
      ((TopologicalSpace.OpenNhds.inclusion ((CategoryTheory.ConcreteCategory.hom f) x)).comp
        (TopologicalSpace.Opens.map f))
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instSingletonOfT1Space : {α : Type u_2} → [inst : TopologicalSpace α] → [T1Space α] → Singleton α (TopologicalSpace.Closeds α)
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.mk.sizeOf_spec : ∀ (map : Lean.AssocList Lean.FVarId Lean.Expr), sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.mk : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R},
  A₀ ^ 2 = 1 →
    A₁ ^ 2 = 1 →
      B₀ ^ 2 = 1 →
        B₁ ^ 2 = 1 →
          star A₀ = A₀ →
            star A₁ = A₁ →
              star B₀ = B₀ →
                star B₁ = B₁ →
                  A₀ * B₀ = B₀ * A₀ →
                    A₀ * B₁ = B₁ * A₀ → A₁ * B₀ = B₀ * A₁ → A₁ * B₁ = B₁ * A₁ → IsCHSHTuple A₀ A₁ B₀ B₁
-- Init.Data.List.TakeDrop
List.map_drop : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : ℕ},
  List.map f (List.drop i l) = List.drop i (List.map f l)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasStrictFDerivAt_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (n : ℕ) [inst_7 : OfNat F n] (x : E), HasStrictFDerivAt (OfNat.ofNat n) 0 x
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instNumberField : ∀ (n : ℕ) (K : Type w) [inst : Field K] [NumberField K], NumberField (CyclotomicField n K)
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Presheaf.isGluing_iff_pairwise : ∀ {X : TopCat} {F : TopCat.Presheaf (Type u_4) X} {ι : Type u_5} {U : ι → TopologicalSpace.Opens ↑X}
  {sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))}
  {s : CategoryTheory.ToType (F.obj (Opposite.op (iSup U)))},
  F.IsGluing U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op).π.app i))
          s =
        TopCat.Presheaf.objPairwiseOfFamily sf i
-- Mathlib.RingTheory.Ideal.Operations
Submodule.mem_smul_span : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : Ideal R}
  [I.IsTwoSided] {s : Set M} {x : M}, x ∈ I • Submodule.span R s ↔ x ∈ Submodule.span R (↑I • s)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_ringEquiv_injective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Injective AlgEquiv.toRingEquiv
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.hasDerivAt_wedgeIntegral_re_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E],
  ContinuousOn f (Metric.ball c r) →
    ∀ {z : ℂ},
      z ∈ Metric.ball c r →
        (fun w => (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - (w - z).re • f z) =o[nhds z] fun w => w - z
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cone is a limit cone if its extension by an isomorphism is.  -/
CategoryTheory.Limits.IsLimit.ofExtendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cone F} →
            {X : C} →
              (i : X ⟶ s.pt) →
                [CategoryTheory.IsIso i] → CategoryTheory.Limits.IsLimit (s.extend i) → CategoryTheory.Limits.IsLimit s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_1.splitter : {w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1) →
      (x : Std.Tactic.BVDecide.BVExpr.Return aig w) →
        ((result : aig.ExtendingRefVecEntry w) →
            (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig) → motive { result := result, cache := cache }) →
          motive x
-- Init.Data.Vector.Lemmas
Vector.map_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f g : α → β} {xs : Vector α n},
  Vector.map f xs = Vector.map g xs ↔ ∀ a ∈ xs, f a = g a
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_monomial_succ : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ),
  Polynomial.derivative ((Polynomial.monomial (n + 1)) a) = (Polynomial.monomial n) (a * (↑n + 1))
-- Mathlib.Order.Filter.Map
Filter.eventuallyLE_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ},
  g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.lift_addConj_eq_add_add_neg_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.AddGrpObj.addConj G) h) =
    CategoryTheory.CategoryStruct.comp (f₁ + f₂ + -f₁) h
-- Lean.Structure
Lean.StructureResolutionState.mk.sizeOf_spec : ∀ (resolutions : Lean.PHashMap Lean.Name (Array Lean.Name)),
  sizeOf { resolutions := resolutions } = 1 + sizeOf resolutions
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instCompleteLattice : {α : Type u_2} → [inst : TopologicalSpace α] → CompleteLattice (TopologicalSpace.Closeds α)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.maximalSeparatedSet_subset : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, Metric.maximalSeparatedSet ε A ⊆ A
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The alphabet for the stacks in the program. `bit0` and `bit1` are used to represent `ℕ` values
as lists of binary digits, `cons` is used to separate `List ℕ` values, and `consₗ` is used to
separate `List (List ℕ)` values. See the section documentation.  -/
Turing.PartrecToTM2.Γ' : Type
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.id_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (X : CategoryTheory.StructuredArrow S T),
  CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id X.right
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rio.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_5 : Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rio α}, r.iter.toList = r.toList
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Adding a point in the affine span and a vector in the spanning submodule produces a point in the
affine span.  -/
vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P} {v : V},
  p ∈ spanPoints k s → v ∈ vectorSpan k s → v +ᵥ p ∈ spanPoints k s
-- Mathlib.LinearAlgebra.Reflection
Module.involutive_reflection : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} (h : f x = 2), Function.Involutive ⇑(Module.reflection h)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_star : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Star β] {f : MeasureTheory.SimpleFunc α β},
  ⇑(star f) = star ⇑f
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.range_faceOpposite_points : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  Set.range (s.faceOpposite i).points = s.points '' {i}ᶜ
-- Mathlib.MeasureTheory.Integral.Bochner.L1
_private.Mathlib.MeasureTheory.Integral.Bochner.L1.0.MeasureTheory.L1.termIntegral : Lean.ParserDescr
-- Lean.Meta.Sym.InstantiateS
/-- Internal variant of `instantiateS` that runs in `AlphaShareBuilderM`.  -/
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateS' : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_fst_assoc : ∀ (X : SSet) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj { len := 1 })) h) =
    h
-- Lean.Parser.Term
Lean.Parser.Term.forall.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [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 → (t.insertMany l).getD k' fallback = v
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- `unfold` correctly decomposes a friendly operation: the head of `op s` depends only on the
head of `s` (and is given by `unfold`), while the tail of `op s` is obtained by applying the
friendly operation returned by `unfold` to the tail of `s`. This gives a coinductive
characterization of `FriendlyOperation`. For the coinduction principle, see
`FriendlyOperation.coind`.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.destruct_apply_eq_unfold : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : Tactic.ComputeAsymptotics.Seq.FriendlyOperation op)
  {s : Stream'.Seq α},
  (op s).destruct =
    Option.map
      (fun x =>
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h.unfold s.head)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- Polarization restricted to `S`-span of roots.  -/
RootPairing.PolarizationIn : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_5) →
                      [inst_5 : CommRing S] →
                        [inst_6 : Algebra S R] →
                          [FaithfulSMul S R] →
                            [inst_8 : Module S M] →
                              [IsScalarTower S R M] →
                                [inst_10 : Module S N] → [P.IsValuedIn S] → [Fintype ι] → ↥(P.rootSpan S) →ₗ[S] N
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (motive : Std.DTreeMap.Internal.RxcIterator α β → Sort u_3) →
        (x : Std.DTreeMap.Internal.RxcIterator α β) →
          ((upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }) →
            ((k : α) →
                (v : β k) →
                  (t : Std.DTreeMap.Internal.Impl α β) →
                    (it : Std.DTreeMap.Internal.Zipper α β) →
                      (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }) →
              motive x
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.mk.injEq : ∀ (carrier : Type u) [str : CommGroup carrier] (carrier_1 : Type u) (str_1 : CommGroup carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.Walk.ofBoxProdLeft.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x : α × β}
  (motive : (y : α × β) → (G □ H).Walk x y → Sort u_3) (h_1 : Unit → motive x SimpleGraph.Walk.nil)
  (h_2 : (y v : α × β) → (h : (G □ H).Adj x v) → (w : (G □ H).Walk v y) → motive y (SimpleGraph.Walk.cons h w)),
  (match x, SimpleGraph.Walk.nil with
    | .(x), SimpleGraph.Walk.nil => h_1 ()
    | y, SimpleGraph.Walk.cons h w => h_2 y v h w) =
    h_1 ()
-- Mathlib.Data.Multiset.Functor
Multiset.map_traverse : ∀ {G : Type u_1 → Type u_1} [inst : Applicative G] [inst_1 : CommApplicative G] {α β γ : Type u_1} (g : α → G β)
  (h : β → γ) (x : Multiset α), Functor.map h <$> Multiset.traverse g x = Multiset.traverse (Functor.map h ∘ g) x
-- Lean.Util.Recognizers
Lean.Expr.not? : Lean.Expr → Option Lean.Expr
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.grindExt : Lean.Meta.Grind.Extension
-- Mathlib.Algebra.Algebra.Basic
Algebra.algebraMapSubmonoid_isUnit_le : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Algebra R S],
  Algebra.algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S