mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Async.Basic
/-- Runs two computations concurrently and returns the result of the one that finishes first.
The other result is lost and the other task is not cancelled, so the task will continue the execution
until the end.
 -/
Std.Async.EAsync.race : {α ε : Type} →
  [Inhabited α] →
    Std.Async.EAsync ε α → Std.Async.EAsync ε α → optParam Task.Priority Task.Priority.default → Std.Async.EAsync ε α
-- Mathlib.Analysis.Calculus.ContDiff.Operations
hasFTaylorSeriesUpToOn_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_3} [inst_3 : Fintype ι] {F' : ι → Type u_5}
  [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i}
  {p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)} {n : WithTop ℕ∞},
  HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
    ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_6 : FirstOrder.Field.FieldAxiom.oneMul.toSentence =
  ((1 * (FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) 0)).all
-- Mathlib.CategoryTheory.Square
/-- the right morphism  -/
CategoryTheory.Square.f₂₄ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.Square C) → self.X₂ ⟶ self.X₄
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balance1_All : ∀ {α : Type u_1} {p : α → Prop} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All p (l.balance1 v r) ↔ p v ∧ RBTree.RBNode.All p l ∧ RBTree.RBNode.All p r
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.anyM.eq_1 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool), List.anyM p [] = pure false
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_6 : ∀ (p : PosNum) (n : ℕ), p.bit1.testBit n.succ = p.testBit n
-- Mathlib.Data.Rel
SetRel.symmetrize_subset_self : ∀ {α : Type u_1} {R : SetRel α α}, R.symmetrize ⊆ R
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instOfIsFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsFinite f], AlgebraicGeometry.IsProper f
-- Mathlib.Order.UpperLower.Prod
UpperSet.bot_prod_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], ⊥ ×ˢ ⊥ = ⊥
-- Mathlib.Data.Seq.Defs
/-- Recursion principle for sequences, compare with `List.recOn`.  -/
Stream'.Seq.recOn : {α : Type u} →
  {motive : Stream'.Seq α → Sort v} →
    (s : Stream'.Seq α) →
      motive Stream'.Seq.nil → ((x : α) → (s : Stream'.Seq α) → motive (Stream'.Seq.cons x s)) → motive s
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The difference of two `C^n` functions is `C^n`.  -/
ContDiff.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f g : E → F}, ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => f x - g x
-- Mathlib.Computability.TuringMachine.Tape
/-- The portion of the tape going off to the right.  -/
Turing.Tape.right : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Tape Γ → Turing.ListBlank Γ
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- `X.asLimitCone` is indeed a limit cone.  -/
Profinite.asLimit : (X : Profinite) → CategoryTheory.Limits.IsLimit X.asLimitCone
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.add_mem_vadd_finset_iff : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] (a : α) {b : α} {s : Finset α}, a + b ∈ a +ᵥ s ↔ b ∈ s
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining the negation of the ring of Witt vectors.  -/
WittVector.wittNeg : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 1 × ℕ) ℤ
-- Batteries.Data.AssocList
Batteries.AssocList.isEmpty_eq : ∀ {α : Type u_1} {β : Type u_2} (l : Batteries.AssocList α β), l.isEmpty = l.toList.isEmpty
-- Init.Data.List.Sublist
List.sublist_append_of_sublist_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Sublist l₁ → l.Sublist (l₁ ++ l₂)
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk'_congr_succ'_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0)
  {X Y : V} (f g : X ⟶ Y) (h : f = g),
  (succ' f).snd.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (succ' g).snd.fst
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeFun.match_1.eq_2 : ∀ {n : ℕ} (motive : (x : ℕ) → Fin (n ^ x) → Sort u_1) (m k : ℕ) (hk : k < n ^ (m + 1))
  (h_1 : (x : Fin (n ^ 0)) → motive 0 x) (h_2 : (m k : ℕ) → (hk : k < n ^ (m + 1)) → motive m.succ ⟨k, hk⟩),
  (match m.succ, ⟨k, hk⟩ with
    | 0, x => h_1 x
    | m.succ, ⟨k, hk⟩ => h_2 m k hk) =
    h_2 m k hk
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.coeffs_p_subset : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B)
  (i : Algebra.Smooth.DescentAux.rels✝ D),
  ↑(Algebra.Smooth.DescentAux.p✝ D i).coeffs ⊆
    Set.range ⇑(MvPolynomial.map (algebraMap (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) A))
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasStrictFDerivAt_const_add_iff : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasStrictFDerivAt (fun x => c + f x) f' x ↔ HasStrictFDerivAt f f' x
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.EdgeDisjointTriangles.mono : ∀ {α : Type u_1} {G H : SimpleGraph α}, G ≤ H → H.EdgeDisjointTriangles → G.EdgeDisjointTriangles
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  l.isEmpty = false → Std.Internal.List.maxKey? l = some (Std.Internal.List.maxKey! l)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V)
  {Z : AlgebraicGeometry.Scheme} (h_1 : ↑↑V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h) (CategoryTheory.CategoryStruct.comp (I.glueDataObjι V) h_1) =
    CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (CategoryTheory.CategoryStruct.comp (X.homOfLE h) h_1)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- Universe lifting is fully faithful.  -/
FGModuleCat.fullyFaithfulULift : (R : Type u) → [inst : Ring R] → (FGModuleCat.ulift R).FullyFaithful
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given an (in)equality, look up the lemma to right-multiply it by a constant.  If relevant, also
take into account the degree of positivity which can be proved of the constant: strict or
non-strict.  -/
Mathlib.Ineq.mulConstRelData : Mathlib.Ineq.WithStrictness → Lean.Name
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- Equivalence of coprime powers of primitive roots. If a * b ≡ 1 (mod n), then x ↦ x ^ a and
x ↦ x ^ b restricts to a bijection on the n-th primitive roots.  -/
IsPrimitiveRoot.primitiveRootsPowEquiv : {R : Type u_4} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] → {a b n : ℕ} → a * b ≡ 1 [MOD n] → ↥(primitiveRoots n R) ≃ ↥(primitiveRoots n R)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flipₗᵢ'_symm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃],
  (ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃).symm = ContinuousLinearMap.flipₗᵢ' F E G σ₁₃ σ₂₃
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of
`fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v`.  -/
Real.hasFDerivAt_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (fun v => ‖v‖ * ‖f v‖) MeasureTheory.volume →
      ∀ (x : V),
        HasFDerivAt (FourierTransform.fourier f)
          (FourierTransform.fourier (VectorFourier.fourierSMulRight (innerSL ℝ) f) x) x
-- Mathlib.Algebra.Order.Kleene
one_add_kstar_mul : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, 1 + KStar.kstar a * a = KStar.kstar a
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_dvd_left : ∀ {m k n : ℕ}, m ∣ k → k.Coprime n → m.Coprime n
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.symm_apply_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B) (x : A), e.symm (e x) = x
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iio a).OrdConnected
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_map_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : M →ₙ+ N},
  AddSubsemigroup.comap f (AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = AddSubsemigroup.comap f S
-- Aesop.Forward.Substitution
Aesop.Substitution.instBEq : BEq Aesop.Substitution
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.toIsOrderedMonoid : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R], IsOrderedMonoid R
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.min? = some km → t.contains km = true
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineEquiv.affineSubspaceMap_apply : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁)
  [inst_7 : Nonempty ↥s] (x : ↥s), ↑((e.affineSubspaceMap s) x) = e ↑x
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.instTopologicalSpace : {α : Type u} → [inst : TopologicalSpace α] → TopologicalSpace (ConnectedComponents α)
-- Init.Data.List.Lemmas
/-- Variant of `filterMap_eq_map` with `some ∘ f` expanded out to a lambda.  -/
List.filterMap_eq_map' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, (List.filterMap fun x => some (f x)) = List.map f
-- Lean.Meta.LazyDiscrTree
/-- Returns rest of entry for later insertion.  -/
Lean.Meta.LazyDiscrTree.InitEntry.entry : {α : Type} → Lean.Meta.LazyDiscrTree.InitEntry α → Lean.Meta.LazyDiscrTree.LazyEntry α
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instIsLocallyFiniteMeasure : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {m : MeasurableSpace X}
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {m' : MeasurableSpace Y}
  {ν : MeasureTheory.Measure Y} [MeasureTheory.IsLocallyFiniteMeasure ν],
  MeasureTheory.IsLocallyFiniteMeasure (μ.prod ν)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
contMDiffOn_symm_coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_15 : MemTrivializationAtlas e] [inst_16 : MemTrivializationAtlas e'],
  ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b).symm)
    (e.baseSet ∩ e'.baseSet)
-- Init.Data.Array.Count
Array.countP_flatMap : ∀ {α : Type u_2} {β : Type u_1} {p : β → Bool} {xs : Array α} {f : α → Array β},
  Array.countP p (Array.flatMap f xs) = (Array.map (Array.countP p ∘ f) xs).sum
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instHasTerminalScheme : CategoryTheory.Limits.HasTerminal AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Category.AlgCat.TensorAlgebra
/-- Taking the tensor algebra forms a left adjoint of the forgetful functor from `AlgCat R` to
`ModuleCat R`.  -/
AlgCat.tensorAlgebraAdj : (R : Type u) → [inst : CommRing R] → AlgCat.tensorAlgebra R ⊣ CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.const_smul` -/
Differentiable.fun_const_smul : ∀ {𝕜 : 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] {f : E → F}
  {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F],
  Differentiable 𝕜 f → ∀ (c : R), Differentiable 𝕜 fun i => c • f i
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_le_ker_smul : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) (c : R₂), f.ker ≤ (c • f).ker
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The action of the tensor product on maps coming from `SimplexCategory`.  -/
AugmentedSimplexCategory.tensorHomOf : {x₁ y₁ x₂ y₂ : SimplexCategory} →
  (x₁ ⟶ y₁) → (x₂ ⟶ y₂) → (AugmentedSimplexCategory.tensorObjOf x₁ x₂ ⟶ AugmentedSimplexCategory.tensorObjOf y₁ y₂)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Fin.Embedding.append.congr_simp : ∀ {α : Type u_1} {m n : ℕ} {x x_1 : Fin m ↪ α} (e_x : x = x_1) {y y_1 : Fin n ↪ α} (e_y : y = y_1)
  (h : Disjoint (Set.range ⇑x) (Set.range ⇑y)), Fin.Embedding.append h = Fin.Embedding.append ⋯
-- Init.Data.BitVec.Lemmas
BitVec.ctz_eq_reverse_clz : ∀ {w : ℕ} {x : BitVec w}, x.ctz = x.reverse.clz
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.flip_separatingRight : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.flip.SeparatingRight ↔ B.SeparatingLeft
-- Std.Http.Protocol.H1
/-- Entry point for `Reader.State.needStartLine`.

Requests more data when input is currently empty, closes on EOF, and otherwise
dispatches to request-line/status-line parsing based on machine direction.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processNeedStartLine : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- To read a symbol from the tape, we use `readAux` to traverse the symbol,
then return to the original position with `n` moves to the left.  -/
Turing.TM1to1.read : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      {n : ℕ} →
        (List.Vector Bool n → Γ) →
          (Γ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂')
  (iso₃ : obj₃ ≅ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv.app j).hom₁ =
    iso₁.inv.app j
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.matched.injEq : ∀ {s : String.Slice} (startPos endPos startPos_1 endPos_1 : s.Pos),
  (String.Slice.Pattern.SearchStep.matched startPos endPos =
      String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1) =
    (startPos = startPos_1 ∧ endPos = endPos_1)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_neg : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
  MeasureTheory.L1.integral (-f) = -MeasureTheory.L1.integral f
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.starMemClass : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A], StarMemClass (StarSubalgebra R A) A
-- Init.Data.Option.Lemmas
Option.filter.eq_2 : ∀ {α : Type u_1} (p : α → Bool), Option.filter p none = none
-- Mathlib.RingTheory.HahnSeries.Basic
/-- If `Γ` is linearly ordered and `R` has zero, then `R⟦Γ⟧` consists of
formal series over `Γ` with coefficients in `R`, whose supports are well-founded.  -/
HahnSeries.«term__⟦_⟧» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv
      (CategoryTheory.Limits.pullback.fst f g) =
    (CategoryTheory.Limits.pushout.inl f.op g.op).unop
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_beth : ∀ (o : Ordinal.{u_1}), Cardinal.lift.{v, u_1} (Cardinal.beth o) = Cardinal.beth (Ordinal.lift.{v, u_1} o)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The base change of a bilinear map (also known as "extension of scalars").  -/
LinearMap.BilinMap.baseChange : {R : Type uR} →
  (A : Type uA) →
    {M₂ : Type uM₂} →
      {N₂ : Type uN₂} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N₂] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N₂] →
                      LinearMap.BilinMap R M₂ N₂ → LinearMap.BilinMap A (TensorProduct R A M₂) (TensorProduct R A N₂)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramerMap_is_linear : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (i : n), IsLinearMap α fun b => A.cramerMap b i
-- Mathlib.Order.Std
/-- `a < b` is equivalent to `a ≤ b ∧ ¬b ≤ a`.  -/
Preorder.OfStdArgs.lawfulOrderLT : ∀ {α : Type u_1} (self : Preorder.OfStdArgs α),
  let this := self.le;
  let this_1 := self.lt;
  Std.LawfulOrderLT α
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced : ∀ {C : Type u_3} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C),
  (CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp ((s b).map ((i a).hom.app X))
      (CategoryTheory.CategoryStruct.comp ((i b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).inv.app X))
          ((i (a + b)).inv.app X)))
-- Lean.Message
Lean.MessageData.instCoeList : Coe (List Lean.MessageData) Lean.MessageData
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.nat_succ : ∀ (n : ℕ), ↑n.succ = Order.succ ↑n
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => -f' x) =o[l] g ↔ f' =o[l] g
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.toHomeomorph_symm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
  [inst_4 : I.Boundaryless] (a : E), I.toHomeomorph.symm a = ↑I.symm a
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.toIsPreorder : ∀ {α : Type u} [self : Std.PreorderPackage α], Std.IsPreorder α
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.SurjOn f s (t i)) → Set.SurjOn f s (⋃ i, t i)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsPureDown : ∀ (P : Std.Do.SPred []), Std.Do.SPred.Tactic.IsPure P P.down
-- Lean.Meta.Sym.Arith.Poly
/-- Coefficient applied to polynomial `p₁`.  -/
Lean.Grind.CommRing.SPolResult.k₁ : Lean.Grind.CommRing.SPolResult → ℤ
-- Lean.Structure
Lean.StructureParentInfo.mk.injEq : ∀ (structName : Lean.Name) (subobject : Bool) (projFn structName_1 : Lean.Name) (subobject_1 : Bool)
  (projFn_1 : Lean.Name),
  ({ structName := structName, subobject := subobject, projFn := projFn } =
      { structName := structName_1, subobject := subobject_1, projFn := projFn_1 }) =
    (structName = structName_1 ∧ subobject = subobject_1 ∧ projFn = projFn_1)
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.TryThisInfo.mk.sizeOf_spec : ∀ (edit : Lean.Lsp.TextEdit) (codeActionTitle : String) (suggestion : Lean.Meta.Tactic.TryThis.Suggestion),
  sizeOf { edit := edit, codeActionTitle := codeActionTitle, suggestion := suggestion } =
    1 + sizeOf edit + sizeOf codeActionTitle + sizeOf suggestion