mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Protocol.H1
/-- Sends an error response with `Connection: close` and shuts down input.

If the machine is waiting to send a message, sends `status` with a `Connection: close`
header and signals that the body is done (letting the step function encode and flush the
response), then stops accepting further input. Otherwise, closes the writer directly and
stops accepting further input.
 -/
Std.Http.Protocol.H1.Machine.closeWithError : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
  Std.Http.Status → Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving
-- Mathlib.LinearAlgebra.StdBasis
Module.range_piEquiv : ∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Finite ι] [inst_1 : CommSemiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : ι → M), ((Module.piEquiv ι R M) v).range = Submodule.span R (Set.range v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.filter_equiv_self_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.Equiv t ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true),
      f (t.getKey a h) (Std.DTreeMap.Internal.Impl.Const.get t a h) = true
-- Mathlib.GroupTheory.Coset.Defs
/-- `α ⧸ s` is the quotient type representing the left cosets of `s`. If `s` is a
normal subgroup, `α ⧸ s` is a group  -/
QuotientAddGroup.instHasQuotientAddSubgroup : {α : Type u_1} → [inst : AddGroup α] → HasQuotient α (AddSubgroup α)
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_iff_norm'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r ↔ ‖b / a‖ < r
-- Mathlib.Data.Rel
SetRel.image_subset_iff : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {s : Set α} {t : Set β}, R.image s ⊆ t ↔ s ⊆ R.core t
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.prod_norm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  (x : WithCStarModule A (E × F)), ‖x‖ = √‖inner A x.1 x.1 + inner A x.2 x.2‖
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.all_bool_eq : ∀ {p : Char → Bool} {s : String.Slice}, s.all p = s.copy.toList.all p
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurableSet_countableFiltration_of_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (n : ℕ) {s : Set α},
  s ∈ MeasurableSpace.countablePartition α n → MeasurableSet s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F H G : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (ℌ :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
  (c j : C) {Z : V}
  (h :
    F.obj j ⟹
        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj j c) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (ℌ.coev_app.app c) (CategoryTheory.CategoryStruct.comp (ℌ.π c j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalClosed.curry ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (j, c))) h
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_monomial : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (a : R),
  (PowerSeries.coeff m) ((PowerSeries.monomial n) a) = if m = n then a else 0
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.IndepFun.cgf_add : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : ℝ} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (t * Y ω)) μ →
        ProbabilityTheory.cgf (X + Y) μ t = ProbabilityTheory.cgf X μ t + ProbabilityTheory.cgf Y μ t
-- Mathlib.Data.Set.Lattice.Image
Set.image2_sInter_subset_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (T : Set (Set β)),
  Set.image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, Set.image2 f s t
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_pow_le : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x : S) (n : ℕ), ‖x ^ n‖ ≤ ‖x‖
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.linear_bijective_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2),
  Function.Bijective ⇑f.linear ↔ Function.Bijective ⇑f
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.curry_left : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {s : Set (E × F)} {p : E × F},
  AnalyticWithinAt 𝕜 f s p → AnalyticWithinAt 𝕜 (fun x => f (x, p.2)) {x | (x, p.2) ∈ s} p.1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons.hinj : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} {V_1 : Type u} {G_1 : SimpleGraph V_1}
  {u_1 v_1 w_1 : V_1} {h_1 : G_1.Adj u_1 v_1} {p_1 : G_1.Walk v_1 w_1},
  V = V_1 →
    G ≍ G_1 →
      u ≍ u_1 →
        w ≍ w_1 →
          SimpleGraph.Walk.cons h p ≍ SimpleGraph.Walk.cons h_1 p_1 →
            V = V_1 ∧ G ≍ G_1 ∧ u ≍ u_1 ∧ v ≍ v_1 ∧ w ≍ w_1 ∧ p ≍ p_1
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) [Nontrivial S] (x : R), h.coeff ((algebraMap R S) x) = Pi.single 0 x
-- Mathlib.Topology.NhdsKer
nhdsKer_eq_nhdsKer_iff_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, nhdsKer s = nhdsKer t ↔ nhdsSet s = nhdsSet t
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.neg_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : IsTopologicalAddGroup N] (m : ι → M), (-f) m = -f m
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular mono category is a category in which every monomorphism is regular.  -/
CategoryTheory.IsRegularMonoCategory : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal] (X Y : D) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.LaxMonoidal.μ G X Y))
      (CategoryTheory.CategoryStruct.comp (adj.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)) h)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasSum.hasSum_iff_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {a₁ a₂ : α} {s : Set β}, HasSum (f ∘ Subtype.val) a₁ → (HasSum f a₂ ↔ HasSum (f ∘ Subtype.val) (a₂ - a₁))
-- Mathlib.Analysis.Normed.Ring.Basic
RingHomIsometric.enorm_map : ∀ {R₁ : Type u_5} {R₂ : Type u_6} [inst : SeminormedRing R₁] [inst_1 : SeminormedRing R₂] (σ : R₁ →+* R₂)
  [RingHomIsometric σ] (x : R₁), ‖σ x‖ₑ = ‖x‖ₑ
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInf_le_coverEntropy : ∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X) (F : Set X),
  Dynamics.coverEntropyInf T F ≤ Dynamics.coverEntropy T F
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkAndCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.mul_polyOfInterest_aux3 : ∀ (p n : ℕ),
  WittVector.wittPolyProd p (n + 1) =
    -(↑p ^ (n + 1) * MvPolynomial.X (0, n + 1)) * (↑p ^ (n + 1) * MvPolynomial.X (1, n + 1)) +
          ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
        ↑p ^ (n + 1) * MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
      WittVector.remainder p n
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_apply_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (b : M),
  e.symm (e b) = b
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_empty_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.deleteEdges ∅ = G'
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.diagonal_kroneckerTMul : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α] [inst_4 : Module R β]
  [inst_5 : DecidableEq l] (a : l → α) (B : Matrix m n β),
  Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) B =
    (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l))
      (Matrix.blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b)
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.State.mk.sizeOf_spec : ∀ (perfect : Bool), sizeOf { perfect := perfect } = 1 + sizeOf perfect
-- Mathlib.Topology.Order.MonotoneConvergence
iInf_eq_iInf_subseq_of_antitone : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : Preorder ι₂] [inst_1 : CompleteLattice α] {l : Filter ι₁}
  [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂}, Antitone f → Filter.Tendsto φ l Filter.atTop → ⨅ i, f i = ⨅ i, f (φ i)
-- Mathlib.Data.Finite.Defs
finite_iff_exists_equiv_fin : ∀ {α : Sort u_3}, Finite α ↔ ∃ n, Nonempty (α ≃ Fin n)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.IsComonHom M.equivMonComonUnitIsoAppX.hom
-- Lean.Server.CodeActions.Attr
/-- An extension which collects all the command code actions.  -/
Lean.CodeAction.cmdCodeActionExt : Lean.PersistentEnvExtension Lean.CodeAction.CommandCodeActionEntry
  (Lean.CodeAction.CommandCodeActionEntry × Lean.CodeAction.CommandCodeAction)
  (Array Lean.CodeAction.CommandCodeActionEntry × Lean.CodeAction.CommandCodeActions)
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_eq_localization_mk : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0),
  RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.num.inj : ∀ {v v_1 : ℕ}, Nat.Internal.Linear.Expr.num v = Nat.Internal.Linear.Expr.num v_1 → v = v_1
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_mul_det : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b b' b'' : Module.Basis ι A M), b.det ⇑b' * b'.det ⇑b'' = b.det ⇑b''
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] {f g : α →*o β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_whiskerLeft_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g h : b ⟶ c) (θ : g ⟶ h),
  (CategoryTheory.Bicategory.whiskerLeft f θ).1 = CategoryTheory.Bicategory.whiskerLeft f.1 θ.1
-- Init.Data.Array.Lemmas
Array.foldl_map' : ∀ {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {xs : Array β₁} {init : α} {stop : ℕ},
  stop = xs.size → Array.foldl g init (Array.map f xs) 0 stop = Array.foldl (fun x y => g x (f y)) init xs
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle.lift_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁]
  {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : (j : J) → T' ⟶ T j),
  (CategoryTheory.Pretriangulated.productTriangle.lift T φ).hom₂ = CategoryTheory.Limits.Pi.lift fun j => (φ j).hom₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyLT_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, compare a k = Ordering.lt},
  Std.DTreeMap.Internal.Impl.getKeyLT k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getKeyLT k t₂ ⋯ ⋯
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optType.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_pmap : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} [inst : Monad m] [LawfulMonad m] {x : Std.Iterators.HetT m α}
  {f : (a : α) → x.Property a → β}, (x.pmap f).Property = fun b => ∃ a, ∃ (h : x.Property a), f a h = b
-- Mathlib.Order.Concept
/-- The concept generated by a single object.  -/
Concept.ofObject : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → α → Concept α β r
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Product of additive subgroups is isomorphic to their product
as additive groups  -/
AddSubgroup.prodEquiv : {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.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.instHasKernelFst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.HasKernel CategoryTheory.Limits.biprod.fst
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_symm : ∀ {α : Type u_1}, SymAlg.unsym.symm = SymAlg.sym
-- Mathlib.SetTheory.ZFC.Ordinal
/-- `Ordinal` is order-equivalent to the type of von Neumann ordinals.  -/
Ordinal.toZFSetIso : Ordinal.{u_1} ≃o { x // x.IsOrdinal }
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.copyCount_bot : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V), G.copyCount ⊥ = 1
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.bind_pure : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type w} {x : Std.Iterators.PostconditionT m α},
  x.bind pure = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), Std.Internal.List.getKey? a l = some (Std.Internal.List.getKey a l h)
-- Mathlib.Topology.Separation.Regular
instT3SpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T3Space X] [T3Space Y],
  T3Space (X × Y)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isBoundedUnder_le_exp_comp : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => Real.exp (f x)) ↔
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f
-- Init.Data.BitVec.Lemmas
BitVec.add_zero : ∀ {n : ℕ} (x : BitVec n), x + 0#n = x
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_mul : ∀ (p q : Polynomial ℂ), (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Around the image of a point in the source, the neighborhoods are the same
within `(extChartAt I x).target` and within `range I`.  -/
nhdsWithin_extChartAt_target_eq' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x y : M},
  y ∈ (extChartAt I x).source →
    nhdsWithin (↑(extChartAt I x) y) (extChartAt I x).target = nhdsWithin (↑(extChartAt I x) y) (Set.range ↑I)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.PreDiscrTree.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (root : Std.HashMap Lean.Meta.RefinedDiscrTree.Key ℕ)
  (tries : Array (Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α))),
  sizeOf { root := root, tries := tries } = 1 + sizeOf root + sizeOf tries
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For `1 ≤ r`, the logarithmic counting function for the poles of `f * g` is less than or equal to the
sum of the logarithmic counting functions for the poles of `f` and `g`, respectively.
 -/
ValueDistribution.logCounting_mul_top_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.logCounting (f₁ * f₂) ⊤ r ≤
              (ValueDistribution.logCounting f₁ ⊤ + ValueDistribution.logCounting f₂ ⊤) r
-- Lean.Environment
/-- Consistently updates synchronous and (private) asynchronous parts of the environment without blocking.  -/
_private.Lean.Environment.0.Lean.Environment.modifyCheckedAsync : Lean.Environment → (Lean.Kernel.Environment → Lean.Kernel.Environment) → Lean.Environment
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.equivMapOfInjective_coe_mulEquiv : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (e : G ≃* G'),
  H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H
-- Init.Data.Vector.Lemmas
Vector.map_append : ∀ {α : Type u_1} {β : Type u_2} {n m : ℕ} {f : α → β} {xs : Vector α n} {ys : Vector α m},
  Vector.map f (xs ++ ys) = Vector.map f xs ++ Vector.map f ys
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The set of skew-adjoint endomorphisms of a module with bilinear map is a submodule. (In fact
it is a Lie subalgebra.)  -/
LinearMap.skewAdjointSubmodule : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup M₂] → [inst_4 : Module R M₂] → (M →ₗ[R] M →ₗ[R] M₂) → Submodule R (Module.End R M)
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.maxRSS : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Order.RelClasses
Std.Trichotomous.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Trichotomous r], Std.Trichotomous (Function.swap r)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_abs_abs : ∀ {α : Type u_1} {l : Filter α} {u v : α → ℝ}, ((fun x => |u x|) =o[l] fun x => |v x|) ↔ u =o[l] v
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsAlt.neg : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsAlt → ∀ (x y : M₁), -(B x) y = (B y) x
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a cyclotomic
extension of `ℚ`.  -/
IsPrimitiveRoot.subOneIntegralPowerBasis : {n : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [NeZero n] →
          [inst_2 : CharZero K] →
            [IsCyclotomicExtension {n} ℚ K] → IsPrimitiveRoot ζ n → PowerBasis ℤ (NumberField.RingOfIntegers K)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- Version of `PowerSeries.IsWeierstrassDivisionAt` for local rings with respect to
its maximal ideal.  -/
PowerSeries.IsWeierstrassDivision : {A : Type u_1} →
  [inst : CommRing A] → PowerSeries A → PowerSeries A → PowerSeries A → Polynomial A → [IsLocalRing A] → Prop
-- Mathlib.Algebra.Jordan.Basic
IsJordan.lmul_comm_rmul : ∀ {A : Type u_1} {inst : Mul A} [self : IsJordan A] (a b : A), a * b * a = a * (b * a)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The proposition that a sesquilinear map is alternating  -/
LinearMap.IsAlt : {R : Type u_1} →
  {R₁ : Type u_2} →
    {M : Type u_5} →
      {M₁ : Type u_6} →
        [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₁] → {I₁ I₂ : R₁ →+* R} → (M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) → Prop
-- Mathlib.Order.Defs.LinearOrder
le_max_right : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), b ≤ max a b
-- Mathlib.Data.Countable.Basic
instCountableForallOfFinite : ∀ {α : Sort u} {π : α → Sort w} [Finite α] [∀ (a : α), Countable (π a)], Countable ((a : α) → π a)
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
/-- `log` as an arithmetic function `ℕ → ℝ`. Note this is in the `ArithmeticFunction`
namespace to indicate that it is bundled as an `ArithmeticFunction` rather than being the usual
real logarithm.  -/
ArithmeticFunction.log : ArithmeticFunction ℝ
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- A shorthand for the predicate that we are proving in the main theorems `trStmts₁_supports`,
`codeSupp'_supports`, `contSupp_supports`, `codeSupp_supports`. The set `S` is fixed throughout
the proof, and denotes the full set of states in the machine, while `K` is a subset that we are
currently proving a property about. The predicate asserts that every state in `K` is closed in `S`
under forward simulation, i.e. stepping forward through evaluation starting from any state in `K`
stays entirely within `S`.  -/
Turing.PartrecToTM2.Supports : Finset Turing.PartrecToTM2.Λ' → Finset Turing.PartrecToTM2.Λ' → Prop
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.expand_card : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] (f : Polynomial K),
  (Polynomial.expand K (Fintype.card K)) f = f ^ Fintype.card K
-- Mathlib.Topology.EMetricSpace.Defs
EMetricSpace.ext : ∀ {α : Type u_2} {m m' : EMetricSpace α}, m.toEDist = m'.toEDist → m = m'