mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.intersecting_singleton : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a : α}, {a}.Intersecting ↔ a ≠ ⊥
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_null_iff_singleton : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s : Set α}, s.Countable → (μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0)
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseOffsetZ : (Std.Time.OffsetZ → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Lean.Elab.AssertExists
/-- `#check_assertions` retrieves all declarations and all imports that were declared
not to exist so far (including in transitively imported files) and reports their current
status:
* ✓ means the declaration or import exists,
* × means the declaration or import does not exist.

This means that the expectation is that all checks *succeed* by the time `#check_assertions`
is used, typically once all of the library has been built.

If all declarations and imports are available when `#check_assertions` is used,
then the command logs an info message. Otherwise, it emits a warning.

The variant `#check_assertions!` only prints declarations/imports that are not present in the
environment. In particular, it is silent if everything is imported, making it useful for testing.
 -/
Lean.Elab.Command.elabCheckAssertions : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.addAction.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : DecidableEq α] [inst_2 : AddMonoid α]
  [inst_3 : AddAction α β], Finset.addAction = { toVAdd := Finset.vadd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_div_two_sub : ∀ (x : ℝ), Real.cos (Real.pi / 2 - x) = Real.sin x
-- Mathlib.MeasureTheory.Integral.Prod
/-- The map that sends an L¹-function `f : α × β → E` to `∫∫f` is continuous.  -/
MeasureTheory.continuous_integral_integral : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ], Continuous fun f => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Matrix.spectrum_toLin' : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] (A : Matrix n n R),
  spectrum R (Matrix.toLin' A) = spectrum R A
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.instInhabited : {R : Type u_1} →
  {E : Type u_5} →
    [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → Inhabited (E →ₗᵢ[R] E)
-- Lean.Data.Json.Basic
Lean.JsonNumber.mk.inj : ∀ {mantissa : ℤ} {exponent : ℕ} {mantissa_1 : ℤ} {exponent_1 : ℕ},
  { mantissa := mantissa, exponent := exponent } = { mantissa := mantissa_1, exponent := exponent_1 } →
    mantissa = mantissa_1 ∧ exponent = exponent_1
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.instInhabited.eq_1 : GrpCat.instInhabited = { default := GrpCat.of PUnit.{u_1 + 1} }