mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (hom' hom'_1 : ↑A →ₐc[R] ↑B),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Init.Data.AC
Lean.Data.AC.evalList : {α : Sort u_1} → (β : Sort u) → [Lean.Data.AC.EvalInformation α β] → α → List ℕ → β
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.motives.all : Lean.Option Bool
-- Mathlib.Algebra.Lie.AdjointAction.Basic
LieAlgebra.isNilpotent_ad_of_isNilpotent : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {L : LieSubalgebra R A}
  {x : ↥L}, IsNilpotent ↑x → IsNilpotent ((LieAlgebra.ad R ↥L) x)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_J : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g],
  (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).J = 𝒰.I₀
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.subsemigroup_eq_addSubgroup_of_ne_top : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  {s : UpperSet (ArchimedeanClass M)}, s ≠ ⊤ → ↑(ArchimedeanClass.subsemigroup s) = ↑(ArchimedeanClass.addSubgroup s)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_smul_right_eq_smul_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {c : NNReal},
  c ≠ 0 → InformationTheory.klDiv μ (c • ν) = ↑c * InformationTheory.klDiv (c⁻¹ • μ) ν
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_mono_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f g : β → α}, (∀ b ∈ s, f b ∣ g b) → s.lcm f ∣ s.lcm g
-- Mathlib.Topology.MetricSpace.PiNat
/-- In a product space `Π n, E n`, the cylinder set of length `n` around `x`, denoted
`cylinder x n`, is the set of sequences `y` that coincide with `x` on the first `n` symbols, i.e.,
such that `y i = x i` for all `i < n`.
 -/
PiNat.cylinder : {E : ℕ → Type u_1} → ((n : ℕ) → E n) → ℕ → Set ((n : ℕ) → E n)
-- Std.Data.HashSet.Lemmas
Std.HashSet.emptyWithCapacity_equiv_iff_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {c : ℕ},
  (Std.HashSet.emptyWithCapacity c).Equiv m ↔ m.isEmpty = true
-- Mathlib.Algebra.Regular.SMul
isSMulRegular_map : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [inst : SMul R M] [inst_1 : SMul S M] (f : R → S),
  (∀ (m : M), f a • m = a • m) → (IsSMulRegular M (f a) ↔ IsSMulRegular M a)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.embedding_inj : ∀ {K : Type u_1} [inst : Field K] {v₁ v₂ : NumberField.InfinitePlace K}, v₁.embedding = v₂.embedding ↔ v₁ = v₂
-- Mathlib.RingTheory.Flat.TorsionFree
Module.Flat.instOfIsDedekindDomainOfIsTorsionFree : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDedekindDomain R]
  [Module.IsTorsionFree R M], Module.Flat R M
-- Std.Http.Data.URI.Parser
/-- Parses a request target with combined parsing and validation.
 -/
Std.Http.URI.Parser.parseRequestTarget : optParam Std.Http.URI.Config { } → Std.Internal.Parsec.ByteArray.Parser Std.Http.RequestTarget
-- Mathlib.Order.Filter.Extr
IsMinOn.inter : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → ∀ (t : Set α), IsMinOn f (s ∩ t) a
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRooSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRooSlice._auto_1) →
      Std.Roo.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RooSlice α β)
-- Init.Data.Nat.Coprime
Nat.coprime_one_left : ∀ (n : ℕ), Nat.Coprime 1 n
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.self_trans_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  e.trans e.symm = MeasurableEquiv.refl α
-- Mathlib.Tactic.FunProp.Core
/-- Try to prove `e` using *pi lambda theorem*.

For example, `e = q(Continuous fun x y ↦ f x y)` and `funPropDecl` is `FunPropDecl` for
`Continuous`
 -/
Mathlib.Meta.FunProp.applyPiRule : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
      Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Lean.Widget.UserWidget
Lean.Widget.instToJsonGetWidgetSourceParams : Lean.ToJson Lean.Widget.GetWidgetSourceParams
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAt_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt p pos pos' ↔
    ∃ (h : pos' ≠ s.startPos), pos = pos'.prev h ∧ p ((pos'.prev h).get ⋯)
-- Mathlib.Order.Filter.Tendsto
/-- **Alias** of the reverse direction of `Filter.tendsto_map'_iff`. -/
Filter.tendsto_map' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ},
  Filter.Tendsto (f ∘ g) x y → Filter.Tendsto f (Filter.map g x) y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet : ∀ (k d : ℕ),
  Set.EqOn (iteratedDerivWithin k (fun z => cotTerm z d) UpperHalfPlane.upperHalfPlaneSet)
    (fun z => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k)))
    UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.Topology.EMetricSpace.Defs
EDist.ext_iff : ∀ {α : Type u_2} {x y : EDist α}, x = y ↔ edist = edist
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ} (m : ℕ)
  (hm : n + 1 = m), R.extMk 0 m hm ⋯ = 0
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.instCStarRing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : NonUnitalNormedRing β]
  [inst_3 : StarRing β] [inst_4 : CStarRing β], CStarRing C(α, β)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
This version assumes joint continuity of `f`, see `integrableOn_cfcₙ'` for a statement
with weaker assumptions.  -/
integrableOn_cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [CompleteSpace A] [inst_9 : TopologicalSpace X] [OpensMeasurableSpace X] {s : Set X},
  MeasurableSet s →
    ∀ (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)],
      ContinuousOn (Function.uncurry f) (s ×ˢ quasispectrum 𝕜 a) →
        (∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0) →
          (∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
            MeasureTheory.HasFiniteIntegral bound (μ.restrict s) →
              autoParam (p a) integrableOn_cfcₙ._auto_1 → MeasureTheory.IntegrableOn (fun x => cfcₙ (f x) a) s μ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (t.alter k f).contains k' = t.contains k'
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.of_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {m n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → m ≤ n → ContDiffWithinAt 𝕜 m f s x
-- Mathlib.NumberTheory.Padics.WithVal
Padic.isDenseInducing_cast_withVal : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)],
  IsDenseInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)
-- Mathlib.AlgebraicTopology.MooreComplex
/-- The normalized Moore complex in degree `n`, as a subobject of `X n`.
 -/
AlgebraicTopology.NormalizedMooreComplex.objX : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Abelian C] →
      (X : CategoryTheory.SimplicialObject C) → (n : ℕ) → CategoryTheory.Subobject (X.obj (Opposite.op { len := n }))
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- The codiagonal object of a morphism `f : X ⟶ Y` is `pushout f f`.  -/
CategoryTheory.Limits.pushout.codiagonalObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasPushout f f] → C
-- Mathlib.Order.Compare
cmp_eq_cmp_symm : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} {β : Type u_3} [inst_1 : LinearOrder β] {x' y' : β},
  cmp x y = cmp x' y' ↔ cmp y x = cmp y' x'
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_typein_succ : ∀ {o : Ordinal.{u_3}}, iSup ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonLocationLink.fromJson : Lean.Json → Except String Lean.Lsp.LocationLink
-- Init.Data.OfScientific
Float.exactlyRepresentablePowersOfTen.eq_1 : Float.exactlyRepresentablePowersOfTen =
  #[Float.ofBits 4607182418800017408, Float.ofBits 4621819117588971520, Float.ofBits 4636737291354636288,
    Float.ofBits 4652007308841189376, Float.ofBits 4666723172467343360, Float.ofBits 4681608360884174848,
    Float.ofBits 4696837146684686336, Float.ofBits 4711630319722168320, Float.ofBits 4726483295884279808,
    Float.ofBits 4741671816366391296, Float.ofBits 4756540486875873280, Float.ofBits 4771362005757984768,
    Float.ofBits 4786511204640096256, Float.ofBits 4801453603149578240, Float.ofBits 4816244402031689728,
    Float.ofBits 4831355200913801216, Float.ofBits 4846369599423283200, Float.ofBits 4861130398305394688,
    Float.ofBits 4876203697187506176, Float.ofBits 4891288408196988160, Float.ofBits 4906019910204099648,
    Float.ofBits 4921056587992461136, Float.ofBits 4936209963552724370]
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Given a `PreservesColimit₂` instance, extract the isomorphism between
a colimit of `uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)` and
`(G.obj c₁).obj c₂` where c₁ (resp. c₂) is a colimit of `K₁` (resp `K₂`).  -/
CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    {K₁ : CategoryTheory.Functor J₁ C₁} →
                      {K₂ : CategoryTheory.Functor J₂ C₂} →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] →
                            {c₁ : CategoryTheory.Limits.Cocone K₁} →
                              CategoryTheory.Limits.IsColimit c₁ →
                                {c₂ : CategoryTheory.Limits.Cocone K₂} →
                                  CategoryTheory.Limits.IsColimit c₂ →
                                    {c₃ :
                                        CategoryTheory.Limits.Cocone
                                          (CategoryTheory.Functor.uncurry.obj
                                            ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))} →
                                      CategoryTheory.Limits.IsColimit c₃ → ((G.obj c₁.pt).obj c₂.pt ≅ c₃.pt)
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homEquiv_symm_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (L : HomologicalComplex C c)
  [inst_3 : e.IsRelIff] (φ : { φ // e.HasLift φ }), (e.homEquiv K L).symm φ = e.liftExtend ↑φ ⋯
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toPartitionOfUnity_zero_of_zero : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) {i : ι} {x : X},
  (f i) x = 0 → (f.toPartitionOfUnity i) x = 0
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
/-- The closure of a property of objects of a category under colimits of
shape `J` for a category `J`.  -/
CategoryTheory.ObjectProperty.colimitClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u_1) → [CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairComp_hom_app_left : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] {J : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} J]
  {K : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} K] (Fₗ : CategoryTheory.Functor C E)
  (Fᵣ : CategoryTheory.Functor D E') (Gₗ : CategoryTheory.Functor E J) (Gᵣ : CategoryTheory.Functor E' K) (c : C),
  (CategoryTheory.Join.mapPairComp Fₗ Fᵣ Gₗ Gᵣ).hom.app (CategoryTheory.Join.left c) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (Gₗ.obj (Fₗ.obj c)))
-- Mathlib.Algebra.Module.Submodule.Map
AddMonoidHom.coe_toIntLinearMap_map : ∀ {A : Type u_9} {A₂ : Type u_10} [inst : AddCommGroup A] [inst_1 : AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A),
  Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instLawfulForwardPatternForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.LawfulForwardPattern p
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.hexnum.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.String.Iterator
String.Legacy.Iterator.mk.sizeOf_spec : ∀ (s : String) (i : String.Pos.Raw), sizeOf { s := s, i := i } = 1 + sizeOf s + sizeOf i
-- Mathlib.Topology.Order.HullKernel
/-- The set of relative-closed sets of the form `hull T a` for some `a` in `α` is closed under
pairwise union.  -/
PrimitiveSpectrum.hull_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] {T : Set α},
  (∀ p ∈ T, InfPrime p) →
    ∀ (a b : α), PrimitiveSpectrum.hull T (a ⊓ b) = PrimitiveSpectrum.hull T a ∪ PrimitiveSpectrum.hull T b
-- Init.Grind.Norm
Lean.Grind.or_assoc : ∀ (p q r : Prop), ((p ∨ q) ∨ r) = (p ∨ q ∨ r)
-- Init.ShareCommon
ShareCommon.Object : Type
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInrCompInverseAssociator_hom_app_down_down : ∀ (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] (X : D),
  ((CategoryTheory.sum.inlCompInrCompInverseAssociator C D E).hom.app X).down.down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inl (Sum.inr X))).down.down
      (CategoryTheory.CategoryStruct.id (Sum.inl (Sum.inr X))).down.down
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.edgeSetSumEquiv.match_1.congr_eq_2 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (x x_1 : V ⊕ W) (x_2 : (G ⊕g H).Adj x x_1)
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h) (u v : W)
  (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)),
  x = Sum.inr u →
    x_1 = Sum.inr v →
      x_2 ≍ h →
        (match x, x_1, x_2 with
          | Sum.inl u, Sum.inl v, h => h_1 u v h
          | Sum.inr u, Sum.inr v, h => h_2 u v h
          | Sum.inl u, Sum.inr v, h => h_3 u v h
          | Sum.inr u, Sum.inl v, h => h_4 u v h) ≍
          h_2 u v h
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.faulhaber_sum_div_prime_eq : ∀ {k p : ℕ} [Fact (Nat.Prime p)],
  (∑ i ∈ Finset.range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ Finset.range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- Maximal intersecting families are upper sets.  -/
Set.Intersecting.isUpperSet : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α},
  s.Intersecting → (∀ (t : Set α), t.Intersecting → s ⊆ t → s = t) → IsUpperSet s
-- Mathlib.NumberTheory.MahlerMeasure
/-- An upper bound on the number of integer polynomials of degree at most `n` and Mahler measure at
most `B`.  -/
Polynomial.card_mahlerMeasure_le_prod : ∀ (n : ℕ) (B : NNReal),
  {p | p.natDegree ≤ n ∧ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.ltoFun_apply : ∀ {R : Type u_6} {M : Type u_7} {N : Type u_8} {A : Type u_9} [inst : Semiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : Module A N] [inst_7 : SMulCommClass R A N] {f : M →ₗ[R] N}, (LinearMap.ltoFun R M N A) f = ⇑f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `η ◫ θ`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompAuxOf : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.HorizontalComp → m Lean.Expr
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instHasLimitWalkingParallelPairParallelPair : ∀ {X Y : ωCPO} (f g : X ⟶ Y), CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.eq_comp_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {α : Type u_3} (e : M ≃ₜ* N) (f : N → α) (g : M → α), f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection_self : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x : P), (Equiv.pointReflection x) x = x
-- Init.Data.ByteArray.Lemmas
ByteArray.size_extract : ∀ {a : ByteArray} {b e : ℕ}, (a.extract b e).size = min e a.size - b
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Restricting an open partial homeomorphism `e` to `e.source ∩ s` when `s` is open.
This is sometimes hard to use because of the openness assumption, but it has the advantage that
when it can be used then its `PartialEquiv` is defeq to `PartialEquiv.restr`.  -/
OpenPartialHomeomorph.restrOpen : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → (s : Set X) → IsOpen s → OpenPartialHomeomorph X Y
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.assoc_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y}
  {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ)
  (s : CategoryTheory.Limits.BinaryFan sXY.pt Z),
  (CategoryTheory.Limits.BinaryFan.assoc Q s).fst = CategoryTheory.CategoryStruct.comp s.fst sXY.fst
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_subtypeDomain : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {p : ι → Prop} [inst_3 : DecidablePred p] {f : Π₀ (i : ι), β i},
  (DFinsupp.subtypeDomain p f).support = Finset.subtype p f.support
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_injective : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f g : X ⟶ Y},
  Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY → f = g
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.right_inv : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : ContinuousMap.HomotopyEquiv X Y), (self.toFun.comp self.invFun).Homotopic (ContinuousMap.id Y)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.lieAlgebra.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  RootPairing.GeckConstruction.lieAlgebra b =
    LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (Set.range RootPairing.GeckConstruction.h ∪ Set.range RootPairing.GeckConstruction.e ∪
        Set.range RootPairing.GeckConstruction.f)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_elim : ∀ (ctx : Int.Internal.Linear.Context) (k₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (k₂ : ℤ) (p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_elim_cert k₁ p₁ k₂ p₂ = true →
    k₁ ∣ Int.Internal.Linear.Poly.denote' ctx p₁ → k₂ ∣ Int.Internal.Linear.Poly.denote' ctx p₂
-- Mathlib.Order.Filter.Pointwise
Filter.div_pure : ∀ {α : Type u_2} [inst : Div α] {f : Filter α} {b : α}, f / pure b = Filter.map (fun x => x / b) f
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The ring homomorphism associated to an inclusion of subfields.  -/
Subfield.inclusion : {K : Type u} → [inst : DivisionRing K] → {S T : Subfield K} → S ≤ T → ↥S →+* ↥T
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.nonMemberSubfamily_memberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  Finset.nonMemberSubfamily a (Finset.memberSubfamily a 𝒜) = Finset.memberSubfamily a 𝒜
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- The composition of positive linear maps is again a positive linear map.  -/
PositiveLinearMap.comp : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      {E₃ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid E₁] →
            [inst_2 : PartialOrder E₁] →
              [inst_3 : AddCommMonoid E₂] →
                [inst_4 : PartialOrder E₂] →
                  [inst_5 : AddCommMonoid E₃] →
                    [inst_6 : PartialOrder E₃] →
                      [inst_7 : Module R E₁] →
                        [inst_8 : Module R E₂] → [inst_9 : Module R E₃] → (E₂ →ₚ[R] E₃) → (E₁ →ₚ[R] E₂) → E₁ →ₚ[R] E₃
-- Init.Data.List.Zip
List.head?_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ},
  (List.zipWith f as bs).head? =
    match as.head?, bs.head? with
    | some a, some b => some (f a b)
    | x, x_1 => none
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_le_encard_self : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} (A : Set X), Metric.externalCoveringNumber ε A ≤ A.encard