mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- Truncation of the multivariate power series `1`  -/
MvPowerSeries.trunc'_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ),
  (MvPowerSeries.trunc' R n) 1 = 1
-- Lean.Language.Basic
/-- Creates a finished snapshot task.  -/
Lean.Language.SnapshotTask.finished : {α : Type} → Option Lean.Syntax → α → Lean.Language.SnapshotTask α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_eq_get!_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} [inst_2 : Inhabited (β a)], t.get! a = (t.get? a).get!
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.gcdCoeffs : Lean.Grind.CommRing.Poly → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.sub_toNat_mod_cancel_of_msb_true : ∀ {w : ℕ} {x : BitVec w}, x.msb = true → (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat
-- Qq.Match
Qq.Impl.PatternVar.mk.inj : ∀ {name : Lean.Name} {arity : ℕ} {mvar : Lean.Expr} {stx : Lean.Term} {name_1 : Lean.Name} {arity_1 : ℕ}
  {mvar_1 : Lean.Expr} {stx_1 : Lean.Term},
  { name := name, arity := arity, mvar := mvar, stx := stx } =
      { name := name_1, arity := arity_1, mvar := mvar_1, stx := stx_1 } →
    name = name_1 ∧ arity = arity_1 ∧ mvar = mvar_1 ∧ stx = stx_1
-- Mathlib.Data.Multiset.Defs
Multiset.Subset.refl : ∀ {α : Type u_1} (s : Multiset α), s ⊆ s
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `StrongDual.extendRCLikeₗ`.

---

The extension `StrongDual.extendRCLike` as a linear equivalence between the algebraic duals.

When `F` is a normed space, this can be upgraded to an *isometric* linear equivalence, see
`StrongDual.extendRCLikeₗᵢ`.  -/
RCLike.extendTo𝕜ₗ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : TopologicalSpace F] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module 𝕜 F] →
            [ContinuousConstSMul 𝕜 F] →
              [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F ≃ₗ[ℝ] StrongDual 𝕜 F
-- Mathlib.Order.Cofinal
/-- **Alias** of `isCofinal_setOfPred_imp_lt`.

---

The set of "records" (the smallest inputs yielding the highest values) with respect to a
well-ordering of `α` is a cofinal set.  -/
isCofinal_setOf_imp_lt : ∀ {α : Type u_1} [inst : LinearOrder α] (r : α → α → Prop) [h : IsWellFounded α r],
  IsCofinal {a | ∀ (b : α), r b a → b < a}
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit_fold : ∀ {n : ℕ} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (assignments0_size : assignments0.size = n)
  (rupUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n)
  (b : Bool) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size rupUnits
      assignments assignments_size →
    let update_res :=
      List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (rupUnits, assignments, b) units;
    have update_res_size := ⋯;
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size update_res.1
      update_res.2.1 update_res_size
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right] (b : J.R)
  {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) h
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatParam : Lean.IR.Param → Std.Format
-- Init.Data.Array.Range
Array.zipIdx_singleton : ∀ {α : Type u_1} {x : α} {k : ℕ}, #[x].zipIdx k = #[(x, k)]
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.insertMany_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF)
  {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)] {l : ρ},
  Std.DHashMap.Raw.Const.insertMany m l = ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany ⟨m, ⋯⟩ l)
-- Init.Data.BitVec.Folds
/-- Constructs a bitvector by iteratively computing a state for each bit using the function `f`,
starting with the initial state `s`. At each step, the prior state and the current bit index are
passed to `f`, and it produces a bit along with the next state value. These bits are assembled into
the final bitvector.

It produces a sequence of state values `[s_0, s_1 .. s_w]` and a bitvector `v` where `f i s_i =
(s_{i+1}, b_i)` and `b_i` is bit `i`th least-significant bit in `v` (e.g., `getLsb v i = b_i`).

The theorem `iunfoldr_replace` allows uses of `BitVec.iunfoldr` to be replaced with declarative
specifications that are easier to reason about.
 -/
BitVec.iunfoldr : {w : ℕ} → {α : Type u_1} → (Fin w → α → α × Bool) → α → α × BitVec w
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry : Type → Type
-- Mathlib.MeasureTheory.Group.Convolution
/-- Scoped notation for the additive convolution of measures.  -/
MeasureTheory.«term_∗_» : Lean.TrailingParserDescr
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `takeWhile₂`.  -/
List.takeWhile₂TR : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → List α → List β → List α × List β
-- Std.Http.Data.Method
Std.Http.Method.propfind.sizeOf_spec : sizeOf Std.Http.Method.propfind = 1
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearMapAt_apply_of_mem : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : E b), (Bundle.Trivialization.continuousLinearMapAt R e b) y = (↑e ⟨b, y⟩).2
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c₆_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.c₆ = -W.b₂ ^ 3
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.instHPowFinNatOfNeZero : {n : ℕ} → [NeZero n] → HPow (Fin n) ℕ (Fin n)
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.irreducible_mul_X_add : ∀ {n : Type u_3} {R : Type u_4} [inst : CommRing R] [IsDomain R] (f g : MvPolynomial n R) (i : n),
  f ≠ 0 → i ∉ f.vars → i ∉ g.vars → IsRelPrime f g → Irreducible (f * MvPolynomial.X i + g)
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan_eq_point : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : Affine.Simplex 𝕜 P 0)
  (p : P), ↑(s.orthogonalProjectionSpan p) = s.points 0
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderBEqOpposite : ∀ {α : Type u_1} {il : LE α} {ib : BEq α} [Std.LawfulOrderBEq α], Std.LawfulOrderBEq α
-- Mathlib.GroupTheory.OrderOfElement
powCardSubgroup.eq_1 : ∀ {G : Type u_6} [inst : Group G] [inst_1 : Fintype G] (S : Set G) (hS : S.Nonempty),
  powCardSubgroup S hS = subgroupOfIdempotent (S ^ Fintype.card G) ⋯ ⋯
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.HasCoeffs.coeffs_subset_range : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} {inst : CommRing R} {inst_1 : CommRing S}
  {inst_2 : Algebra R S} {P : Algebra.Presentation R S ι σ} {R₀ : Type u_5} {inst_3 : CommRing R₀}
  {inst_4 : Algebra R₀ R} {inst_5 : Algebra R₀ S} {inst_6 : IsScalarTower R₀ R S} [self : P.HasCoeffs R₀],
  P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.rTensor_refl : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  LinearEquiv.rTensor M (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R N M)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- Left multiplication by `g`. It is meant to mimic the usual notation in Lie groups.
Used mostly through the notation `𝑳`.
Lemmas involving `smoothLeftMul` with the notation `𝑳` usually use `L` instead of `𝑳` in the
names.  -/
smoothLeftMul : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {G : Type u_4} →
                  [inst_4 : Mul G] →
                    [inst_5 : TopologicalSpace G] →
                      [inst_6 : ChartedSpace H G] → G → [ContMDiffMul I (↑⊤) G] → ContMDiffMap I I G G ↑⊤
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_def' : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion = ⋃ J ∈ π.boxes, ↑J
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk'_apply : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (x : G), (QuotientAddGroup.mk' N) x = ↑x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffWithinAt_finsetSum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reset.sizeOf_spec : ∀ (n : ℕ) (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.reset n x) = 1 + sizeOf n + sizeOf x
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.homotopyEquiv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  (HomologicalComplex.pathObject.homotopyEquiv K hc).hom = HomologicalComplex.pathObject.ι K
-- Mathlib.RingTheory.Artinian.Module
/-- A module is Artinian iff every decreasing chain of submodules stabilizes.  -/
monotone_stabilizes_iff_artinian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsArtinian R M
-- Mathlib.Topology.Algebra.ConstMulAction
instContinuousConstVAddULift : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α],
  ContinuousConstVAdd (ULift.{u_4, u_1} M) α
-- Aesop.Forward.RuleInfo
/-- A slot represents a maximal premise of a forward rule, i.e. a premise with
no forward dependencies. The goal of forward reasoning is to assign a
hypothesis to each slot in such a way that the assignments agree on all
variables shared between them.

Exceptionally, a slot can also represent the rule pattern substitution. Rules
with a rule pattern have exactly one such slot, which is assigned an arbitrary
premise index.  -/
Aesop.Slot : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d),
  I.sndPiMapOfIsLimit c hd =
    CategoryTheory.Limits.Fan.IsLimit.lift hd fun i => CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (I.snd i)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.constantCoeff_invOfUnit : ∀ {R : Type u_1} [inst : Ring R] (φ : PowerSeries R) (u : Rˣ), PowerSeries.constantCoeff (φ.invOfUnit u) = ↑u⁻¹
-- Mathlib.Topology.Homotopy.Lifting
/-- A version of `IsCoveringMap.existsUnique_continuousMap_lifts` for maps
that are covering on a subset of the codomain.

Let `p` be a covering map on `s`.
Let `f` be a continuous map with a simply connected locally path connected domain
such that all values of `f` belong to `s`.
Given a point `a₀` in the domain of `f` and a lift `e₀` of `f a₀` along `p`,
there exists a unique lift `F` of `f` along `p` such that `F a₀ = e₀`.
 -/
IsCoveringMapOn.existsUnique_continuousMap_lifts : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] {s : Set X},
  IsCoveringMapOn p s →
    ∀ (f : C(A, X)) {a₀ : A} {e₀ : E}, p e₀ = f a₀ → (∀ (a : A), f a ∈ s) → ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₂.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_max?_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.max?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Data.Nat.PSub
Nat.psub_eq_none : ∀ {m n : ℕ}, m.psub n = none ↔ m < n
-- Mathlib.Topology.Algebra.MulAction
continuousVAdd_iInf : ∀ {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : VAdd M X]
  {ts' : ι → TopologicalSpace X}, (∀ (i : ι), ContinuousVAdd M X) → ContinuousVAdd M X
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C]
  (A₀ : CategoryTheory.Subobject X) (J : Type w) [inst_3 : LinearOrder J] [inst_4 : OrderBot J] [inst_5 : SuccOrder J]
  [inst_6 : WellFoundedLT J] {j j' : J} (f : j ⟶ j'),
  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver hG A₀ J).map f =
    CategoryTheory.MonoOver.homMk
      ((transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j A₀).ofLE
        (transfiniteIterate (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG) j' A₀) ⋯)
      ⋯
-- Mathlib.Tactic.Ring.Common
/-- A division semiring instance on `α`, if available.  -/
Mathlib.Tactic.Ring.Common.Cache.dsα : {u : Lean.Level} →
  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → Mathlib.Tactic.Ring.Common.Cache sα → Option Q(Semifield «$α»)
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv.eq_4 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (P Q : RegularExpression α), (P.plus Q).deriv x = P.deriv x + Q.deriv x
-- Lean.Meta.Sym.Arith.Types
/-- Cached `getDecLevel type`  -/
Lean.Meta.Sym.Arith.Semiring.u : Lean.Meta.Sym.Arith.Semiring → Lean.Level
-- Mathlib.Analysis.InnerProductSpace.ProdL2
/-- The product of two orthonormal bases is a basis for the L2-product.  -/
OrthonormalBasis.prod : {𝕜 : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {E : Type u_4} →
        {F : Type u_5} →
          [inst : RCLike 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : InnerProductSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : InnerProductSpace 𝕜 F] →
                    [inst_5 : Fintype ι₁] →
                      [inst_6 : Fintype ι₂] →
                        OrthonormalBasis ι₁ 𝕜 E →
                          OrthonormalBasis ι₂ 𝕜 F → OrthonormalBasis (ι₁ ⊕ ι₂) 𝕜 (WithLp 2 (E × F))
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.recOneCoe_coe : ∀ {α : Type u} {motive : WithOne α → Sort u_1} (h₁ : motive 1) (h₂ : (a : α) → motive ↑a) (a : α),
  WithOne.recOneCoe h₁ h₂ ↑a = h₂ a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Raw α β),
  m = m_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → m.alter a f = m_1.alter a f_1