mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ofSubsingletonₗ_symm_apply : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [inst : Semiring R]
  [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Module S M₃] [inst_6 : Module R M₃] [inst_7 : SMulCommClass R S M₃] [inst_8 : Subsingleton ι] (i : ι)
  (a : MultilinearMap R (fun x => M₂) M₃),
  (MultilinearMap.ofSubsingletonₗ R S M₂ M₃ i).symm a = (MultilinearMap.ofSubsingleton R M₂ M₃ i).symm a
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.ker_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage), (↑u).ker = pkg.decDom.X₀
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {a : α} {c : ℕ},
  (Std.HashSet.Raw.emptyWithCapacity c).get! a = default
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.surjective_vadd : ∀ (M : Type u_1) {α : Type u_3} [inst : VAdd M α] [AddAction.IsPretransitive M α] (x : α),
  Function.Surjective fun c => c +ᵥ x
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.pure : ∀ {x y : Std.Do.ExceptConds Std.Do.PostShape.pure}, x.entails y
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.idCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ →
      Lean.Elab.ContextInfo →
        Lean.LocalContext →
          Lean.Syntax →
            Lean.Name →
              Lean.Server.Completion.HoverInfo →
                Bool → Lean.Server.CancellableM (Array Lean.Lsp.ResolvableCompletionItem)
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnostics.noConfusionType : Sort v✝ → Lean.Lsp.WaitForDiagnostics → Lean.Lsp.WaitForDiagnostics → Sort v✝
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.closure_iUnion : ∀ {K : Type u} [inst : DivisionRing K] {ι : Sort u_1} (s : ι → Set K),
  Subfield.closure (⋃ i, s i) = ⨆ i, Subfield.closure (s i)
-- Mathlib.Algebra.Module.Injective
Module.Baer.of_equiv : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (e : Q ≃ₗ[R] M), Module.Baer R Q → Module.Baer R M
-- Init.Data.Option.Lemmas
Option.pelim_congr : ∀ {α : Type u_1} {β : Sort u_2} {o o' : Option α} {b b' : β} {f : (a : α) → o = some a → β}
  {g : (a : α) → o' = some a → β} (ho : o = o'),
  b = b' → (∀ (a : α) (ha : o' = some a), f a ⋯ = g a ha) → o.pelim b f = o'.pelim b' g
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_pow_eq : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), PowerSeries.X ^ n = (PowerSeries.monomial n) 1
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A]
  (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.ConcreteCategory.hom
        (A.map
          (CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.CategoryOfElements.π A))
            ((CategoryTheory.CategoryOfElements.π A).mapCone c))))
      c.pt.snd =
    CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.self_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.LimitPresentation.self X).diag = (CategoryTheory.Functor.const PUnit.{s + 1}).obj X
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Equivalence.induced_counitIso : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D),
  (CategoryTheory.Equivalence.induced e).counitIso =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState.mk : Array (Array (Lean.Name × Array Lean.Name)) → Lean.ExportedAxiomsState✝
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to a `USize`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toUSize : Float32.Model → USize
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_atBot_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [OrderTopology β],
  Asymptotics.IsEquivalent l u v → (Filter.Tendsto u l Filter.atBot ↔ Filter.Tendsto v l Filter.atBot)
-- Mathlib.CategoryTheory.MorphismProperty.Local
/-- If `P` holds for `𝒰.f i ≫ f` for all `i`, it holds for `f : X ⟶ Y` for any `K`-cover
`R` of X.  -/
CategoryTheory.MorphismProperty.IsLocalAtSource.of_forall_comp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [self : P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
  R ∈ K.coverings X → (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f)) → P f
-- Mathlib.Dynamics.OmegaLimit
eventually_mapsTo_of_isOpen_of_omegaLimit_subset : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [CompactSpace β] {v : Set β}, IsOpen v → omegaLimit f ϕ s ⊆ v → ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s v
-- Mathlib.MeasureTheory.Function.Floor
Int.measurable_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [inst_3 : TopologicalSpace R]
  [OrderTopology R] [inst_5 : MeasurableSpace R] [OpensMeasurableSpace R], Measurable Int.floor
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.eq_of_closure_subset : ∀ {α : Type u_2} {M : Matroid α} {X I J : Set α}, M.IsBasis I X → J ⊆ I → X ⊆ M.closure J → J = I
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A) (X : C)
  (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) (Φ.presheafFiberMapObjIso F K P).hom =
    Φ.toPresheafFiber X x (F.op.comp P)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  ↑(TensorProduct.quotTensorEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (TensorProduct.mk R (R ⧸ I) M) 1
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonneg_of_mul_nonpos_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R]
  [AddRightReflectLE R] {a b : R}, a * b ≤ 0 → a < 0 → 0 ≤ b
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.chromaticNumber_le_sum_left : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W}, G.chromaticNumber ≤ (G ⊕g H).chromaticNumber
-- Mathlib.RingTheory.Trace.Basic
IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : Type u_6}
  [inst_3 : Field F] [inst_4 : Algebra K F] (x : L),
  (Polynomial.map (algebraMap K F) (minpoly K x)).Splits →
    (algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).sum
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
/-- Assuming `j : J` is a limit element and that we have `∀ (i : J), i < j → Φ.Iteration i`,
this is the inductive system `Set.Iio j ⥤ C` which sends `⟨i, _⟩` to
`(iter i _).F.obj ⟨i, _⟩`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Φ : CategoryTheory.SmallObject.SuccStruct C} →
      {J : Type u} →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  {j : J} → ((i : J) → i < j → Φ.Iteration i) → CategoryTheory.Functor (↑(Set.Iio j)) C
-- Init.Data.Vector.Lemmas
Vector.count_toList : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {a : α} {xs : Vector α n}, List.count a xs.toList = Vector.count a xs
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processSort : Lean.Level → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.RingTheory.Finiteness.Ideal
Ideal.exists_pow_le_of_le_radical_of_fg : ∀ {R : Type u_3} [inst : CommSemiring R] {I J : Ideal R}, I ≤ J.radical → I.FG → ∃ n, I ^ n ≤ J
-- Mathlib.Data.Multiset.MapFold
Multiset.map_strictMono : ∀ {α : Type u_1} {β : Type v} (f : α → β), StrictMono (Multiset.map f)
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.natAdd m) (Finset.Ico i j) = Finset.Ico (Fin.natAdd m i) (Fin.natAdd m j)
-- Aesop.Index.Basic
Aesop.instInhabitedIndexMatchResult.default : {α : Type} → [Inhabited α] → Aesop.IndexMatchResult α
-- Mathlib.Algebra.Order.UpperLower
Set.OrdConnected.smul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α} {a : α},
  s.OrdConnected → (a • s).OrdConnected
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.hausdorffMeasure_measurePreserving_funUnique : ∀ (ι : Type u_1) (X : Type u_2) [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  [inst_3 : Unique ι] (d : ℝ),
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique ι X)) (MeasureTheory.Measure.hausdorffMeasure d)
    (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Ioo_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo ↑a ↑b = WithTop.some '' Set.Ioo a b
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.toArray_iter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.iter.toArray = m.toArray
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- A proof that the full subcategory inclusion is fully faithful  -/
SimplexCategory.Truncated.inclusion.fullyFaithful : (n : ℕ) → (SimplexCategory.Truncated.inclusion n).op.FullyFaithful
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Return true if `declName` is automatically generated,
or otherwise unsuitable as a lemma suggestion.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.blacklist : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
IsUnit.set : ∀ {α : Type u_2} [inst : Monoid α] {a : α}, IsUnit a → IsUnit {a}
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_iteratedFDeriv_zero : ∀ {𝕜 : 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] {f : E → F}
  {x : E}, ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖
-- Mathlib.RingTheory.ChainOfDivisors
emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [UniqueFactorizationMonoid N] [inst_4 : UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N},
  n ≠ 0 →
    ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)),
      emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharThreeNF_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.IsCharThreeNF
-- Mathlib.CategoryTheory.Abelian.Yoneda
CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor D C) [F.Full] {G : C}
  [CategoryTheory.Projective G],
  CategoryTheory.IsSeparator G →
    (∀ (X : D), ∃ p, CategoryTheory.Epi p) → (F.comp (CategoryTheory.preadditiveCoyonedaObj G)).Full
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
  (i : Fin (1 + 1)),
  (G.mapComposableArrowsObjMk₁Iso f).inv.app i =
    match i with
    | ⟨0, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj X)
    | ⟨1, isLt⟩ => CategoryTheory.CategoryStruct.id (G.obj Y)
-- Init.Core
Decidable.not_and_iff_or_not : ∀ {p q : Prop} [d₁ : Decidable p] [d₂ : Decidable q], ¬(p ∧ q) ↔ ¬p ∨ ¬q
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.isubtree.eq_def : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (x : PFunctor.Approx.Path F) (x_1 : F.M),
  PFunctor.M.isubtree x x_1 =
    match x, x_1 with
    | [], x => x
    | ⟨a, i⟩ :: ps, x => x.casesOn' fun a' f => if h : a = a' then PFunctor.M.isubtree ps (f (cast ⋯ i)) else default
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_j : ∀ {F : Type u_2} [inst : Field F] (j : F) [inst_1 : DecidableEq F], (WeierstrassCurve.ofJ j).j = j
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `Ioo a b` and
nonnegative on `Ioi b`. Then `f` attains its minimum on `Ioi a` at `b`.  -/
isMinOn_Ioi_of_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      DifferentiableOn ℝ f (Set.Ioi b) →
        (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioi b, 0 ≤ deriv f x) → IsMinOn f (Set.Ioi a) b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- the projection `pullback ⟶ S`  -/
CategoryTheory.Limits.ChosenPullback.p : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} → {f₂ : X₂ ⟶ S} → (self : CategoryTheory.Limits.ChosenPullback f₁ f₂) → self.pullback ⟶ S
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.contDiff_cosh : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.cosh
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
ContinuousMap.instNonUnitalCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] → [CompactSpace α] → [inst_2 : NonUnitalCStarAlgebra A] → NonUnitalCStarAlgebra C(α, A)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.toDescentData_obj : ∀ {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) (M : ↑(F.obj { as := Opposite.op S })),
  (F.toDescentData f).obj M = CategoryTheory.Pseudofunctor.DescentData.ofObj M
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.smul_sup : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M] (a : α)
  (S T : Submonoid M), a • (S ⊔ T) = a • S ⊔ a • T
-- Mathlib.Topology.Connected.Basic
isPreconnected_univ_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)},
  (∀ (i : ι), IsPreconnected (s i)) → IsPreconnected (Set.univ.pi s)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : m.WF) {h' : k ∈ Std.HashMap.Raw.filter f m},
  (Std.HashMap.Raw.filter f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For finite values `a₀`, the logarithmic counting function `logCounting f a₀` equals the logarithmic
counting function for the zeros of `f - a₀`.
 -/
ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E},
  ValueDistribution.logCounting f ↑a₀ = ValueDistribution.logCounting (f - fun x => a₀) 0
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_self`. -/
Set.diff_self : ∀ {α : Type u_1} {s : Set α}, s \ s = ∅
-- ImportGraph.Tools.FindHome
GoToModuleLinkProps.mk.inj : ∀ {modName modName_1 : Lean.Name}, { modName := modName } = { modName := modName_1 } → modName = modName_1
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.exists_add_eq_add_add_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), ∃ n, σ (g₁ + g₂) = σ g₁ + σ g₂ + S.inl n
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_add_left_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (x * z + y) → IsCoprime x y
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.reorder c_1) =
    (c = c_1)
-- Mathlib.Analysis.Normed.Module.Convex
convexHull_sphere_eq_closedBall : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [Nontrivial F] (x : F) {r : ℝ},
  0 ≤ r → (convexHull ℝ) (Metric.sphere x r) = Metric.closedBall x r
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {a b : R},
  (IsDiscreteValuationRing.addVal R) (a * b) =
    (IsDiscreteValuationRing.addVal R) a + (IsDiscreteValuationRing.addVal R) b
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.toGrothendieck_mono : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J K : CategoryTheory.Precoverage C},
  J ≤ K → J.toGrothendieck ≤ K.toGrothendieck
-- Init.Data.Array.Lemmas
Array.setIfInBounds_empty : ∀ {α : Type u_1} {i : ℕ} {a : α}, #[].setIfInBounds i a = #[]
-- Std.Sat.AIG.Basic
/-- For a `c : Cache α decls`, any index `idx` that is a cache hit for some `decl` is within bounds of `decls` (i.e. `idx < decls.size`).
 -/
Std.Sat.AIG.Cache.get?_bounds : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  (c : Std.Sat.AIG.Cache α decls) (decl : Std.Sat.AIG.Decl α), (↑c)[decl]? = some idx → idx < decls.size
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_expChar : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) {p : ℕ} [hR : ExpChar R p], (x - y) ^ p = x ^ p - y ^ p
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self : ∀ {w : ℕ} (n : BitVec w), n >>> n = 0#w
-- Mathlib.Algebra.BrauerGroup.Defs
CSA.toAlgCat : {K : Type u} → [inst : Field K] → CSA K → AlgCat K
-- Lean.Elab.Util
/-- Two names are from the same lexical scope if their scoping information modulo `MacroScopesView.name`
is equal.
 -/
Lean.MacroScopesView.equalScope : Lean.MacroScopesView → Lean.MacroScopesView → Bool
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_one_left_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, y ∣ x → IsRelPrime (x + 1) y
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
SzemerediRegularity.increment.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ),
  SzemerediRegularity.increment hP G ε = P.bind fun x => SzemerediRegularity.chunk hP G ε
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A purely inseparable extension has finite inseparable degree equal to degree.  -/
IsPurelyInseparable.finInsepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E],
  Field.finInsepDegree F E = Module.finrank F E
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'_inv_app : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (X : ModuleCat R₃),
  (ModuleCat.restrictScalarsComp' f g gf hgf).inv.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).inv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.keysArray_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keysArray = t₂.keysArray
-- Lean.Expr
/-- `.proj structName idx struct` is now the preferred form.
 -/
Lean.mkProj : Lean.Name → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_uIoc : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.uIoc x y = Set.uIoc ↑x ↑y
-- Mathlib.RingTheory.PowerSeries.Schroder
PowerSeries.coeff_largeSchroderSeries : ∀ (n : ℕ), (PowerSeries.coeff n) PowerSeries.largeSchroderSeries = n.largeSchroder
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.RationalMap.comp.congr_simp : ∀ {X Y Z : AlgebraicGeometry.Scheme} [inst : PreirreducibleSpace ↥X] [inst_1 : Nonempty ↥Y] (f f_1 : X.RationalMap Y)
  (e_f : f = f_1) [inst_2 : f.IsDominant] (g g_1 : Y.RationalMap Z), g = g_1 → f.comp g = f_1.comp g_1
-- Init.Data.SInt.Basic
/-- Decides whether one 8-bit signed integer is less than or equal to another. Usually accessed via the
`DecidableLE Int64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int64) ≤ 7 then "yes" else "no") = "yes"`
 * `(if (15 : Int64) ≤ 15 then "yes" else "no") = "yes"`
 * `(if (15 : Int64) ≤ 5 then "yes" else "no") = "no"`
 * `show (7 : Int64) ≤ 7 by decide`
 -/
Int64.decLe : (a b : Int64) → Decidable (a ≤ b)
-- Mathlib.Topology.Order.WithTop
WithTop.nhds_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] {r : ι},
  nhds ↑r = Filter.map WithTop.some (nhds r)
-- Init.Data.SInt.Lemmas
Int16.pow_succ : ∀ (x : Int16) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.CategoryTheory.Category.PartialFun
pointedToPartialFun_map : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : PartialFun.of { x // x ≠ X.point }),
  pointedToPartialFun.map f a = (PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val) a
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instSetLike.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.instSetLike = { coe := fun U => ↑↑U, coe_injective := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {f : β k → β k}, (Std.DTreeMap.Internal.Impl.modify k f t).getKey? k = if k ∈ t then some k else none