mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CharP.Lemmas
add_pow_prime_eq' : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ},
  Nat.Prime p →
    ∀ (x y : R), (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
-- Mathlib.RingTheory.MvPowerSeries.Restricted
/-- Restricted power series as an additive subgroup of `MvPowerSeries σ R`.  -/
MvPowerSeries.IsRestricted.addSubgroup : {R : Type u_1} → [inst : NormedRing R] → {σ : Type u_2} → (σ → ℝ) → AddSubgroup (MvPowerSeries σ R)
-- Std.Tactic.BVDecide.LRAT.Actions
/-- `Action` where variables are (positive) `Nat`, clauses are arrays of `Int`, and ids are `Nat`.
This Action type is meant to be a convenient target for parsing LRAT proofs.
 -/
Std.Tactic.BVDecide.LRAT.IntAction : Type
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Canonical ring equivalence between `WithVal v` and `WithVal w`.  -/
WithVal.equivWithVal : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      [inst_1 : Ring R] →
        {Γ'₀ : Type u_3} →
          [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] →
            (v : Valuation R Γ₀) → (w : Valuation R Γ'₀) → WithVal v ≃+* WithVal w
-- Mathlib.Data.FinEnum
FinEnum.equiv_up : ∀ {α : Type u} [inst : FinEnum α] (a : α), FinEnum.equiv { down := a } = FinEnum.equiv a
-- Mathlib.Topology.Algebra.ConstMulAction
punctured_nhds_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G) (x : α), nhdsWithin (c +ᵥ x) {c +ᵥ x}ᶜ = c +ᵥ nhdsWithin x {x}ᶜ
-- Lean.Language.Basic
/-- Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree
preorder.  -/
Lean.Language.SnapshotTree.forM : {m : Type u_1 → Type u_2} →
  [Monad m] → Lean.Language.SnapshotTree → (Lean.Language.Snapshot → m PUnit.{u_1 + 1}) → m PUnit.{u_1 + 1}
-- Lean.Meta.IndPredBelow
/-- Map from motive to motive index (opposite of `motives[·]`)  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.motiveToIdx : Lean.Meta.IndPredBelow.Context✝ → Lean.FVarIdMap ℕ
-- Std.Time.Zoned.Database.TzIf
/-- Represents the local time type information, including offset and daylight saving details.
 -/
Std.Time.TimeZone.TZif.LocalTimeType : Type
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.iff_of_surjective : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_6} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Function.Surjective ⇑(algebraMap R A) → (Algebra.FormallySmooth R A ↔ IsIdempotentElem (RingHom.ker (algebraMap R A)))
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulActionMonoidHom : {M : Type u_5} →
  {A : Type u_7} →
    {B : Type u_8} →
      [inst : Monoid M] →
        [inst_1 : Monoid A] → [MulDistribMulAction M A] → [inst_3 : MulOneClass B] → MulAction Mᵈᵐᵃ (A →* B)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.ConstructProducts.conesEquivInverseObj_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (B : C) {J : Type w}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) (c : CategoryTheory.Limits.Cone F)
  (X : CategoryTheory.Limits.WidePullbackShape J),
  (CategoryTheory.Over.ConstructProducts.conesEquivInverseObj B F c).π.app X =
    Option.casesOn X c.pt.hom fun j => CategoryTheory.Over.Hom.left (c.π.app { as := j })
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    {a b : R} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → [Algebra S R] → Algebra S (QuadraticAlgebra R a b)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.coeq₃_condition₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C}
  (f g h : j₁ ⟶ j₂),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h)
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_exp_Iic : ∀ (c : ℝ), ∫ (x : ℝ) in Set.Iic c, Real.exp x = Real.exp c
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mulSaturated : ∀ {M : Type u_1} [inst : MulOneClass M] (self : SaturatedSubmonoid M), self.MulSaturated
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.mk.sizeOf_spec : ∀ {α : Sort u_1} [inst : SizeOf α] (content : α) (location : Lean.Syntax) (seen : Bool),
  sizeOf { content := content, location := location, seen := seen } = 1 + sizeOf content + sizeOf location + sizeOf seen
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc : ∀ {n : Type u} (R : CommRingCat) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n R).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) h
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le : ∀ {R : Type u} [inst : CommRing R] {f : Polynomial R} {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : R}
  {x : S},
  (Polynomial.aeval x) f = 0 →
    f.Monic →
      f.IsWeaklyEisensteinAt (R ∙ p) →
        ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ i
-- Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
CategoryTheory.Abelian.epiWithInjectiveKernel_iff_of_isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.Limits.IsZero Y → (CategoryTheory.Abelian.epiWithInjectiveKernel f ↔ CategoryTheory.Injective X)
-- Mathlib.Data.Set.Image
Set.image_eq_image : ∀ {α : Type u_1} {β : Type u_2} {s t : Set α} {f : α → β}, Function.Injective f → (f '' s = f '' t ↔ s = t)
-- Mathlib.Condensed.Light.Functors
/-- The functor from `LightProfinite` to `LightCondSet` is monoidal with respect to the cartesian
monoidal structure.
 -/
instMonoidalLightProfiniteLightCondSetLightProfiniteToLightCondSet : lightProfiniteToLightCondSet.Monoidal
-- Mathlib.CategoryTheory.Join.Basic
/-- Equivalent categories have equivalent joins.  -/
CategoryTheory.Join.mapPairEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (C ≌ C') → (D ≌ D') → (CategoryTheory.Join C D ≌ CategoryTheory.Join C' D')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) {u : R},
  IsUnit u → (W'.Nonsingular (u • P) ↔ W'.Nonsingular P)
-- Mathlib.Topology.Sheaves.Presheaf
/-- restriction of a section along a subset relation  -/
AlgebraicGeometry.«term_|_ₗ_⟪_⟫» : Lean.TrailingParserDescr
-- Std.Time.Internal.Bounded
/-- Convert a `Bounded.LE` to an Int.
 -/
Std.Time.Internal.Bounded.LE.toInt : {lo hi : ℤ} → Std.Time.Internal.Bounded.LE lo hi → ℤ
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- `mabs a`, denoted `|a|ₘ`, is the absolute value of `a`.  -/
«term|___|ₘ» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.copy.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = ↑S),
  S.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯ }
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt8.size ≤ n →
    (UInt8.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt8.size - 1) UInt8.toUInt32_ofNatClamp_of_le._proof_1
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.lintegral_rnDeriv_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, ∫⁻ (x : α), μ.rnDeriv ν x ∂ν ≤ μ Set.univ
-- Mathlib.Topology.Specialization
Specialization.ofEquiv_inj : ∀ {α : Type u_1} {a b : Specialization α}, Specialization.ofEquiv a = Specialization.ofEquiv b ↔ a = b
-- Init.Data.Vector.Lemmas
Vector.toArray_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {start stop : ℕ},
  (xs.extract start stop).toArray = xs.toArray.extract start stop
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.instInhabitedState : Inhabited Lean.CollectLevelMVars.State
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map : ∀ {X Y : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair} (a : X ⟶ Y),
  CategoryTheory.Limits.walkingCospanOpEquiv.inverse.map a =
    CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair X Y a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- Given `F : WalkingCospan ⥤ C`, which is really the same as `cospan (F.map inl) (F.map inr)`,
and a cone on `F`, we get a pullback cone on `F.map inl` and `F.map inr`.  -/
CategoryTheory.Limits.PullbackCone.ofCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      CategoryTheory.Limits.Cone F →
        CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
          (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- `f : ℂ → E` is analytic at `z` iff it's differentiable near `z`  -/
Complex.analyticAt_iff_eventually_differentiableAt : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ},
  AnalyticAt ℂ f c ↔ ∀ᶠ (z : ℂ) in nhds c, DifferentiableAt ℂ f z
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instDiv.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Div Y],
  LocallyConstant.instDiv = { div := fun f g => { toFun := ⇑f / ⇑g, isLocallyConstant := ⋯ } }
-- Mathlib.Data.Finset.Sups
Finset.infs_inter_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t₁ t₂ : Finset α},
  s ⊼ (t₁ ∩ t₂) ⊆ s ⊼ t₁ ∩ s ⊼ t₂
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend_eq_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {b : β} {c : γ} {f : α → γ},
  Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c) → di.extend f b = c
-- Init.Data.Nat.Basic
Nat.le_sub_one_of_lt : ∀ {a b : ℕ}, a < b → a ≤ b - 1
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → FunLike (CompleteLatticeHom α β) α β
-- Mathlib.Data.Matrix.Basis
Matrix.singleLinearMap_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid α] [inst_4 : Module R α] (i : m) (j : n) (a : α),
  (Matrix.singleLinearMap R i j) a = Matrix.single i j a
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- If `x` is not an accumulation point of `s`, then the tangent cone of `s` at `x`
is a subset of `{0}`.  -/
tangentConeAt_subset_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s : Set E} {x : E} [T2Space E],
  ¬AccPt x (Filter.principal s) → tangentConeAt 𝕜 s x ⊆ 0
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The injection induced by the natural homomorphism from `Rˣ` to `K⟮∅, n⟯`.  -/
IsDedekindDomain.selmerGroup.fromUnitLift : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              {n : ℕ} → [Fact (0 < n)] → Rˣ ⧸ (powMonoidHom n).range →* ↥IsDedekindDomain.selmerGroup
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
ContMDiffCovariantDerivativeOn.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] {k : WithTop ℕ∞} {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
  {u : Set M},
  (∀ {σ : (x : M) → V x},
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) (k + 1) (fun x => ⟨x, σ x⟩) u →
        ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 (E →L[𝕜] F))) k (fun x => ⟨x, cov σ x⟩) u) →
    ContMDiffCovariantDerivativeOn F k cov u
-- Mathlib.Tactic.DepRewrite
/-- Analogue of `Lean.MVarId.rewrite` with support for inserting casts.  -/
Lean.MVarId.depRewrite : Lean.MVarId →
  Lean.Expr →
    Lean.Expr → optParam Bool false → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.MetaM Lean.Meta.RewriteResult
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid form an additive group.  -/
AddUnits.instAddGroup : {α : Type u} → [inst : AddMonoid α] → AddGroup (AddUnits α)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IciExtend_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a x : α} (f : ↑(Set.Ici a) → β) (hx : x ∈ Set.Ici a),
  Set.IciExtend f x = f ⟨x, hx⟩
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.map_ne_zero_of_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R},
  g.IsDistinguishedAt I → PowerSeries.constantCoeff h ∉ I → f = ↑g * h → (PowerSeries.map (Ideal.Quotient.mk I)) f ≠ 0
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  (F G : CategoryTheory.Functor (↑(Set.Iic x)) C) (k₁ k₂ : K) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ x),
  CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G k₁ k₂ h₁₂ h₂ =
    (CategoryTheory.SmallObject.SuccStruct.arrowMap F k₁ k₂ h₁₂ h₂ =
      CategoryTheory.SmallObject.SuccStruct.arrowMap G k₁ k₂ h₁₂ h₂)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.map_dvd_map' : ∀ {R : Type u} {k : Type y} [inst : Field R] [inst_1 : Field k] (f : R →+* k) {x y : Polynomial R},
  Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y
-- Mathlib.Probability.Kernel.MeasurableLIntegral
/-- For an s-finite kernel `κ` and a function `f : α → β → ℝ≥0∞` which is measurable when seen as a
map from `α × β` (hypothesis `Measurable (uncurry f)`), the integral `a ↦ ∫⁻ b, f a b ∂(κ a)` is
measurable.  -/
Measurable.lintegral_kernel_prod_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal},
  Measurable (Function.uncurry f) → Measurable fun a => ∫⁻ (b : β), f a b ∂κ a
-- Mathlib.RingTheory.GradedAlgebra.FiniteType
GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero : ∀ {S : Type u_1} {σ : Type u_2} {ι : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing S]
  [inst_3 : SetLike σ S] [inst_4 : AddSubgroupClass σ S] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜]
  [Algebra.FiniteType (↥(𝒜 0)) S], ∃ s, Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `single` as a `LinearMap`.  -/
lp.lsingle : {𝕜 : Type u_1} →
  {α : Type u_3} →
    {E : α → Type u_4} →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : NormedRing 𝕜] →
          [inst_2 : (i : α) → Module 𝕜 (E i)] →
            [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] →
              [DecidableEq α] → (p : ENNReal) → (i : α) → E i →ₗ[𝕜] ↥(lp E p)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.center_eq_bot : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], 4 ≤ Nat.card α → Subgroup.center ↥(alternatingGroup α) = ⊥
-- Std.Data.ExtDHashMap.Basic
/-- Extensional dependent hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
must be an equivalence relation and `a == b` must imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

In contrast to regular dependent hash maps, `Std.ExtDHashMap` offers several extensionality lemmas
and therefore has more lemmas about equality of hash maps. This however also makes it lose the
ability to iterate freely over the hash map.

These hash maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.DHashMap.Raw` and
`Std.DHashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer
`DHashMap` over `DHashMap.Raw`.
 -/
Std.ExtDHashMap : (α : Type u) → (α → Type v) → [BEq α] → [Hashable α] → Type (max u v)
-- Lean.Util.LeanOptions
Lean.LeanOption.mk : Lean.Name → Lean.LeanOptionValue → Lean.LeanOption
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.isClopen : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (U : OpenSubgroup G),
  IsClopen ↑U
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.pow_eq_closure_pow_set : ∀ {R : Type u_2} [inst : Semiring R] (s : AddSubmonoid R) (n : ℕ), s ^ n = AddSubmonoid.closure (↑s ^ n)
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceTo_endPos : ∀ {s : String.Slice}, s.sliceTo s.endPos = s
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addConvolution_indicator_zero_left : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {F : Type u_6} [inst : AddMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid F] [inst_4 : Module S E] [inst_5 : Module S F]
  [inst_6 : TopologicalSpace F] (L : E →ₗ[S] F →ₗ[S] F) (e : E) (f : M → F),
  (∀ (y : F), (L e) y = y) → DiscreteConvolution.addConvolution L ({0}.indicator fun x => e) f = f
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f₁ : i₀ ⟶ i₁) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_EIsoH_hom._auto_3),
  CategoryTheory.CategoryStruct.comp
      (X.πE (CategoryTheory.CategoryStruct.id i₀) f₁ (CategoryTheory.CategoryStruct.id i₁) n₀ n₁ n₂ hn₁ hn₂)
      (X.EIsoH f₁ n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.cyclesIsoH f₁ n₁ n₂ hn₂).hom
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.reset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (n : ℕ) (var : Lean.FVarId)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_17),
  sizeOf (Lean.Compiler.LCNF.LetValue.reset n var h) = 1 + sizeOf n + sizeOf var + sizeOf h
-- Mathlib.MeasureTheory.Group.ModularCharacter
/-- Independence of addModularCharacterFun from the chosen Haar measure  -/
MeasureTheory.Measure.addModularCharacterFun_eq_addHaarScalarFactor : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G] [inst_4 : MeasurableSpace G] [inst_5 : BorelSpace G] (μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] (g : G),
  MeasureTheory.Measure.addModularCharacterFun g = (MeasureTheory.Measure.map (fun x => x + g) μ).addHaarScalarFactor μ
-- Lean.Meta.WHNF
/-- If `e` is of the form `Expr.const declName us`, executes `k info us` if
- `declName` is in the `Environment` and (is unfoldable or `ignoreTransparency = true`)
- `info` is the `ConstantInfo` associated with `declName`.

Otherwise executes `failK`.
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.matchConstAux : {α : Type} →
  Lean.Expr →
    (Unit → Lean.MetaM α) → (Lean.ConstantInfo → List Lean.Level → Lean.MetaM α) → optParam Bool false → Lean.MetaM α
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algebra' : (S : Type u_1) →
  (R : Type u) →
    (M : Type v) →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra S R] →
              [inst_4 : Module S M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : SMulCommClass R Rᵐᵒᵖ M] →
                      [IsScalarTower S R M] → [IsScalarTower S Rᵐᵒᵖ M] → Algebra S (TrivSqZeroExt R M)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqvAux.eq_1 : ∀ {α : Type u} (xs ys : Array α) (hsz : xs.size = ys.size) (p : α → α → Bool) (x_2 : 0 ≤ xs.size),
  xs.isEqvAux ys hsz p 0 x_2 = true
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.singleton : ∀ {α : Type u_2} [inst : PartialOrder α] {x : α}, CountableInfClosed {x}
-- Mathlib.Algebra.GroupWithZero.Action.Units
Equiv.smulRight_symm_apply : ∀ {α : Type u_4} {β : Type u_5} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α} (ha : a ≠ 0) (b : β),
  (Equiv.smulRight ha).symm b = a⁻¹ • b
-- Mathlib.Order.SuccPred.LinearLocallyFinite
Nonempty.some.congr_simp : ∀ {α : Sort u_3} (h : Nonempty α), h.some = h.some
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Shorthand for the 1st group homology of a `k`-linear `G`-representation `A`, `H₁(G, A)`,
defined as the 1st homology of the complex of inhomogeneous chains of `A`.  -/
groupHomology.H1 : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ModuleCat k
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula.0.tacticDerivative_simp : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedCommRing : Inhabited Lean.Meta.Grind.Arith.CommRing.CommRing
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k fallback : α}, m.contains k = true → m.getKeyD k fallback = k
-- Mathlib.Data.PNat.Defs
PNat.succPNat_natPred : ∀ (n : ℕ+), n.natPred.succPNat = n
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map_map₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ζ : Type u_4} {n : ℕ} (xs : List.Vector α n) (ys : List.Vector β n)
  (f₁ : γ → ζ) (f₂ : α → β → γ),
  List.Vector.map f₁ (List.Vector.map₂ f₂ xs ys) = List.Vector.map₂ (fun x y => f₁ (f₂ x y)) xs ys