mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Antitone.mul_const : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [MulPosMono M₀], Antitone f → 0 ≤ a → Antitone fun x => f x * a
-- Init.Data.Iterators.Consumers.Loop
/-- Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.fold`.
 -/
Std.Iter.Total.fold : {α β : Type w} →
  {γ : Type x} →
    [inst : Std.Iterator α Id β] →
      [Std.IteratorLoop α Id Id] → [Std.Iterators.Finite α Id] → (γ → β → γ) → γ → Std.Iter.Total β → γ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul_smul : ∀ {α : Type u_1} {F : Type u_4} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0}
  [inst_3 : NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) (x : F),
  MeasureTheory.condExpIndSMul hm hs hμs (c • x) = c • MeasureTheory.condExpIndSMul hm hs hμs x
-- Mathlib.Data.List.Sigma
List.dedupKeys_cons : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {x : Sigma β} (l : List (Sigma β)),
  (x :: l).dedupKeys = List.kinsert x.fst x.snd l.dedupKeys
-- Init.Omega.IntList
Lean.Omega.IntList.dvd_bmod_dot_sub_dot_bmod : ∀ (m : ℕ) (xs ys : Lean.Omega.IntList), ↑m ∣ Lean.Omega.IntList.bmod_dot_sub_dot_bmod m xs ys
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.inr__obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : D), (CategoryTheory.Sum.inr_ C D).obj X = Sum.inr X
-- Mathlib.RepresentationTheory.Equiv
/-- Equiv between representations induced by linear equiv between `(α →₀ V) ⊗[k] W` and
`α →₀ (V ⊗[k] W)`.  -/
Representation.finsuppTensorLeft : {G : Type v} →
  [inst : Monoid G] →
    {V : Type v'} →
      [inst_1 : AddCommMonoid V] →
        {W : Type w'} →
          [inst_2 : AddCommMonoid W] →
            {k : Type u} →
              [inst_3 : CommSemiring k] →
                [inst_4 : Module k V] →
                  [inst_5 : Module k W] →
                    (σ : Representation k G V) →
                      (ρ : Representation k G W) →
                        (α : Type w') → [DecidableEq α] → ((σ.finsupp α).tprod ρ).Equiv ((σ.tprod ρ).finsupp α)
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.mk.injEq : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (toAddSubgroup : AddSubgroup G)
  (isClosed' : IsClosed toAddSubgroup.carrier) (toAddSubgroup_1 : AddSubgroup G)
  (isClosed'_1 : IsClosed toAddSubgroup_1.carrier),
  ({ toAddSubgroup := toAddSubgroup, isClosed' := isClosed' } =
      { toAddSubgroup := toAddSubgroup_1, isClosed' := isClosed'_1 }) =
    (toAddSubgroup = toAddSubgroup_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.instIsMonHomSnd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N]
  [inst_4 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsMonHom (CategoryTheory.SemiCartesianMonoidalCategory.snd M N)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} {f g : R₁ ⟶ R₂},
  f = g ↔ f.hom = g.hom
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- The yoneda version of the sheaf condition is equivalent to the sheaf condition.

C2.1.4 of [Elephant].
 -/
CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ CategoryTheory.Presieve.YonedaSheafCondition P S
-- Mathlib.Data.ENat.Basic
ENat.le_sub_of_add_le_left : ∀ {a b c : ℕ∞}, a ≠ ⊤ → a + b ≤ c → b ≤ c - a
-- Mathlib.Order.Category.Lat
/-- Turn a morphism in `Lat` back into a `LatticeHom`.  -/
Lat.Hom.hom : {X Y : Lat} → X.Hom Y → LatticeHom ↑X ↑Y
-- Mathlib.Data.List.Sort
List.sortedLT_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedLT ↔ l.SortedGT
-- Std.Async.UDP
_private.Std.Async.UDP.0.Std.Async.UDP.Socket.ofNative.inj : ∀ {native native_1 : Std.Internal.UV.UDP.Socket}, { native := native } = { native := native_1 } → native = native_1
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_mono : Monotone ENat.floor
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBaseNat.sum.sizeOf_spec : ∀ {e : Q(ℕ)} (x : Mathlib.Tactic.Ring.Common.ExSumNat e),
  sizeOf (Mathlib.Tactic.Ring.Common.ExBaseNat.sum x) = 1 + sizeOf e + sizeOf x
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The free-forgetful adjunction for groups.
 -/
GrpCat.adj : GrpCat.free ⊣ CategoryTheory.forget GrpCat
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteAddMonoidOfIsAddCommutative : ∀ (M : Type u_2) [inst : AddZero M] [IsAddCommutative M], IsDedekindFiniteAddMonoid M
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- Auxiliary definition for `desc`.  -/
SSet.horn₃₁.desc.multicofork : {X : SSet} →
  (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X) →
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃ →
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
          CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂ →
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
            CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃ →
          CategoryTheory.Limits.Multicofork
            ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map SSet.Subcomplex.toSSetFunctor)
-- Mathlib.Algebra.Order.Group.Equiv
coe_ofLexMulEquiv : ∀ (α : Type u_1) [inst : Mul α], ⇑(ofLexMulEquiv α) = ⇑ofLex
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- The hard part of the trapezoidal rule error bound: proving it in the case of a non-empty closed
interval with ordered endpoints. This lemma is used in the proof of the general error bound later
on.  -/
_private.Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule.0.trapezoidal_error_le_of_lt : ∀ {f : ℝ → ℝ} {ζ a b : ℝ},
  a < b →
    DifferentiableOn ℝ f (Set.Icc a b) →
      DifferentiableOn ℝ (derivWithin f (Set.Icc a b)) (Set.Icc a b) →
        (∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ) →
          ∀ {N : ℕ}, 0 < N → |trapezoidal_error f N a b| ≤ (b - a) ^ 3 * ζ / (12 * ↑N ^ 2)
-- Mathlib.Algebra.Star.Prod
Prod.instStarRing : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] → [StarRing R] → [StarRing S] → StarRing (R × S)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₁.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j =
    HomologicalComplex.mapBifunctor₂₃.d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j
-- Init.Data.SInt.Bitwise
instIdempotentOpISizeHOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstArrayRef.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.UInt.BasicAux
UInt32.ofNat.eq_1 : ∀ (n : ℕ), UInt32.ofNat n = { toBitVec := BitVec.ofNat 32 n }
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- This is an intermediate result; use the more general `CFC.monotone_nnrpow` instead.  -/
_private.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order.0.CFC.monotoneOn_nnrpow_Ioo : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : NNReal},
  p ∈ Set.Ioo 0 1 → MonotoneOn (fun a => a ^ p) (Set.Ici 0)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instOrdSpan : Ord Std.Time.Nanosecond.Span
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeleton_top`. -/
Topology.CWComplex.skeleton_top : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ↑(Topology.RelCWComplex.skeleton C ⊤) = C
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.homeomorph_mk_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (a : X ≃ Y)
  (b : Continuous a.toFun) (c : Continuous a.invFun),
  ⇑{ toEquiv := a, continuous_toFun := b, continuous_invFun := c } = ⇑a
-- Init.Data.Option.Lemmas
Option.min_pfilter_right : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {o : Option α} {p : (a : α) → o = some a → Bool},
  o ⊓ o.pfilter p = o.pfilter p
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldRev.eq_1 : ∀ {α : Type u} (x : α) (f : (i : ℕ) → i < 0 → α → α), Nat.foldRev 0 f x = x
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.det_coe : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R), (↑A).det = 1
-- Mathlib.Condensed.Epi
Condensed.epi_iff_surjective_on_stonean : ∀ (A : Type u') [inst : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type v'}
  [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] {X Y : Condensed A} (f : X ⟶ Y)
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)]
  [∀ (X : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A]
  [(CategoryTheory.extensiveTopology Stonean).WEqualsLocallyBijective A]
  [CategoryTheory.HasSheafify (CategoryTheory.extensiveTopology Stonean) A]
  [(CategoryTheory.extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)]
  [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology Stonean) A)],
  CategoryTheory.Epi f ↔
    ∀ (S : Stonean), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S.compHaus)))
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) {X : C}
  (f : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P),
  CategoryTheory.uliftYonedaEquiv
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom φ P)) =
    (CategoryTheory.ConcreteCategory.hom ((G.map f).app (Opposite.op (F.obj X))))
      ((CategoryTheory.ConcreteCategory.hom ((φ.app X).app (Opposite.op (F.obj X))))
        { down := CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X))) })
-- Mathlib.Analysis.InnerProductSpace.PiL2
Module.finrank.hcongr_5 : ∀ (R R' : Type u_1),
  R = R' →
    ∀ (M M' : Type u_2),
      M = M' →
        ∀ (inst : Semiring R) (inst' : Semiring R'),
          inst ≍ inst' →
            ∀ (inst_1 : AddCommMonoid M) (inst'_1 : AddCommMonoid M'),
              inst_1 ≍ inst'_1 →
                ∀ (inst_2 : Module R M) (inst'_2 : Module R' M'),
                  inst_2 ≍ inst'_2 → Module.finrank R M ≍ Module.finrank R' M'
-- Init.Data.List.Sublist
List.suffix_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, l <:+ List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
-- Mathlib.FieldTheory.IsAlgClosed.Classification
IsAlgClosed.isAlgClosure_of_transcendence_basis : ∀ {R : Type u_1} {K : Type u_3} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] {ι : Type u_4} (v : ι → K)
  [IsAlgClosed K], IsTranscendenceBasis R v → IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleHover : Lean.Lsp.HoverParams → Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.Hover))
-- Mathlib.Topology.Order
IndiscreteTopology.eq_top : ∀ (α : Type u_2) {inst : TopologicalSpace α} [self : IndiscreteTopology α], inst = ⊤
-- Init.Data.BitVec.Lemmas
BitVec.getElem_cast : ∀ {w v i : ℕ} (h : w = v) (x : BitVec w) (p : i < v), (BitVec.cast h x)[i] = x[i]
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), edist a b < δ → edist (f a) (f b) < ε
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char.congr_simp : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e e_1 : AddChar ℝ Circle}
  (e_e : e = e_1) {L L_1 : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (e_L : L = L_1) (he : Continuous ⇑e)
  (hL : Continuous fun p => (L p.1) p.2) (w w_1 : W),
  w = w_1 → BoundedContinuousFunction.char he hL w = BoundedContinuousFunction.char ⋯ ⋯ w_1
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.mk.injEq : ∀ {C : Type u₁} (ι : Type) [fintype : Fintype ι] (X : ι → C) (ι_1 : Type) (fintype_1 : Fintype ι_1) (X_1 : ι_1 → C),
  ({ ι := ι, fintype := fintype, X := X } = { ι := ι_1, fintype := fintype_1, X := X_1 }) =
    (ι = ι_1 ∧ fintype ≍ fintype_1 ∧ X ≍ X_1)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getD_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  (cs.leftInvSeq ω).getD j 1 =
    cs.wordProd (List.take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (List.take j ω))⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.fac_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {f : F ⟶ G} {X : C}
  (H : CategoryTheory.Limits.MonoFactorisation f) (x : F.obj X),
  (CategoryTheory.ConcreteCategory.hom (H.m.app X)) ((CategoryTheory.ConcreteCategory.hom (H.e.app X)) x) =
    (CategoryTheory.ConcreteCategory.hom (f.app X)) x
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.isValue.sizeOf_spec : ∀ (bvarIdx : ℕ) (strict : Bool),
  sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.isValue bvarIdx strict) = 1 + sizeOf bvarIdx + sizeOf strict
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] (c : β), MeasureTheory.Integrable (fun x => c) μ
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sInf_eq : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α] {s : Set (WithBot α)},
  ⊥ ∉ s → BddBelow (WithBot.some ⁻¹' s) → sInf s = ↑(sInf (WithBot.some ⁻¹' s))
-- Mathlib.Probability.CDF
ProbabilityTheory.unitInterval.cdf_eq_real : ∀ (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] (x : ↑unitInterval),
  ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map Subtype.val μ)) ↑x = μ.real (Set.Icc 0 x)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  m.WF → ((Std.DHashMap.Raw.filter (fun a x => f a) m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = false)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (e : R ≃+* S) (x : R), e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- This is used as the ext lemma instead of `AffineMap.pi_ext_nonempty` for reasons explained in
note [partially-applied ext lemmas]. Analogous to `LinearMap.pi_ext'`  -/
AffineMap.pi_ext_nonempty' : ∀ {k : Type u_2} {V2 : Type u_5} {P2 : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V2] [inst_2 : AddTorsor V2 P2]
  [inst_3 : Module k V2] {ι : Type u_9} {φv : ι → Type u_10} [inst_4 : (i : ι) → AddCommGroup (φv i)]
  [inst_5 : (i : ι) → Module k (φv i)] [Finite ι] [inst_7 : DecidableEq ι] {f g : ((i : ι) → φv i) →ᵃ[k] P2}
  [Nonempty ι],
  (∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap) → f = g
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forward.injEq : ∀ (term : Aesop.RuleTerm) (immediate : Aesop.UnorderedArraySet Aesop.PremiseIndex) (isDestruct : Bool)
  (term_1 : Aesop.RuleTerm) (immediate_1 : Aesop.UnorderedArraySet Aesop.PremiseIndex) (isDestruct_1 : Bool),
  (Aesop.RuleTacDescr.forward term immediate isDestruct = Aesop.RuleTacDescr.forward term_1 immediate_1 isDestruct_1) =
    (term = term_1 ∧ immediate = immediate_1 ∧ isDestruct = isDestruct_1)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toListRev_take_zip : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂]
  [Std.Iterators.Productive α₁ Id] [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β₁} {it₂ : Std.Iter β₂} {n : ℕ},
  (Std.Iter.take n (it₁.zip it₂)).toListRev = ((Std.Iter.take n it₁).toList.zip (Std.Iter.take n it₂).toList).reverse
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValued.def`. -/
FunctionField.inftyValuedFqt.def : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc F},
  Valued.v x = RatFunc.inftyValuationDef F x
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_finset_iff_smul_finset_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.op_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (b : CategoryTheory.Limits.BinaryBicone P Q), b.op.snd = b.inr.op
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_natCast_lt_lift : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.beth ↑n < Cardinal.lift.{v, u} c ↔ Cardinal.beth ↑n < c
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.Monic.C_dvd_iff_isUnit : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R}, p.Monic → ∀ {a : R}, Polynomial.C a ∣ p ↔ IsUnit a
-- Mathlib.Topology.Algebra.Group.Basic
/-- A version of `Homeomorph.addRight (-a) b` that is defeq to `b - a`.  -/
Homeomorph.subRight : {G : Type w} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [IsTopologicalAddGroup G] → G → G ≃ₜ G
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
algebraicIndependent_equiv' : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (e : ι ≃ ι') {f : ι' → A} {g : ι → A},
  f ∘ ⇑e = g → (AlgebraicIndependent R g ↔ AlgebraicIndependent R f)
-- Mathlib.Util.Export
Lean.Export.State.stk : Lean.Export.State → Array (Bool × Lean.Export.Entry)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.prop_hom_right : ∀ {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 : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (self : X.Hom Y), W self.right
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (g : f.right ⟶ f'.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g) = f'.hom)
      CategoryTheory.StructuredArrow.homMk._auto_1),
  (CategoryTheory.StructuredArrow.homMk g w).right = g
-- Lean.Data.Lsp.Basic
/-- If this field is present and the editor supports it,
`newText` is ignored
and an interactive snippet edit is performed instead.

The use of snippets in `TextEdit`s
is a Lean-specific extension to the LSP standard,
so `newText` should still be set to a correct value
as fallback in case the editor does not support this feature.
Even editors that support snippets may not always use them;
for instance, if the file is not already open,
VS Code will perform a normal text edit in the background instead.  -/
Lean.Lsp.TextEdit.leanExtSnippet? : Lean.Lsp.TextEdit → Option Lean.Lsp.SnippetString
-- Mathlib.Analysis.RCLike.Basic
RCLike.reLm_coe : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.reLm = ⇑RCLike.re
-- Mathlib.Data.Sym.Basic
Sym.cons_inj_left : ∀ {α : Type u_1} {n : ℕ} (a a' : α) (s : Sym α n), a ::ₛ s = a' ::ₛ s ↔ a = a'
-- Lean.Expr
Lean.BinderInfo.hash : Lean.BinderInfo → UInt64
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderTriple.of_toNNReal : ∀ {p q r : ENNReal}, p.toNNReal.HolderTriple q.toNNReal r.toNNReal → p.HolderTriple q r
-- Init.Data.SInt.Basic
/-- Signed 8-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 8-bit value.
 -/
Int8 : Type