mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.injective_of_comp_eq_id : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ →ₛₗ[σ'] M),
  g ∘ₛₗ f = LinearMap.id → Function.Injective ⇑f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.singleton_eq_insert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {p : (a : α) × β a}, {p} = ∅.insert p.fst p.snd
-- Mathlib.Order.WithBot
WithTop.instWellFoundedGT : ∀ {α : Type u_1} [inst : LT α] [WellFoundedGT α], WellFoundedGT (WithTop α)
-- Mathlib.Algebra.Group.AddChar
AddChar.pow_apply : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ : AddChar A M) (n : ℕ) (a : A),
  (ψ ^ n) a = ψ a ^ n
-- Mathlib.Topology.Bases
IsTopologicalBasis.iInf : ∀ {β : Type u_1} {ι : Type u_2} {t : ι → TopologicalSpace β} {T : ι → Set (Set β)},
  (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) →
    TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_ofReal_im : ∀ (x : ℂ) (y : ℝ), (x ^ ↑y).im = ‖x‖ ^ y * Real.sin (x.arg * y)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.subtypeVal_submodule_convexCombPair : ∀ {F : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : SetLike F M]
  [inst_6 : AddSubmonoidClass F M] [inst_7 : SMulMemClass F R M] [inst_8 : Convexity.ConvexSpace R M]
  [inst_9 : Convexity.IsModuleConvexSpace R M] (S : F) (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : ↥S),
  ↑(Convexity.convexCombPair a b ha hb hab x y) = Convexity.convexCombPair a b ha hb hab ↑x ↑y
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Isomorphic pre-`1`-hypercovers have equivalent multifork index categories.  -/
CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E F : CategoryTheory.PreOneHypercover S} →
        (E ≅ F) →
          (CategoryTheory.Limits.WalkingMulticospan E.multicospanShape ≌
            CategoryTheory.Limits.WalkingMulticospan F.multicospanShape)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {h : k ∈ Std.HashMap.filterMap f m},
  (Std.HashMap.filterMap f m)[k] = (f (m.getKey k ⋯) m[k]).get ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BiconeMorphism.wι : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) self.hom = B.ι j
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coe_sub`. -/
MeasureTheory.VectorMeasure.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- Note that `QuadraticMap.Isometry.id` would not be well-typed as the RHS.  -/
QuadraticMap.Isometry.proj_comp_single_of_same : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (i : ι) (Q : QuadraticMap R (Mᵢ i) P),
  (QuadraticMap.Isometry.proj i Q).comp (QuadraticMap.Isometry.single (Pi.single i Q) i) = QuadraticMap.Isometry.ofEq ⋯
-- Init.Data.UInt.Basic
instMinUInt64 : Min UInt64
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.one_def : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] [inst_3 : One X], 1 = 1 /ₒ 1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a normed vector space, the addition of a measurable function and a strongly measurable
function is measurable. Note that this is not true without further second-countability assumptions
for the addition of two measurable functions.  -/
Measurable.add_stronglyMeasurable : ∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddCancelMonoid E] [inst_1 : TopologicalSpace E]
  [inst_2 : MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [TopologicalSpace.PseudoMetrizableSpace E]
  {g f : α → E}, Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (g + f)
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve integer power.

See note [hom simp lemma priority]  -/
map_zpow : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
  [MonoidHomClass F G H] (f : F) (g : G) (n : ℤ), f (g ^ n) = f g ^ n
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.liftAt : ∀ {L : FirstOrder.Language} {α : Type u'} {l : ℕ} {φ : L.BoundedFormula α l} {k m : ℕ},
  φ.IsPrenex → (FirstOrder.Language.BoundedFormula.liftAt k m φ).IsPrenex
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instQuasiIsoIntιTruncLEOfIsLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsLE n], QuasiIso (K.ιTruncLE n)
-- Mathlib.Topology.Bornology.Basic
Bornology.mk : {α : Type u_4} → (cobounded : Filter α) → cobounded ≤ Filter.cofinite → Bornology α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Batteries.Logic
cast_eq_iff_heq : ∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' ↔ a_2 ≍ a'
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → γ},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x, g x)) μ
-- Mathlib.Order.Category.Preord
/-- Construct a bundled `Preord` from the underlying type and typeclass.  -/
Preord.of : (carrier : Type u_1) → [str : Preorder carrier] → Preord
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.below : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    {J : CategoryTheory.Precoverage C} →
      {motive : (X : C) → (a : CategoryTheory.Sieve X) → J.Saturate X a → Prop} →
        {X : C} → {a : CategoryTheory.Sieve X} → J.Saturate X a → Prop
-- Mathlib.Order.Filter.Map
Filter.map_neBot : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} [hf : f.NeBot], (Filter.map m f).NeBot
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Homeomorph.toMeasurableEquiv_symm_coe : ∀ {γ : Type u_3} {γ₂ : Type u_4} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
  [inst_3 : TopologicalSpace γ₂] [inst_4 : MeasurableSpace γ₂] [inst_5 : BorelSpace γ₂] (h : γ ≃ₜ γ₂),
  ⇑h.toMeasurableEquiv.symm = ⇑h.symm
-- Mathlib.SetTheory.Ordinal.Univ
/-- The cardinal `univ.{u, v}` is the cardinality of `Ordinal.{u}` or `Cardinal.{u}`, as an element
of `Cardinal.{v}` (when `u < v`).  -/
Cardinal.univ : Cardinal.{max (u + 1) v}
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The forgetful functor from commutative group objects to group objects.  -/
CategoryTheory.CommGrp.forget₂Grp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommGrp C) (CategoryTheory.Grp C)
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_zero_left : ∀ {α : Type u_1} (s : Multiset α), Multiset.powersetCard 0 s = {0}
-- Init.Notation
Lean.rawStx.quot : Lean.ParserDescr
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iSup_of_le : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l} {α : Type u_1} {Ψ : α → l} (a : α),
  Lean.Order.PartialOrder.rel P (Ψ a) → Lean.Order.PartialOrder.rel P (Lean.Order.iSup Ψ)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_mul_aleph0_eq : ∀ {α : Type u_1} [Infinite α], Cardinal.mk α * Cardinal.aleph0 = Cardinal.mk α
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatParam : Std.ToFormat Lean.IR.Param
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress_of_disjoint_of_le : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {u v a : α}, Disjoint u a → v ≤ a → UV.compress u v a = (a ⊔ u) \ v
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_mono : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {f g : C(↑(spectrum R a), R)}, f ≤ g → (cfcHom ha) f ≤ (cfcHom ha) g
-- Batteries.Data.String.Lemmas
String.toRawSubstring.eq_1 : ∀ (s : String), s.toRawSubstring = { str := s, startPos := { }, stopPos := s.rawEndPos }
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isUniformEmbedding : ∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → UniformContinuous f → IsUniformEmbedding f
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The map `fun t ↦ exp (t * I)` from `ℝ` to the unit circle in `ℂ` is analytic.  -/
contMDiff_circleExp : ∀ {m : WithTop ℕ∞},
  ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) m ⇑Circle.exp
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.unitsFstOne_val_inv_val_fst : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : ↥(Unitization.unitsFstOne R A)),
  (↑(↑x)⁻¹).toProd.1 = 1
-- Mathlib.Data.Finsupp.Defs
Finsupp.mk.injEq : ∀ {α : Type u_9} {M : Type u_10} [inst : Zero M] (support : Finset α) (toFun : α → M)
  (mem_support_toFun : ∀ (a : α), a ∈ support ↔ toFun a ≠ 0) (support_1 : Finset α) (toFun_1 : α → M)
  (mem_support_toFun_1 : ∀ (a : α), a ∈ support_1 ↔ toFun_1 a ≠ 0),
  ({ support := support, toFun := toFun, mem_support_toFun := mem_support_toFun } =
      { support := support_1, toFun := toFun_1, mem_support_toFun := mem_support_toFun_1 }) =
    (support = support_1 ∧ toFun = toFun_1)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the numerator of a right fraction  -/
CategoryTheory.MorphismProperty.RightFraction.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.RightFraction X Y) → self.X' ⟶ Y
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- Rescale a multivariate power series, as an `AlgHom` in the scaling parameters,
by multiplying each variable `x` by the value `a x`.  -/
MvPowerSeries.rescaleAlgHom : {σ : Type u_1} → {R : Type u_3} → [inst : CommRing R] → (σ → R) → MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.extendId`.

---

Extending a cone by the identity does nothing.  -/
CategoryTheory.Limits.Cones.extendId : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) → s.extend (CategoryTheory.CategoryStruct.id s.pt) ≅ s
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.eq_5 : ∀ (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingReflexivePair) → motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
  (h_4 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
  (h_5 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion)
  (h_6 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion),
  (match CategoryTheory.Limits.WalkingReflexivePair.one, CategoryTheory.Limits.WalkingReflexivePair.one,
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion with
    | x, .(x), CategoryTheory.Limits.WalkingReflexivePair.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right => h_3 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.zero), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion => h_4 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion => h_5 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion => h_6 ()) =
    h_5 ()
-- Mathlib.Algebra.Order.Module.Defs
instPosSMulStrictMonoNatOfIsOrderedAddMonoid : ∀ {M : Type u_3} [inst : PartialOrder M] [inst_1 : AddCancelCommMonoid M] [IsOrderedAddMonoid M], PosSMulStrictMono ℕ M
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.eq_2 : ∀ {α : Type u_1} (sep x_1 : List α), sep.intercalateTR [x_1] = x_1
-- Qq.AssertInstancesCommute
Qq.Impl.termAssertInstancesCommuteImpl_ : Lean.ParserDescr
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.ruleTac.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.RuleTacDescr.ruleTac decl = Aesop.RuleTacDescr.ruleTac decl_1) = (decl = decl_1)
-- Mathlib.Data.List.Sym
List.mem_sym2_iff : ∀ {α : Type u_1} {xs : List α} {z : Sym2 α}, z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.num.eq_1 : ∀ (g : GL (Fin 2) ℝ) (z : ℂ), UpperHalfPlane.num g z = ↑(↑g 0 0) * z + ↑(↑g 0 1)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_two : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ Y₂ : C₂} {X₃ : C₃}
  (f₂ : X₂ ⟶ Y₂) (g : Y₂ ⟶ (G.obj (Opposite.op X₁)).obj X₃),
  adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp f₂ g) =
    CategoryTheory.CategoryStruct.comp ((F.obj X₁).map f₂) (adj₂.homEquiv.symm g)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toArray_eq_empty_iff : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], r.toArray = #[] ↔ ¬r.lower ≤ r.upper
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ι_l_assoc : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d) {Z : SSet}
  (h : SSet.relativeCellComplexOfMono.sigmaStdSimplex i d ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.l i d) h) =
    CategoryTheory.CategoryStruct.comp (SSet.boundary d).ι (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f' (CategoryTheory.Limits.pushout.inl f g))
      (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').hom =
    CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.equalizerSieve_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ}
  (x y : CategoryTheory.ToType (F.obj X)) (x_1 : C) (f : x_1 ⟶ Opposite.unop X),
  (CategoryTheory.Presheaf.equalizerSieve x y).arrows f =
    ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) y)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfSquareZero.dividedPowers.eq_1 : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] (hI2 : I ^ 2 = 0),
  DividedPowers.OfSquareZero.dividedPowers hI2 = DividedPowers.OfInvertibleFactorial.dividedPowers ⋯ hI2
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.measurable_cauchyPDFReal : ∀ (x₀ : ℝ) (γ : NNReal), Measurable (ProbabilityTheory.cauchyPDFReal x₀ γ)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.change : Lean.Lsp.TextDocumentSyncOptions → Lean.Lsp.TextDocumentSyncKind
-- Plausible.Testable
/-- Enable tracing of values that didn't fulfill preconditions and were thus discarded.
 -/
Plausible.Configuration.traceDiscarded : Plausible.Configuration → Bool
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.not_isClique_iff : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, ¬G.IsClique s ↔ ∃ v w, v ≠ w ∧ ¬G.Adj ↑v ↑w
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformlyOn_iff_tendstoUniformlyOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι}, TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (Filter.principal s)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_set_coe : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} (s : Set ι) [inst_1 : Fintype ↑s],
  ∏ i, f ↑i = ∏ i ∈ s.toFinset, f i
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Simp lemmas for rewriting a hom in monoidal categories into a normal form.
 -/
Mathlib.Tactic.Coherence.monoidal_simps : Lean.ParserDescr
-- Mathlib.Order.Bounds.Basic
upperBounds_mono_of_isCofinalFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsCofinalFor s t → upperBounds t ⊆ upperBounds s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_emptyWithCapacity : ∀ {α : Type u} [BEq α] [Hashable α] {c : ℕ}, (Std.HashSet.Raw.emptyWithCapacity c).isEmpty = true
-- Init.Data.SInt.Lemmas
ISize.toFin_toBitVec : ∀ (x : ISize), x.toBitVec.toFin = x.toUSize.toFin
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.isometry_realToRCLike : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] [inst_2 : CompactSpace X],
  Isometry (ContinuousMap.realToRCLike 𝕜)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.labelledCopyCount.eq_1 : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] [inst_1 : Fintype W] (G : SimpleGraph V) (H : SimpleGraph W),
  G.labelledCopyCount H = Fintype.card (H.Copy G)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSets.condIndepSets : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)},
  ProbabilityTheory.iCondIndepSets m' hm' s μ →
    ∀ {i j : ι}, i ≠ j → ProbabilityTheory.CondIndepSets m' hm' (s i) (s j) μ
-- Mathlib.Algebra.Group.Support
Function.mulSupport_fun_inv : ∀ {α : Type u_1} {G : Type u_3} [inst : DivisionMonoid G] (f : α → G),
  (Function.mulSupport fun x => (f x)⁻¹) = Function.mulSupport f
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Weaken the conditions on all components.  -/
CategoryTheory.MorphismProperty.Comma.changeProp : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                {P P' : CategoryTheory.MorphismProperty T} →
                  {Q Q' : CategoryTheory.MorphismProperty A} →
                    {W W' : CategoryTheory.MorphismProperty B} →
                      P ≤ P' →
                        Q ≤ Q' →
                          W ≤ W' →
                            [inst_3 : Q.IsMultiplicative] →
                              [inst_4 : Q'.IsMultiplicative] →
                                [inst_5 : W.IsMultiplicative] →
                                  [inst_6 : W'.IsMultiplicative] →
                                    CategoryTheory.Functor (CategoryTheory.MorphismProperty.Comma L R P Q W)
                                      (CategoryTheory.MorphismProperty.Comma L R P' Q' W')
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.withReader : ∀ {m n : Type u → Type v} {ρ α : Type u} [inst : MonadFunctor m n] [inst_1 : MonadWithReaderOf ρ m] (f : ρ → ρ),
  MonadWithReaderOf.withReader f = monadMap fun {β} => MonadWithReaderOf.withReader f
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.nestedPR.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.nestedPR = 1
-- Std.Data.HashSet.Lemmas
Std.HashSet.forM_eq_forM : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {m' : Type v → Type w} [inst : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{v + 1}}, Std.HashSet.forM f m = forM m f