mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.LpSpace
/-- Plancherel's theorem for `L2` functions.  -/
MeasureTheory.Lp.norm_fourier_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E] (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)),
  ‖FourierTransform.fourier f‖ = ‖f‖
-- Std.Http.Server.Handler
/-- Called for each incoming HTTP request.
 -/
Std.Http.Server.Handler.onRequest : {σ : Type} →
  [self : Std.Http.Server.Handler σ] →
    σ →
      Std.Http.Request Std.Http.Body.Stream →
        Std.Async.ContextAsync (Std.Http.Response (Std.Http.Server.Handler.ResponseBody σ))
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
/-- If `x : X _⦋n⦌` is a nondegenerate simplex of a nonsingular simplicial set,
this is the isomorphism `Δ[n] ≅ Subcomplex.ofSimplex x` induced by `x`.  -/
SSet.Nonsingular.iso : {X : SSet} →
  [X.Nonsingular] →
    {n : ℕ} →
      (x : X.obj (Opposite.op { len := n })) →
        x ∈ X.nonDegenerate n → (SSet.stdSimplex.obj { len := n } ≅ (SSet.Subcomplex.ofSimplex x).toSSet)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {unit : CategoryTheory.Functor.id C ⟶ F.comp G}
  {counit : G.comp F ⟶ CategoryTheory.Functor.id D}
  {left_triangle_components :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (F.map (unit.app X)) (counit.app (F.obj X)) =
          CategoryTheory.CategoryStruct.id (F.obj X))
      CategoryTheory.Adjunction.left_triangle_components._autoParam}
  {right_triangle_components :
    autoParam
      (∀ (Y : D),
        CategoryTheory.CategoryStruct.comp (unit.app (G.obj Y)) (G.map (counit.app Y)) =
          CategoryTheory.CategoryStruct.id (G.obj Y))
      CategoryTheory.Adjunction.right_triangle_components._autoParam}
  {unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G} {counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D}
  {left_triangle_components_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (F.map (unit_1.app X)) (counit_1.app (F.obj X)) =
          CategoryTheory.CategoryStruct.id (F.obj X))
      CategoryTheory.Adjunction.left_triangle_components._autoParam}
  {right_triangle_components_1 :
    autoParam
      (∀ (Y : D),
        CategoryTheory.CategoryStruct.comp (unit_1.app (G.obj Y)) (G.map (counit_1.app Y)) =
          CategoryTheory.CategoryStruct.id (G.obj Y))
      CategoryTheory.Adjunction.right_triangle_components._autoParam},
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components } =
      { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
        right_triangle_components := right_triangle_components_1 } →
    unit = unit_1 ∧ counit = counit_1
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.eq_1 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α) (b : β),
  Computation.LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b
-- Mathlib.Data.Multiset.Functor
Multiset.instMonad : Monad Multiset
-- Mathlib.Algebra.Polynomial.Derivation
/-- The derivation on `R[X]` that takes the value `a` on `X`.  -/
Polynomial.mkDerivation : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [inst_3 : Module (Polynomial R) A] →
            [inst_4 : IsScalarTower R (Polynomial R) A] → A →ₗ[R] Derivation R (Polynomial R) A
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flipₗᵢ_symm : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ],
  (ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ).symm = ContinuousLinearMap.flipₗᵢ 𝕜 Fₗ E Gₗ
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.coe_one : ModularGroup.coe 1 = 1
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- `AbstractMeasure.contractSnd` bundled with continuity in the function argument.  -/
AbstractMeasure.contractSndCLM : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] →
                [inst_5 : LocallyCompactSpace X] →
                  [LocallyCompactSpace Y] → AbstractMeasure Y R R →ₗ[R] C(X × Y, R) →L[R] C(X, R)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac.injEq : ∀ (r₁ c r₂ : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (r₁_1 c_1 r₂_1 : Lean.Grind.AC.Seq)
  (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac r₁ c r₂ c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac r₁_1 c_1 r₂_1 c₁_1 c₂_1) =
    (r₁ = r₁_1 ∧ c = c_1 ∧ r₂ = r₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RocSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RocSliceData α β → Std.Roc α
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.buildRule : Aesop.Frontend.RuleConfig → Aesop.ElabM (Aesop.LocalRuleSetMember × Array Aesop.RuleSetName)
-- Mathlib.Topology.NoetherianSpace
/-- [Stacks Tag 0052](https://stacks.math.columbia.edu/tag/0052) ((2)) -/
TopologicalSpace.NoetherianSpace.finite_irreducibleComponents : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α], (irreducibleComponents α).Finite
-- Mathlib.Topology.Neighborhoods
all_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) (P : Set X → Prop),
  (∀ (s t : Set X), s ⊆ t → P s → P t) → ((∀ s ∈ nhds x, P s) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → P s)
-- Std.Async.Signal
Std.Async.Signal.sigttin.sizeOf_spec : sizeOf Std.Async.Signal.sigttin = 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.Hom.hom_hom_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X] (f : G ⟶ H), (-f).hom.hom = -f.hom.hom
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.symm_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  P.symm.i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_set_indicator : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (⇑fun₀ | a => b) = {a}.indicator fun x => b
-- Mathlib.Order.Filter.IndicatorFunction
indicator_eventuallyEq : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s t : Set α} {f g : α → M} {l : Filter α},
  f =ᶠ[l ⊓ Filter.principal s] g → s =ᶠ[l] t → s.indicator f =ᶠ[l] t.indicator g
-- Mathlib.Logic.Function.Basic
Set.separatesPoints_mono : ∀ {α : Type u_3} {β : Type u_4} {A B : Set (α → β)}, A ⊆ B → A.SeparatesPoints → B.SeparatesPoints
-- Mathlib.Topology.Neighborhoods
/-- If `f x ≤ g x` in a neighbourhood of `x`, then for `y` sufficiently close to `x` we have
`f x ≤ g x` in a neighbourhood of `y`.  -/
Filter.EventuallyLE.eventuallyLE_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} [inst_1 : LE α] {f g : X → α},
  f ≤ᶠ[nhds x] g → ∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g
-- Mathlib.Data.Setoid.Partition
IndexedPartition.mk.inj : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} {eq_of_mem : ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j}
  {some : ι → α} {some_mem : ∀ (i : ι), some i ∈ s i} {index : α → ι} {mem_index : ∀ (x : α), x ∈ s (index x)}
  {eq_of_mem_1 : ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j} {some_1 : ι → α}
  {some_mem_1 : ∀ (i : ι), some_1 i ∈ s i} {index_1 : α → ι} {mem_index_1 : ∀ (x : α), x ∈ s (index_1 x)},
  { eq_of_mem := eq_of_mem, some := some, some_mem := some_mem, index := index, mem_index := mem_index } =
      { eq_of_mem := eq_of_mem_1, some := some_1, some_mem := some_mem_1, index := index_1, mem_index := mem_index_1 } →
    some = some_1 ∧ index = index_1
-- Lean.LocalContext
Lean.mkLocalDeclEx : ℕ → Lean.FVarId → Lean.Name → Lean.Expr → Lean.BinderInfo → Lean.LocalDecl
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.castLEquiv_apply : ∀ {n m : ℕ} (h : n ≤ m) (i : Fin n), (Fin.castLEquiv h) i = ⟨Fin.castLE h i, ⋯⟩
-- Init.Data.Vector.Basic
Vector.shrink_eq_take : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ), xs.shrink i = xs.take i
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.isPretransitive_of_isGaloisGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (G : Type u_3) [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : IsGaloisGroup G A B],
  MulAction.IsPretransitive G ↑(p.primesOver B)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ} (h : D₁ ≤ D₂),
  CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h =
    CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h
-- Mathlib.Combinatorics.Graph.Maps
Graph.Inc.map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {v : α} {e : β} (f : α → α'),
  G.Inc e v → (Graph.map f G).Inc e (f v)
-- Mathlib.CategoryTheory.Iso
/-- The existence of an inverse morphism.  -/
CategoryTheory.IsIso.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsIso f],
  ∃ inv,
    CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧
      CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_type : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  (Ordinal.type fun x1 x2 => x1 < x2).cof = Order.cof α
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_smul' : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : βᵒᵈ) (a : α), OrderDual.ofDual b • a = b • a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : k ∈ t), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.loop.eq_2 : ∀ {α : Type u} (x : Array α) (n : ℕ), Array.shrink.loop✝ n.succ x = Array.shrink.loop✝ n x.pop
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_eq_bot_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N},
  H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.instMulPosStrictMonoNonZeroDivisors : ∀ {A : Type u_2} (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K], MulPosStrictMono (FractionalIdeal (nonZeroDivisors A) K)
-- Lean.Data.Json.FromToJson.Basic
Lean.Json.setObjValAs! : Lean.Json → {α : Type u} → [Lean.ToJson α] → String → α → Lean.Json
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffineOpen.biInf : ∀ {X : AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))]
  {ι : Type u_1} (s : Set ι),
  s.Finite →
    s.Nonempty →
      ∀ {U : ι → X.Opens},
        (∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (U i)) → AlgebraicGeometry.IsAffineOpen (⨅ i ∈ s, U i)
-- Init.Data.String.Basic
String.utf8GetAux : List Char → String.Pos.Raw → String.Pos.Raw → Char
-- Mathlib.Logic.Small.Set
small_subset : ∀ {α : Type u1} {s t : Set α}, t ⊆ s → ∀ [Small.{u, u1} ↑s], Small.{u, u1} ↑t
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {P : CategoryTheory.ProjectiveResolution Z} {Z' : C}
  {P' : CategoryTheory.ProjectiveResolution Z'} {f : Z ⟶ Z'} [inst_3 : SizeOf C] (hom : P.complex ⟶ P'.complex)
  (hom_f_zero_comp_π_f_zero :
    CategoryTheory.CategoryStruct.comp (hom.f 0) (P'.π.f 0) =
      CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0)),
  sizeOf { hom := hom, hom_f_zero_comp_π_f_zero := hom_f_zero_comp_π_f_zero } =
    1 + sizeOf hom + sizeOf hom_f_zero_comp_π_f_zero
-- Mathlib.Algebra.Free
FreeSemigroup.lift_mk_eq_foldl : ∀ {α : Type u} {β : Type v} [inst : Semigroup β] {f : α → β} {x : α} {xs : List α},
  (FreeSemigroup.lift f) { head := x, tail := xs } = List.foldl (fun x1 x2 => x1 * f x2) (f x) xs
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The inclusion of polynomials into power series has dense image  -/
PowerSeries.WithPiTopology.denseRange_toPowerSeries : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : CommSemiring R], DenseRange Polynomial.toPowerSeries
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q)
  (hq' : q' = q), CategoryTheory.CategoryStruct.comp (γ.v p q hpq) (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯
-- Mathlib.Control.Bifunctor
Sum.bifunctor : Bifunctor Sum
-- Mathlib.Analysis.Convex.Segment
segment_symm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E), segment 𝕜 x y = segment 𝕜 y x
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.arrow.sizeOf_spec : sizeOf Lean.Meta.DiscrTree.Key.arrow = 1
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.isStronglyProgressive_of_tendsto'`. -/
MeasureTheory.progMeasurable_of_tendsto' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} {γ : Type u_4} [inst_2 : MeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β] (fltr : Filter γ) [fltr.NeBot] [fltr.IsCountablyGenerated]
  {U : γ → ι → Ω → β},
  (∀ (l : γ), MeasureTheory.IsStronglyProgressive f (U l)) →
    Filter.Tendsto U fltr (nhds u) → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.instCompleteLattice : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [S : AddTorsor V P] → CompleteLattice (AffineSubspace k P)
-- Std.Http.Data.Status
Std.Http.Status.tooEarly.sizeOf_spec : sizeOf Std.Http.Status.tooEarly = 1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
is a non-unital commutative semiring.

See note [reducible non-instances].  -/
NonUnitalStarAlgebra.adjoinNonUnitalCommSemiringOfComm : (R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] →
                [inst_6 : SMulCommClass R A A] →
                  [inst_7 : StarModule R A] →
                    {s : Set A} →
                      (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) →
                        (∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) →
                          NonUnitalCommSemiring ↥(NonUnitalStarAlgebra.adjoin R s)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.two_nsmul_reflection_eq_of_perm_eq : ∀ {ι : 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) (i j : ι),
  P.reflectionPerm i = P.reflectionPerm j → 2 • ⇑(P.reflection i) = 2 • ⇑(P.reflection j)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)) (f : σ → Λ),
  Turing.TM2.stepAux (Turing.TM2.Stmt.goto f) x x_1 = { l := some (f x), var := x, stk := x_1 }
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.Word.equivPairAux.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] (i : ι) (w : Monoid.CoprodI.Word M),
  Monoid.CoprodI.Word.equivPairAux✝ i w =
    Monoid.CoprodI.Word.consRecOn w ⟨{ head := 1, tail := Monoid.CoprodI.Word.empty, fstIdx_ne := ⋯ }, ⋯⟩
      fun j m w h1 h2 x =>
      if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
      else ⟨{ head := 1, tail := Monoid.CoprodI.Word.cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩
-- Mathlib.RingTheory.WittVector.Complete
/-- If `k` is a perfect ring of characteristic `p`, then the ring of Witt vectors `𝕎 k` is
`p`-torsion free.
 -/
WittVector.eq_zero_of_p_mul_eq_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p]
  (x : WittVector p k), x * ↑p = 0 → x = 0
-- Init.Data.Function
Function.curry_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) (x : α) (y : β), Function.curry f x y = f (x, y)
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.mk.sizeOf_spec : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {L : SummationFilter β} [inst_3 : SizeOf β] [inst_4 : SizeOf 𝕜] [inst_5 : SizeOf X]
  (basis : β → X) (coord : β → StrongDual 𝕜 X) (ortho : ∀ (i j : β), (coord i) (basis j) = Pi.single j 1 i)
  (expansion : ∀ (x : X), HasSum (fun i => (coord i) x • basis i) x L),
  sizeOf { basis := basis, coord := coord, ortho := ortho, expansion := expansion } = 1
-- Batteries.Data.Array.Scan
Array.scanlM_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] {f : β → α → m β}
  {start stop : ℕ}, Array.scanlM f init #[] start stop = pure #[init]
-- Init.Data.Vector.Lemmas
Vector.extract_empty : ∀ {α : Type u_1} {start stop : ℕ}, #v[].extract start stop = Vector.cast ⋯ #v[]
-- Mathlib.Data.Finset.Sups
Finset.powerset_inter : ∀ {α : Type u_2} [inst : DecidableEq α] (s t : Finset α), (s ∩ t).powerset = s.powerset ⊼ t.powerset
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.insertSorted : ℕ → Nat.Internal.SOM.Mon → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.finallySmall_of_small_weakly_terminal_set : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J] (s : Set J)
  [Small.{v, u} ↑s], (∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)) → CategoryTheory.FinallySmall J
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Fact.instToString : ToString Lean.Elab.Tactic.Omega.Fact
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.log_lt_iff_lt_exp : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  x ≠ 0 → (x.log < a ↔ x < WithZero.exp a)
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- Given a connected index category, the colimit of the constant unit-valued functor is `PUnit`.  -/
CategoryTheory.Limits.Types.colimitConstPUnitIsoPUnit : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsConnected C] →
      CategoryTheory.Limits.colimit (CategoryTheory.Limits.Types.constPUnitFunctor C) ≅ PUnit.{w + 1}
-- Lean.Meta.Tactic.Grind.CheckResult
/-- Joins two results. It uses the order `.none < .progress < .propagated < .closed`
 -/
Lean.Meta.Grind.CheckResult.join : Lean.Meta.Grind.CheckResult → Lean.Meta.Grind.CheckResult → Lean.Meta.Grind.CheckResult
-- Mathlib.ModelTheory.Basic
/-- Makes a `Language.empty.Hom` out of any function.
This is only needed because there is no instance of `FunLike (M → N) M N`, and thus no instance of
`Language.empty.HomClass M N`.  -/
Function.emptyHom : {M : Type w} →
  {N : Type w'} →
    [inst : FirstOrder.Language.empty.Structure M] →
      [inst_1 : FirstOrder.Language.empty.Structure N] → (M → N) → FirstOrder.Language.empty.Hom M N
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_zsmul_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
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem : Type
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addRight_apply : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c x : G),
  (IsometryEquiv.addRight c) x = x + c
-- Mathlib.GroupTheory.OrderOfElement
zpow_eq_zpow_iff_modEq : ∀ {G : Type u_1} [inst : Group G] {x : G} {m n : ℤ}, x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.val_sectionInBasicOpen_apply : ∀ {A σ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (p : ↑(ProjectiveSpectrum.top 𝒜))
  (c : HomogeneousLocalization.NumDenSameDeg 𝒜 p.asHomogeneousIdeal.toIdeal.primeCompl)
  (q : ↥(ProjectiveSpectrum.basicOpen 𝒜 ↑c.den)),
  HomogeneousLocalization.val (↑(AlgebraicGeometry.sectionInBasicOpen 𝒜 p c) q) = Localization.mk ↑c.num ⟨↑c.den, ⋯⟩
-- Mathlib.LinearAlgebra.InvariantBasisNumber
StrongRankCondition.mk : ∀ {R : Type u} [inst : Semiring R],
  (∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Injective ⇑f → n ≤ m) → StrongRankCondition R
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (toAlgHom : A →ₐ[R] B)
  (map_star' : ∀ (x : A), (↑↑toAlgHom.toRingHom).toFun (star x) = star ((↑↑toAlgHom.toRingHom).toFun x))
  (toAlgHom_1 : A →ₐ[R] B)
  (map_star'_1 : ∀ (x : A), (↑↑toAlgHom_1.toRingHom).toFun (star x) = star ((↑↑toAlgHom_1.toRingHom).toFun x)),
  ({ toAlgHom := toAlgHom, map_star' := map_star' } = { toAlgHom := toAlgHom_1, map_star' := map_star'_1 }) =
    (toAlgHom = toAlgHom_1)
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.edist_efixedPoint_le' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} {s : Set α} (hsc : IsComplete s)
  (hsf : Set.MapsTo f s s) (hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ⊤), edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Which cost function is instantiated  -/
ValuedCSP.Term.f : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] →
          {Γ : ValuedCSP D C} → {ι : Type u_3} → (self : Γ.Term ι) → (Fin self.n → D) → C
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_apply_left : ∀ {n : ℕ} (i : Fin n), (finSumNatEquiv n) (Sum.inl i) = ↑i