mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.mk.injEq : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)] [inst_7 : FiberBundle F E]
  [inst_8 : VectorBundle ℝ F E] (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ)
  (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v)
  (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1})
  (continuous : Continuous fun b => ⟨b, inner b⟩) (inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ)
  (symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v)
  (pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v)
  (isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1})
  (continuous_1 : Continuous fun b => ⟨b, inner_1 b⟩),
  ({ inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, continuous := continuous } =
      { inner := inner_1, symm := symm_1, pos := pos_1, isVonNBounded := isVonNBounded_1,
        continuous := continuous_1 }) =
    (inner = inner_1)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.mul : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {w x y z : R}, c w x → c y z → c (w * y) (x * z)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- There is a unique additive monoid homomorphism between two additive monoids with
a unique element.  -/
AddEquiv.instUnique : {M : Type u_16} → {N : Type u_17} → [Unique M] → [Unique N] → [inst : Add M] → [inst_1 : Add N] → Unique (M ≃+ N)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictMonoOn.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α} {s : Set β}, StrictMonoOn f s → StrictAntiOn (fun x => (f x)⁻¹) s
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.whiskerLeft_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B),
  (CategoryTheory.Lax.LaxTrans.whiskerLeft η Γ).as.app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → ∀ (a : α), t.get? a = t_1.get? a
-- Mathlib.Data.Set.Card
Set.two_lt_ncard_iff : ∀ {α : Type u_1} {s : Set α},
  autoParam s.Finite Set.two_lt_ncard_iff._auto_1 →
    (2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The bottom left map in the reverse hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ C
-- Lean.Elab.SyntheticMVars
/-- Try to solve postponed universe constraints, and throws an exception if there are stuck constraints.

Remark: in previous versions, each `isDefEq u v` invocation would fail if there
were pending universe level constraints. With this old approach, we were not able
to process
```
Functor.map Prod.fst (x s)
```
because after elaborating `Prod.fst` and trying to ensure its type
match the expected one, we would be stuck at the universe constraint:
```
u =?= max u ?v
```
Another benefit of using `withoutPostponingUniverseConstraints` is better error messages. Instead
of getting a mysterious type mismatch constraint, we get a list of
universe constraints the system is stuck at.
 -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.processPostponedUniverseConstraints : Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
/-- A simplicial set is nonempty when the type of `0`-simplices is nonempty.  -/
SSet.Nonempty : SSet → Prop
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.iSup : ∀ {G : Type u_3} [inst : Group G] {ι : Sort u_5} [Finite ι] (P : ι → Subgroup G), (∀ (i : ι), (P i).FG) → (iSup P).FG
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.MagmaCat.Hom.mk.sizeOf_spec : ∀ {A B : MagmaCat} (hom' : ↑A →ₙ* ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₈_det : CartanMatrix.E₈.det = 1
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesSummable.of_re_le_re : ∀ {f : ℕ → ℂ} {s s' : ℂ}, s.re ≤ s'.re → LSeriesSummable f s → LSeriesSummable f s'