mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniformly_extend_exists : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {e : β → α},
  IsUniformInducing e →
    DenseRange e →
      ∀ {f : β → γ},
        UniformContinuous f → ∀ [CompleteSpace γ] (a : α), ∃ c, Filter.Tendsto f (Filter.comap e (nhds a)) (nhds c)
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquivOfImageEq_source : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α) (t : Set β) (h : ⇑e '' s = t),
  (e.toPartialEquivOfImageEq s t h).source = s
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.extension_instLieAlgebra : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : LieAlgebra.IsExtension i p),
  h.extension.instLieAlgebra = inst_2
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (result? : Option Lean.Language.Lean.HeaderProcessedState) (toSnapshot_1 : Lean.Language.Snapshot)
  (metaSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (result?_1 : Option Lean.Language.Lean.HeaderProcessedState),
  ({ toSnapshot := toSnapshot, metaSnap := metaSnap, result? := result? } =
      { toSnapshot := toSnapshot_1, metaSnap := metaSnap_1, result? := result?_1 }) =
    (toSnapshot = toSnapshot_1 ∧ metaSnap = metaSnap_1 ∧ result? = result?_1)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRight_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E)
  {X Y : CategoryTheory.Functor C D} (α : X ⟶ Y),
  ((CategoryTheory.Functor.whiskeringRight C D E).obj H).map α = CategoryTheory.Functor.whiskerRight α H
-- Mathlib.Algebra.Quaternion
Quaternion.imK_neg : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (-a).imK = -a.imK
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
SzemerediRegularity.chunk.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ) {U : Finset α} (hU : U ∈ P.parts),
  SzemerediRegularity.chunk hP G ε hU =
    if hUcard :
        U.card =
          Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card +
            (Fintype.card α / P.parts.card -
              Fintype.card α / SzemerediRegularity.stepBound P.parts.card * 4 ^ P.parts.card) then
      Finpartition.equitabilise ⋯
    else Finpartition.equitabilise ⋯
-- Mathlib.Algebra.Quandle
/-- The *adjoint action* of a rack on itself is `op'`, and the adjoint
action of `x ◃ y` is the conjugate of the action of `y` by the action
of `x`. It is another way to understand the self-distributivity axiom.

This is used in the natural rack homomorphism `toConj` from `R` to
`Conj (R ≃ R)` defined by `op'`.
 -/
Rack.ad_conj : ∀ {R : Type u_2} [inst : Rack R] (x y : R), Rack.act' (Shelf.act x y) = Rack.act' x * Rack.act' y * (Rack.act' x)⁻¹
-- Mathlib.Topology.DerivedSet
Continuous.image_derivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {β : Type u_2} [inst_1 : TopologicalSpace β] {A : Set X} {f : X → β},
  Continuous f → Function.Injective f → f '' derivedSet A ⊆ derivedSet (f '' A)
-- Mathlib.Data.Real.Pointwise
Real.iInf_mul_of_nonneg : ∀ {ι : Sort u_1} {r : ℝ}, 0 ≤ r → ∀ (f : ι → ℝ), (⨅ i, f i) * r = ⨅ i, f i * r
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_norm_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp (fun x => ‖f x‖) p ↔ Memℓp f p
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.prodEquivOfIsTopCompl_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q)
  (x : ↥p × ↥q), (p.prodEquivOfIsTopCompl q h) x = ↑x.1 + ↑x.2
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constSMul.eq_1 : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : IsIsometricSMul G X] (c : G),
  IsometryEquiv.constSMul c = { toEquiv := MulAction.toPerm c, isometry_toFun := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.transposeInvertibleEquivInvertible_symm_apply : ∀ {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring α] (A : Matrix n n α)
  [inst_3 : Invertible A], A.transposeInvertibleEquivInvertible.symm inst_3 = A.invertibleTranspose
-- Mathlib.RingTheory.Artinian.Algebra
IsArtinianRing.isUnit_submonoid_eq_of_isIntegral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [IsArtinianRing R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  [Algebra.IsIntegral R A], IsUnit.submonoid A = nonZeroDivisors A
-- Mathlib.Logic.Equiv.Prod
Equiv.funSplitAt_symm_apply : ∀ {α : Type u_9} [inst : DecidableEq α] (i : α) (β : Type u_10)
  (f : (fun a => β) i × ((j : { j // j ≠ i }) → (fun a => β) ↑j)) (j : α),
  (Equiv.funSplitAt i β).symm f j = if h : j = i then f.1 else f.2 ⟨j, ⋯⟩
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommGroup : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [CommGroup G] → CommGroup (l.Germ G)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.any_eq_true_iff_exists_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p a (Std.DHashMap.Const.get m a h) = true
-- Mathlib.Logic.Unique
Unique.subsingleton_unique' : ∀ {α : Sort u_1} (h₁ h₂ : Unique α), h₁ = h₂
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
/-- This coincides with `φ₀` when `HasCardinalLT B κ₂` holds.  -/
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ : {κ₁ κ₂ : Cardinal.{w}} →
  {X : Type w} →
    (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)) →
      ((B : Set X) →
          (hB : HasCardinalLT (↑B) κ₂) →
            (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X) →
        Set X → Set X
-- Lean.Meta.Basic
/-- `fun _ : Unit => a`  -/
Lean.Meta.mkFunUnit : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ioc_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c + b) (d + b)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.refl : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀},
  v.IsEquiv v
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.NoPrefixPatternModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat],
  (∀ (s t : String),
      String.Slice.Pattern.Model.PatternModel.Matches pat s →
        String.Slice.Pattern.Model.PatternModel.Matches pat (s ++ t) → t = "") →
    String.Slice.Pattern.Model.NoPrefixPatternModel pat
-- Mathlib.Computability.Primrec.Basic
Primcodable.unit : Primcodable PUnit.{u_1 + 1}
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of two vectors, divided by the product of their
norms, has absolute value 1 if and only if they are nonzero and one is
a multiple of the other. One form of equality case for Cauchy-Schwarz.  -/
abs_real_inner_div_norm_mul_norm_eq_one_iff : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  |inner ℝ x y / (‖x‖ * ‖y‖)| = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.add_neg : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Predicate asserting the word `L` admits no reduction steps,
i.e., no two neighboring elements of the word cancel.  -/
FreeAddGroup.IsReduced : {α : Type u} → List (α × Bool) → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- The property of scheme morphisms `SmoothOfRelativeDimension n` is associated with the ring
homomorphism property `Locally (IsStandardSmoothOfRelativeDimension n)`.  -/
AlgebraicGeometry.instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension : ∀ (n : ℕ),
  AlgebraicGeometry.HasRingHomProperty (@AlgebraicGeometry.SmoothOfRelativeDimension n)
    fun {R S} [CommRing R] [CommRing S] =>
    RingHom.Locally fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension n
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.cons.injEq : ∀ {α : Type u} (rank : ℕ) (val : α) (node : Batteries.BinomialHeap.Imp.HeapNode α)
  (next : Batteries.BinomialHeap.Imp.Heap α) (rank_1 : ℕ) (val_1 : α) (node_1 : Batteries.BinomialHeap.Imp.HeapNode α)
  (next_1 : Batteries.BinomialHeap.Imp.Heap α),
  (Batteries.BinomialHeap.Imp.Heap.cons rank val node next =
      Batteries.BinomialHeap.Imp.Heap.cons rank_1 val_1 node_1 next_1) =
    (rank = rank_1 ∧ val = val_1 ∧ node = node_1 ∧ next = next_1)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.prevAux.go.match_1.eq_1 : ∀ {s : String.Slice}
  (motive :
    (off : ℕ) →
      (h₁ : off < s.utf8ByteSize) → ¬(s.getUTF8Byte { byteIdx := off } h₁).IsUTF8FirstByte → 0 ≠ off → Sort u_1)
  (h₁ : 0 < s.utf8ByteSize) (hbyte : ¬(s.getUTF8Byte { } h₁).IsUTF8FirstByte) (this : 0 ≠ 0)
  (h_1 :
    (h₁ : 0 < s.utf8ByteSize) →
      (hbyte : ¬(s.getUTF8Byte { } h₁).IsUTF8FirstByte) → (this : 0 ≠ 0) → motive 0 h₁ hbyte this)
  (h_2 :
    (off : ℕ) →
      (h₁ : off + 1 < s.utf8ByteSize) →
        (hbyte : ¬(s.getUTF8Byte { byteIdx := off + 1 } h₁).IsUTF8FirstByte) →
          (this : 0 ≠ off + 1) → motive off.succ h₁ hbyte this),
  (match 0, h₁, hbyte, this with
    | 0, h₁, hbyte, this => h_1 h₁ hbyte this
    | off.succ, h₁, hbyte, this => h_2 off h₁ hbyte this) =
    h_1 h₁ hbyte this
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_cancel : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (a : R) (b c : ↥M),
  IsLocalization.mk' S (a * ↑c) (b * c) = IsLocalization.mk' S a b
-- Init.Data.UInt.Bitwise
UInt32.toBitVec_not : ∀ {a : UInt32}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Algebra.GradedMonoid
/-- A type alias of sigma types for graded monoids.  -/
GradedMonoid : {ι : Type u_1} → (ι → Type u_2) → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} {f_1 g : D₁ ⟶ D₂}, (∀ (i : ι), f_1.hom i = g.hom i) → f_1 = g
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.eigenvalues.congr_simp : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T T_1 : E →ₗ[𝕜] E} (e_T : T = T_1) [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n) (a a_1 : Fin n), a = a_1 → hT.eigenvalues hn a = ⋯.eigenvalues hn a_1
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.sdiff_cylinder_same : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S T : Set ((i : ↥s) → α ↑i)),
  MeasureTheory.cylinder s S \ MeasureTheory.cylinder s T = MeasureTheory.cylinder s (S \ T)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_of_eq' : ∀ {a x p : ℤ}, a * x + p = 0 → a ∣ p
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic_apply_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)),
  ↑(stereographic ⋯) (-v) = 0
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.lt_iff_exists_eq_append : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String},
  p₁.Splits t₁ t₂ → p₂.Splits t₃ t₄ → (p₁ < p₂ ↔ ∃ t₅, t₅ ≠ "" ∧ t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄)
-- Mathlib.GroupTheory.Perm.List
List.mem_of_formPerm_apply_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {x : α}, l.formPerm x ∈ l → x ∈ l
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_Icc : ∀ {f : ℝ → ℝ} {y z : ℝ},
  ConvexOn ℝ (Set.Icc y z) f →
    y < z → ContinuousWithinAt f (Set.Ici y) y → ContinuousWithinAt f (Set.Iic z) z → ContinuousOn f (Set.Icc y z)
-- Mathlib.Data.List.MinMax
List.coe_le_maximum_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a : α}, ↑a ≤ l.maximum ↔ ∃ b ∈ l, a ≤ b
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_equivMapOfInjective_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring R) (f : R →+* S)
  (hf : Function.Injective ⇑f) (x : ↥s), ↑((s.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_left_eq_Ioc_sub_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α} [NoMinOrder α], a ≤ b → insert a (Finset.Ioc a b) = Finset.Ioc (a - 1) b
-- Mathlib.LinearAlgebra.Matrix.Permutation
Matrix.permMatrixHom_apply : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : NonAssocSemiring R]
  (σ : Equiv.Perm n), Matrix.permMatrixHom σ = Equiv.Perm.permMatrix R σ⁻¹
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isLittleO_congr_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} {k' : α → G'} {l : Filter α},
  g' =Θ[l] k' → (f =o[l] g' ↔ f =o[l] k')
-- Mathlib.LinearAlgebra.Dimension.Subsingleton
rank_bot : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Module.rank R ↥⊥ = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add.eq_1 : ∀ {α : Type u_2} [inst : Add α], Set.add = { add := Set.image2 fun x1 x2 => x1 + x2 }
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function which is continuous on a compact set `s` is almost everywhere strongly measurable
with respect to `μ.restrict s`.  -/
ContinuousOn.aestronglyMeasurable_of_isCompact : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_2 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {s : Set α}
  {μ : MeasureTheory.Measure α},
  ContinuousOn f s → IsCompact s → MeasurableSet s → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.instInhabitedOfDecidableEq : (R : Type u_1) → [inst : NonUnitalRing R] → [DecidableEq R] → Inhabited (RingNorm R)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ico_add_one_left_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α}, a < b → insert a (Finset.Ico (a + 1) b) = Finset.Ico a b
-- Init.Grind.Offset
Lean.Grind.Nat.le_of_eq_2 : ∀ (u v : ℕ), u = v → v ≤ u
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.instCreatesColimitLocallyRingedSpaceForgetToLocallyRingedSpace : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [Quiver.IsThin J] →
            [Small.{u, w} J] → CategoryTheory.CreatesColimit F AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Init.Data.Fin.Lemmas
Fin.natAdd_mk : ∀ {m : ℕ} (n i : ℕ) (hi : i < m), Fin.natAdd n ⟨i, hi⟩ = ⟨n + i, ⋯⟩
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.nonempty : ∀ {α : Type u} {s : Set α}, s.Nontrivial → s.Nonempty
-- Mathlib.Order.Basic
Pi.instSDiff.eq_1 : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → SDiff (π i)], Pi.instSDiff = { sdiff := fun x y i => x i \ y i }
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_inclusion : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) (a : ↥H), ↑((AddSubgroup.inclusion h) a) = ↑a
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The norm on a `NormedField`, as a `MulRingNorm`.  -/
NormedField.toMulRingNorm : (R : Type u_2) → [inst : NormedField R] → MulRingNorm R
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.add_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (x y z : M), (B x) (y + z) = (B x) y + (B x) z
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_neg_add_nhds_zero_swapped : ∀ (Gₗ : Type u_2) [inst : UniformSpace Gₗ] [inst_1 : AddGroup Gₗ] [IsLeftUniformAddGroup Gₗ],
  uniformity Gₗ = Filter.comap (fun x => -x.2 + x.1) (nhds 0)
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.isGaussian_of_map_eq_gaussianReal : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] {mE : MeasurableSpace E}
  [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E},
  (∀ (L : E →L[ℝ] ℝ), ∃ m v, MeasureTheory.Measure.map (⇑L) μ = ProbabilityTheory.gaussianReal m v) →
    ProbabilityTheory.IsGaussian μ
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- If the sum of points of a cone is in a face, then all the points are in the face.  -/
PointedCone.IsFaceOf.mem_of_sum_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} {ι : Type u_4} [inst_5 : Fintype ι]
  {f : ι → M}, F.IsFaceOf C → (∀ (i : ι), f i ∈ C) → ∑ i, f i ∈ F → ∀ (i : ι), f i ∈ F
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f}
  (hf : CategoryTheory.Limits.IsColimit cc) (cc' : CategoryTheory.Limits.CokernelCofork f')
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C} (h : cc'.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc') h)
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- **Bernoulli's inequality** for real exponents, strict version: for `1 < p` and `-1 ≤ s`, with
`s ≠ 0`, we have `1 + p * s < (1 + s) ^ p`.  -/
one_add_mul_self_lt_rpow_one_add : ∀ {s : ℝ}, -1 ≤ s → s ≠ 0 → ∀ {p : ℝ}, 1 < p → 1 + p * s < (1 + s) ^ p
-- Mathlib.Algebra.Order.Ring.Idempotent
instPartialOrderSubtypeProdAndEqHMulFstSndOfNatHAdd : {R : Type u_1} → [inst : CommSemiring R] → PartialOrder { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
-- Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
TopCat.instIsIsoSingularHomology₀εOfPathConnectedSpaceCarrier : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C)
  [PathConnectedSpace ↑X], CategoryTheory.IsIso (X.singularHomology₀ε R)
-- Mathlib.Data.Multiset.Sym
/-- **Alias** of `Multiset.setOfPred_mem_sym2`. -/
Multiset.setOf_mem_sym2 : ∀ {α : Type u_1} {m : Multiset α}, {z | z ∈ m.sym2} = {x | x ∈ m}.sym2
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.mem_smul_pointwise_iff_exists : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (m : M) (a : α)
  (S : Submodule R M), m ∈ a • S ↔ ∃ b ∈ S, a • b = m
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.selfProdProj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {X A : C} (u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X)
  (x : (F.obj X).obj),
  CategoryTheory.PreGaloisCategory.selfProdProj✝ u x =
    CategoryTheory.CategoryStruct.comp u (CategoryTheory.Limits.Pi.π (fun x => X) x)
-- Std.Time.Format.Modifier
Std.Time.instReprOffsetX.repr : Std.Time.OffsetX → ℕ → Std.Format
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ico_succ_right_eq_Icc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ico a (Order.succ b) = Set.Icc a b
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Given a continuous linear map `f : M → N`, `mapRangeₗ` is the linear map mapping the
vector measure `v` on `M` to the vector measure `f ∘ v` on `N`.  -/
MeasureTheory.VectorMeasure.mapRangeₗ : {M : Type u_3} →
  [inst : AddCommMonoid M] →
    [inst_1 : TopologicalSpace M] →
      {N : Type u_4} →
        [inst_2 : AddCommMonoid N] →
          [inst_3 : TopologicalSpace N] →
            {R : Type u_5} →
              [inst_4 : Semiring R] →
                [inst_5 : Module R M] →
                  [inst_6 : Module R N] →
                    [inst_7 : ContinuousConstSMul R M] →
                      [inst_8 : ContinuousConstSMul R N] →
                        [inst_9 : ContinuousAdd M] →
                          [inst_10 : ContinuousAdd N] →
                            {α : Type u_6} →
                              [inst_11 : MeasurableSpace α] →
                                (f : M →ₗ[R] N) →
                                  Continuous ⇑f → MeasureTheory.VectorMeasure α M →ₗ[R] MeasureTheory.VectorMeasure α N
-- Mathlib.Algebra.CharZero.Quotient
AddSubgroup.nsmul_mem_zmultiples_iff_exists_sub_div : ∀ {R : Type u_1} [inst : DivisionRing R] [CharZero R] {p r : R} {n : ℕ},
  n ≠ 0 → (n • r ∈ AddSubgroup.zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ AddSubgroup.zmultiples p)
-- Init.Data.Float.Float32
/-- Computes the tangent of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`tanf`.
 -/
Float32.tan : Float32 → Float32
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem : Type
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The bijection `(X ⟶ Y) ≃ (X.val ⟶ Y.val)` when `X` and `Y` are sheaves.  -/
CategoryTheory.Sheaf.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] → {X Y : CategoryTheory.Sheaf J A} → (X ⟶ Y) ≃ (X.obj ⟶ Y.obj)
-- Mathlib.Order.Interval.Finset.Defs
/-- A constructor from a definition of `Finset.Ici` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderTop.ofIci`, this one requires `DecidableLE` but
only `Preorder`.  -/
LocallyFiniteOrderTop.ofIci' : (α : Type u_1) →
  [inst : Preorder α] →
    [DecidableLE α] → (finsetIci : α → Finset α) → (∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x) → LocallyFiniteOrderTop α