mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.eq_bot_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] (I : HomogeneousIdeal 𝒜),
  I = ⊥ ↔ I.toIdeal = ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertList_insertEntry_right_equiv_insertEntry_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} (p : (a : α) × β a),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      (Std.Internal.List.insertList l (Std.Internal.List.insertEntry p.fst p.snd toInsert)).Perm
        (Std.Internal.List.insertEntry p.fst p.snd (Std.Internal.List.insertList l toInsert))
-- Std.Http.Data.Headers
/-- Adds a header from string name and value, panicking if either is invalid.
 -/
Std.Http.Headers.insert! : Std.Http.Headers → String → String → Std.Http.Headers
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.hom_ext' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  {Z : C} {Δ : SimplexCategoryᵒᵖ} (f g : X.obj Δ ⟶ Z),
  (∀ (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
      CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) f =
        CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) g) →
    f = g
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk : {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] →
              (carrier : Set P) →
                (∀ (c : k) {p₁ p₂ p₃ : P},
                    p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier) →
                  AffineSubspace k P
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.AddMon.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.le_centralizer_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Subalgebra R A},
  s ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R ↑s)
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_self_right : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  dualTensorHom R M R = ↑(TensorProduct.rid R (Module.Dual R M))
-- Init.Data.Nat.Lcm
Nat.lcm_ne_zero : ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.lcm n ≠ 0
-- Mathlib.Topology.Algebra.InfiniteSum.Order
multipliable_mabs_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α]
  [inst_3 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α] {f : ι → α},
  (Multipliable fun x => |f x|ₘ) ↔ Multipliable f
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.add_zero : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), a + 0 = a
-- Std.Do.PostCond
/-- Conjunction of postconditions.

This is defined pointwise, as the conjunction of the assertions about the return value and the
conjunctions of the assertions about each potential exception.
 -/
Std.Do.PostCond.and : {α : Type u_1} → {ps : Std.Do.PostShape} → Std.Do.PostCond α ps → Std.Do.PostCond α ps → Std.Do.PostCond α ps
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toArray_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Raw.map f t).toArray = Array.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toArray
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
equivTangentBundleProd_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) (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  (M' : Type u_7) [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  (p : TangentBundle (I.prod I') (M × M')),
  (equivTangentBundleProd I M I' M') p = (⟨p.proj.1, p.snd.1⟩, ⟨p.proj.2, p.snd.2⟩)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If a function and its derivative are integrable on `(a, +∞)`, then the function tends to zero
at `+∞`.  -/
MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi : ∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x) →
    MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
      MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume → Filter.Tendsto f Filter.atTop (nhds 0)
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNat' : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNat n).toUInt16 = UInt16.ofNat n
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Each column sum of a doubly stochastic matrix is 1.  -/
sum_col_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n → ∀ (j : n), ∑ i, M i j = 1
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.coe_id : ∀ (α : Type u_1) [inst : TopologicalSpace α], ⇑(CocompactMap.id α) = id
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.mk.sizeOf_spec : ∀ (m returnType expectedType : Lean.Expr),
  sizeOf { m := m, returnType := returnType, expectedType := expectedType } =
    1 + sizeOf m + sizeOf returnType + sizeOf expectedType
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.iff_iff_imp_and_imp : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n},
  T.Iff φ ψ ↔ T.Imp φ ψ ∧ T.Imp ψ φ
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.aeval.congr_simp : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a a_1 : σ → S} (e_a : a = a_1) [inst_4 : IsTopologicalSemiring R]
  [inst_5 : IsUniformAddGroup R] [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S]
  [inst_9 : IsTopologicalRing S] [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S]
  (ha : MvPowerSeries.HasEval a), MvPowerSeries.aeval ha = MvPowerSeries.aeval ⋯
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.mk.injEq : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (toFun : E → F)
  (contDiff' : ContDiff ℝ (↑n) toFun) (zero_on_compl' : Set.EqOn toFun 0 (↑K)ᶜ) (toFun_1 : E → F)
  (contDiff'_1 : ContDiff ℝ (↑n) toFun_1) (zero_on_compl'_1 : Set.EqOn toFun_1 0 (↑K)ᶜ),
  ({ toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' } =
      { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 }) =
    (toFun = toFun_1)
-- Init.Data.UInt.Bitwise
UInt32.right_le_or : ∀ {a b : UInt32}, b ≤ a ||| b
-- Init.Data.Array.Monadic
Array.foldlM_filterMap : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {stop : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : α → Option β} {g : γ → β → m γ} {xs : Array α} {init : γ} {w : stop = (Array.filterMap f xs).size},
  Array.foldlM g init (Array.filterMap f xs) 0 stop =
    Array.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init xs
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_bitVecToInt : ∀ (n : BitVec 64), Int64.ofIntLE n.toInt ⋯ ⋯ = Int64.ofBitVec n
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.ofIsoObj_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  (R : F.RepresentableBy X) (e : Y ≅ X) {Z : C}, (R.ofIsoObj e).homEquiv = e.homToEquiv.trans R.homEquiv
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.CoherenceHom.mk : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ → Lean.Expr → Lean.Expr → Mathlib.Tactic.BicategoryLike.CoherenceHom
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- To check this condition when the space already has a real normed space structure,
use `Convex.convex_isRCLikeNormedField` which eliminates the `letI`s below, or the constructor
`ModelWithCorners.ofConvexRange`  -/
ModelWithCorners.convex_range' : ∀ {𝕜 : 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] (self : ModelWithCorners 𝕜 E H),
  if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑self.toPartialEquiv)
  else Set.range ↑self.toPartialEquiv = Set.univ
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.compatible : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y},
  Continuous f → ∀ (a b : X), a ≈ b → f a = f b
-- Mathlib.Analysis.InnerProductSpace.Basic
isSymm_inner : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E], (innerₗ E).IsSymm
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.mk : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {E : Type u_11} →
            {E₂ : Type u_12} →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] →
                  [inst_4 : Module R E] →
                    [inst_5 : Module R₂ E₂] →
                      (toLinearMap : E →ₛₗ[σ₁₂] E₂) → (∀ (x : E), ‖toLinearMap x‖ = ‖x‖) → E →ₛₗᵢ[σ₁₂] E₂
-- Mathlib.Data.Set.Sups
Set.sups_subset : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂
-- Mathlib.Algebra.MvPolynomial.SchwartzZippel
/-- The **Schwartz-Zippel lemma**

For a nonzero multivariable polynomial `p` over an integral domain, the probability that `p`
evaluates to zero at points drawn at random from a product of finite subsets `S i` of the integral
domain is bounded by the sum of `degᵢ p / #(S i)`.  -/
MvPolynomial.schwartz_zippel_sum_degreeOf : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [inst_2 : DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R},
  p ≠ 0 →
    ∀ (S : Fin n → Finset R),
      ↑{x ∈ Fintype.piFinset fun i => S i | (MvPolynomial.eval x) p = 0}.card / ∏ i, ↑(S i).card ≤
        ∑ i, ↑(MvPolynomial.degreeOf i p) / ↑(S i).card
-- Std.Time.Time.Unit.Millisecond
/-- Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds.
 -/
Std.Time.Millisecond.Ordinal.ofFin : Fin 1000 → Std.Time.Millisecond.Ordinal
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_restrictScalars_comp_includeRight : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D),
  (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight =
    Algebra.TensorProduct.includeRight.comp g
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_long_short : ∀ {ι : 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} [self : P.EmbeddedG2],
  P.pairingIn ℤ (RootPairing.EmbeddedG2.long P) (RootPairing.EmbeddedG2.short P) = -3
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given left-open right-closed range.
 -/
Std.Roc.size : {α : Type u} → [Std.Rxc.HasSize α] → [Std.PRange.UpwardEnumerable α] → Std.Roc α → ℕ
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_inf'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (fun a => s.inf' hne fun x => f x a) x
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryLED : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α × β → α × β
-- Mathlib.Combinatorics.Quiver.Path
/-- An arrow viewed as a path of length one.  -/
Quiver.Hom.toPath : {V : Type u_1} → [inst : Quiver V] → {a b : V} → (a ⟶ b) → Quiver.Path a b
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul_of_lt_of_le : ∀ {a c b d : ℕ}, a < c → b ≤ d → 0 < d → a * b < c * d
-- Mathlib.Analysis.Normed.Operator.Banach
/-- A (possibly nonlinear) right inverse to a continuous linear map, which doesn't have to be
linear itself but which satisfies a bound `‖inverse x‖ ≤ C * ‖x‖`. A surjective continuous linear
map doesn't always have a continuous linear right inverse, but it always has a nonlinear inverse
in this sense, by Banach's open mapping theorem.  -/
ContinuousLinearMap.NonlinearRightInverse : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] → [inst_5 : NormedSpace 𝕜' F] → (E →SL[σ] F) → Type (max u_3 u_4)
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ‖f'‖` the ratio
`‖f z - f x‖ / ‖z - x‖` is frequently less than `r` as `z → x+0`.
In other words, the limit inferior of this ratio as `z` tends to `x+0`
is less than or equal to `‖f'‖`. See also `HasDerivWithinAt.limsup_norm_slope_le`
for a stronger version using limit superior and any set `s`.  -/
HasDerivWithinAt.liminf_right_norm_slope_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {f' : E} {x r : ℝ},
  HasDerivWithinAt f f' (Set.Ici x) x → ‖f'‖ < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), ‖z - x‖⁻¹ * ‖f z - f x‖ < r
-- Mathlib.Order.Filter.Bases.Basic
/-- Definition of `HasBasis` unfolded with implicit set argument.  -/
Filter.HasBasis.mem_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α},
  l.HasBasis p s → (t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t)
-- Mathlib.Data.List.Sort
List.sortedGE_insertionSort : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α], (List.insertionSort (fun x1 x2 => x1 ≥ x2) l).SortedGE
-- Mathlib.Algebra.Group.Submonoid.Operations
AddEquiv.ofLeftInverse'_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) {g : N → M}
  (h : Function.LeftInverse g ⇑f) (a : M), (AddEquiv.ofLeftInverse' f h) a = f.mrangeRestrict a
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
NumberField.Ideal.primesOverSpanEquivMonicFactorsMod.congr_simp : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K} {p : ℕ} [inst_1 : Fact (Nat.Prime p)]
  [inst_2 : NumberField K] (hp : ¬p ∣ RingOfIntegers.exponent θ),
  NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp = NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
/-- An alternative characterization of the Grothendieck topology associated to a precoverage `J`:
it is the infimum of all Grothendieck topologies containing `Sieve.generate S` for all presieves
`S` in `J`.
 -/
CategoryTheory.Precoverage.toGrothendieck_eq_sInf : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (J : CategoryTheory.Precoverage C),
  J.toGrothendieck = sInf {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, CategoryTheory.Sieve.generate S ∈ K X}
-- Mathlib.Topology.Compactness.Compact
/-- If `s : Set S` belongs to `l ⊓ 𝓝 x` for all `x` from a compact set `K`,
then it belongs to `l ⊓ (𝓝ˢ K)`,
i.e., there exist `T ∈ l` and an open `U ⊇ K` such that `T ∩ U ⊆ s`.  -/
IsCompact.mem_inf_nhdsSet_of_forall : ∀ {X : Type u} [inst : TopologicalSpace X] {K : Set X} {l : Filter X} {s : Set X},
  IsCompact K → (∀ y ∈ K, s ∈ l ⊓ nhds y) → s ∈ l ⊓ nhdsSet K
-- Std.Http.Data.Body.Stream
Std.Http.Body.Stream.instNextChunkContextAsync : Std.Http.Body.Stream.NextChunk Std.Async.ContextAsync
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.extract.go₁.match_1.eq_2 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → Sort u_1) (c : Char) (cs : List Char)
  (i b e : String.Pos.Raw) (h_1 : (x x_1 x_2 : String.Pos.Raw) → motive [] x x_1 x_2)
  (h_2 :
    (s : List Char) → (c : Char) → (cs : List Char) → s = c :: cs → (i b e : String.Pos.Raw) → motive (c :: cs) i b e),
  (match c :: cs, i, b, e with
    | [], x, x_1, x_2 => h_1 x x_1 x_2
    | s@h:(c :: cs), i, b, e => h_2 s c cs h i b e) =
    h_2 (c :: cs) c cs ⋯ i b e
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.one_apply_eq : ∀ {n : Type u_2} {A : Type u_5} [inst : DecidableEq n] [inst_1 : Zero A] [inst_2 : One A] (i : n), 1 i i = 1
-- Lean.Elab.InfoTree.Types
/-- The information needed to render the tactic state in the infoview.

We store the list of goals before and after the execution of a tactic.
We also store the metavariable context at each time since we want metavariables
unassigned at tactic execution time to be displayed as `?m...`.  -/
Lean.Elab.TacticInfo : Type
-- Mathlib.Order.Heyting.Basic
himp_iff_imp : ∀ (p q : Prop), p ⇨ q ↔ p → q
-- Mathlib.Topology.Instances.CantorSet
/-- If two base-3 representations using only digits `0` and `2` define the same number,
then the sequences must be equal.
This uniqueness fails for general base-3 representations (e.g. `0.1000... = 0.0222...`).  -/
ofDigits_zero_two_sequence_unique : ∀ {a b : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → (∀ (n : ℕ), b n ≠ 1) → Real.ofDigits a = Real.ofDigits b → a = b
-- Mathlib.Analysis.Complex.Basic
Complex.summable_ofReal : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℝ}, Summable (fun x => ↑(f x)) L ↔ Summable f L
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.liftMonoid_coe_addMonoidHom : ∀ {α : Type u} {R : Type u_2} [inst : Monoid α] [inst_1 : Ring R] (f : α →* R),
  ↑(FreeAbelianGroup.liftMonoid f) = FreeAbelianGroup.lift ⇑f
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpImpl : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.ofList l cmp).get? k = none
-- Mathlib.Data.Sign.Defs
/-- A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the `Fintype` deriving handler.) -/
SignType.enumList : List SignType
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotent_center_quotient_ind`.

---

A custom induction principle for nilpotent groups. The base case is a trivial group
(`subsingleton G`), and in the induction step, one can assume the hypothesis for
the group quotiented by its center.  -/
nilpotent_center_quotient_ind : ∀ {P : (G : Type u_2) → [inst : Group G] → [Group.IsNilpotent G] → Prop} (G : Type u_2) [inst : Group G]
  [inst_1 : Group.IsNilpotent G],
  (∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G) →
    (∀ (G : Type u_2) [inst : Group G] [inst_2 : Group.IsNilpotent G], P (G ⧸ Subgroup.center G) → P G) → P G
-- Lean.Elab.BuiltinCommand
/-- Returns the first suffix of `base` that begins with `seg`, if one exists.

Note: this uses a naive, O(m*n) implementation for simplicity; we assume repeated partial overlap of
name components to be relatively uncommon, so that practical performance is closer to linear.
 -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.findSuffixWithPrefix : Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Data.Rel
/-- The maximal symmetric relation contained in a given relation.  -/
SetRel.symmetrize : {α : Type u_1} → SetRel α α → SetRel α α
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balance_eq_balance' : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced → r.Balanced → l.Sized → r.Sized → l.balance x r = l.balance' x r
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_apply_def : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0] (x : R), 1 x = if x = 0 then 0 else 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.CooperSplit),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂ c) = 1 + sizeOf c
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_filter_eq_size_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF → ((Std.TreeMap.Raw.filter f t).size = t.size ↔ ∀ (a : α) (h : a ∈ t), f (t.getKey a h) t[a] = true)
-- Mathlib.Data.Vector.Basic
List.Vector.tail_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (v : List.Vector α (n + 1)) (f : α → β),
  (List.Vector.map f v).tail = List.Vector.map f v.tail
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.instHasTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Limits.HasTerminal (CategoryTheory.Comon C)
-- Init.PropLemmas
forall_or_eq_imp' : ∀ {α : Sort u_1} {a' : α} {P Q : α → Prop}, (∀ (a : α), Q a ∨ a' = a → P a) ↔ (∀ (a : α), Q a → P a) ∧ P a'
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_one : Cardinal.preBeth 1 = 1
-- Mathlib.Topology.Algebra.Constructions
/-- An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead.  -/
AddUnits.embedding_val_mk : ∀ {M : Type u_4} [inst : SubtractionMonoid M] [inst_1 : TopologicalSpace M],
  ContinuousOn Neg.neg {x | IsAddUnit x} → Topology.IsEmbedding AddUnits.val
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_def : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddCommMonoid N]
  (f : SkewMonoidAlgebra k G) (g : G → k → N), f.sum g = f.coeff.sum g
-- Mathlib.Data.WSeq.Defs
Stream'.WSeq.IsFinite.out : ∀ {α : Type u} {s : Stream'.WSeq α} [self : s.IsFinite], s.toList.Terminates
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Every diagram indexing a pushout is naturally isomorphic (actually, equal) to a `span`  -/
CategoryTheory.Limits.diagramIsoSpan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C) →
      F ≅
        CategoryTheory.Limits.span (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
          (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)