mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.LFunction_isBigO_horizontal_of_eq_zero : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] {y : ℝ},
  y ≠ 0 ∨ χ ≠ 1 →
    DirichletCharacter.LFunction χ (1 + Complex.I * ↑y) = 0 →
      (fun x => DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => ↑x
-- Init.Data.Array.Attach
Array.back?_attach : ∀ {α : Type u_1} {xs : Array α}, xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The interval `[0,1]` as a compact set with non-empty interior.  -/
TopologicalSpace.PositiveCompacts.Icc01 : TopologicalSpace.PositiveCompacts ℝ
-- Init.Data.String.Decode
String.utf8EncodeCharFast.eq_1 : ∀ (c : Char),
  String.utf8EncodeCharFast c =
    if c.val ≤ 127 then [c.val.toUInt8]
    else
      if c.val ≤ 2047 then [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
      else
        if c.val ≤ 65535 then
          [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
        else
          [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
            (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
/-- If `c₁` and `c₂` are limit fans and `bc` is a limit binary fan on their cone
points, then the fan constructed from `combPairHoms` is a limit cone.  -/
CategoryTheory.Limits.Fan.combPairIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {ι₁ : Type u_1} →
      {ι₂ : Type u_2} →
        {f₁ : ι₁ → C} →
          {f₂ : ι₂ → C} →
            {c₁ : CategoryTheory.Limits.Fan f₁} →
              {c₂ : CategoryTheory.Limits.Fan f₂} →
                {bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt} →
                  CategoryTheory.Limits.IsLimit c₁ →
                    CategoryTheory.Limits.IsLimit c₂ →
                      CategoryTheory.Limits.IsLimit bc →
                        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk bc.pt (c₁.combPairHoms c₂ bc))
-- Init.Meta.Defs
/-- Type used to lift an arbitrary value into a type parameter so it can
appear in a proof goal.

It is used by the #check_tactic command.
 -/
Lean.Meta.CheckTactic.CheckGoalType : {α : Sort u} → α → Prop
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
/-- Lemma 4.2 from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.instIsIrreducible : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : CharZero K]
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] [inst_4 : AddCommGroup M] [inst_5 : Module K M]
  [inst_6 : AddCommGroup N] [inst_7 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  [inst_9 : P.IsCrystallographic] {b : P.Base} [P.IsReduced] [P.IsIrreducible] [Nonempty ι],
  LieModule.IsIrreducible K (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → K)
-- Lean.Meta.Coe
/-- Return `some (m, α)` if `type` can be reduced to an application of the form `m α` using `[reducible]` transparency.  -/
Lean.Meta.isTypeApp? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instCompatibleValueGroupWithZeroValuation : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R], (ValuativeRel.valuation R).Compatible
-- Mathlib.LinearAlgebra.Dimension.Finite
finrank_eq_zero_of_basis_imp_false : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  (∀ (s : Finset M) (a : Module.Basis (↑↑s) R M), False) → Module.finrank R M = 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Preconnected.degree_zero_iff : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph},
  H.Preconnected → ∀ (v : ↑H.verts) [inst : Fintype ↑(H.neighborSet ↑v)], H.degree ↑v = 0 ↔ H.verts.Subsingleton
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith.eq_def : ∀ (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}),
  Ordinal.veblenWith f o =
    if o = 0 then f
    else
      Ordinal.derivFamily fun x =>
        match (motive := { x // x ∈ Set.Iio o } → Ordinal.{u} → Ordinal.{u}) x with
        | ⟨x, property⟩ => Ordinal.veblenWith f x
-- Mathlib.Data.List.Sort
List.Pairwise.merge : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Total r] [IsTrans α r] {l l' : List α},
  List.Pairwise r l → List.Pairwise r l' → List.Pairwise r (l.merge l' fun x1 x2 => decide (r x1 x2))
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mapDomainLinearEquiv_single : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N) (s : S) (m : M),
  (AddMonoidAlgebra.mapDomainLinearEquiv R S e) (AddMonoidAlgebra.single m s) = AddMonoidAlgebra.single (e m) s
-- Std.Sync.Broadcast
/-- Subscribes a new `Receiver` in the `Bounded` channel.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.trySend' : {α : Type} → α → Std.AtomicT (Std.Bounded.State✝ α) BaseIO (Option ℕ)
-- Lean.Parser.Term
/-- `assert! cond` panics if `cond` evaluates to `false`.  -/
Lean.Parser.Term.assert : Lean.Parser.Parser
-- Init.WF
/-- A relation `r` is `WellFounded` if all elements of `α` are accessible within `r`.
If a relation is `WellFounded`, it does not allow for an infinite descent along the relation.

If the arguments of the recursive calls in a function definition decrease according to
a well founded relation, then the function terminates.
Well-founded relations are sometimes called _Artinian_ or said to satisfy the “descending chain condition”.
 -/
WellFounded : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
FreeAlgebra.toTensor_ι : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  FreeAlgebra.toTensor (FreeAlgebra.ι R m) = (TensorAlgebra.ι R) m
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.foldlM.match_1.splitter : {δ : Type u_4} →
  {α : Type u_1} →
    {β : Type u_2} →
      (motive : δ → Batteries.AssocList α β → Sort u_3) →
        (x : δ) →
          (x_1 : Batteries.AssocList α β) →
            ((d : δ) → motive d Batteries.AssocList.nil) →
              ((d : δ) →
                  (a : α) → (b : β) → (es : Batteries.AssocList α β) → motive d (Batteries.AssocList.cons a b es)) →
                motive x x_1
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_of : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) [inst_2 : DecidableEq ι] (i : ι) (x : α i),
  (DirectSum.map f) ((DirectSum.of α i) x) = (DirectSum.of β i) ((f i) x)
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instInhabitedRingMode.default : Mathlib.Tactic.RingNF.RingMode
-- Mathlib.Analysis.Convex.EGauge
egauge_zero_right : ∀ (𝕜 : Type u_1) [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, s.Nonempty → egauge 𝕜 s 0 = 0
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.mapToSelf.injEq : ∀ {α : Type u} (xs : List ((_ : α) × α)) (a : (List.map Sigma.fst xs).Perm (List.map Sigma.snd xs))
  (a_1 : (List.map Sigma.snd xs).Nodup) (xs_1 : List ((_ : α) × α))
  (a_2 : (List.map Sigma.fst xs_1).Perm (List.map Sigma.snd xs_1)) (a_3 : (List.map Sigma.snd xs_1).Nodup),
  (Plausible.InjectiveFunction.mapToSelf xs a a_1 = Plausible.InjectiveFunction.mapToSelf xs_1 a_2 a_3) = (xs = xs_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Copy of a sub_mul_action with a new `carrier` equal to the old one.
Useful to fix definitional equalities.  -/
SubAddAction.copy : {R : Type u} → {M : Type v} → [inst : VAdd R M] → (p : SubAddAction R M) → (s : Set M) → s = ↑p → SubAddAction R M
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.isEmpty : Lean.Meta.Grind.ParentSet → Bool
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.sub.eq_def : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) (x x_1 : Mathlib.Tactic.Module.qNF R M),
  Mathlib.Tactic.Module.qNF.sub iR x x_1 =
    match x, x_1 with
    | [], l => l.onScalar q(Neg.neg)
    | l, [] => l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ < k₂ then ((a₁, x₁), k₁) ::ᵣ Mathlib.Tactic.Module.qNF.sub iR t₁ (((a₂, x₂), k₂) ::ᵣ t₂)
      else
        if k₁ = k₂ then ((q(«$a₁» - «$a₂»), x₁), k₁) ::ᵣ Mathlib.Tactic.Module.qNF.sub iR t₁ t₂
        else ((q(-«$a₂»), x₂), k₂) ::ᵣ Mathlib.Tactic.Module.qNF.sub iR (((a₁, x₁), k₁) ::ᵣ t₁) t₂
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.cast.congr_simp : ∀ {s t : String.Slice} (hst : s.copy = t.copy) (a a_1 : String.Slice.Pattern.SearchStep s),
  a = a_1 → String.Slice.Pattern.SearchStep.cast hst a = String.Slice.Pattern.SearchStep.cast hst a_1
-- Lean.Elab.MutualInductive
/-- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration,
and `numParams` is `numVars` + number of explicit parameters provided in the declaration.  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.replaceIndFVarsWithConsts : Array Lean.Elab.Command.InductiveView →
  Array Lean.Expr →
    List Lean.Name →
      ℕ → ℕ → List Lean.InductiveType → optParam Bool true → Lean.Elab.TermElabM (List Lean.InductiveType)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Add.sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], MeasureTheory.SigmaFinite (μ + ν)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.semilatticeSup : {E : Type u_3} → [inst : AddGroup E] → SemilatticeSup (AddGroupSeminorm E)
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.coe_addRight : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : SeparatelyContinuousAdd X] (x : X),
  ⇑(ContinuousMap.addRight x) = fun y => y + x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g : ι → E → 𝕜} {s : Finset ι},
  (∀ i ∈ s, Function.HasTemperateGrowth (g i)) →
    (SchwartzMap.smulLeftCLM F fun x => ∑ i ∈ s, g i x) = ∑ i ∈ s, SchwartzMap.smulLeftCLM F (g i)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_map_continuousLinearMap : ∀ {μ : ℝ} {v : NNReal} (L : ℝ →L[ℝ] ℝ),
  MeasureTheory.Measure.map (⇑L) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)
-- Mathlib.MeasureTheory.Group.ModularCharacter
/-- The additive modular character as a map is `g ↦ μ (· - g) / μ`, where `μ` is an
left additive Haar measure.  -/
MeasureTheory.Measure.addModularCharacterFun : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → [LocallyCompactSpace G] → G → NNReal
-- Lean.Data.Position
Lean.Position.mk.sizeOf_spec : ∀ (line column : ℕ), sizeOf { line := line, column := column } = 1 + sizeOf line + sizeOf column
-- Init.Sym.Simp.SimprocDSL
Lean.Parser.Sym.Simp.sym_simproc.quot : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast_decl_eq : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig) (idx : ℕ)
  (h1 : idx < aig.decls.size) (h2 : idx < (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig.decls.size),
  (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig.decls[idx] = aig.decls[idx]
-- Init.Data.SInt.Lemmas
Int32.ofIntClamp_toInt : ∀ (x : Int32), Int32.ofIntClamp x.toInt = x
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mk_coe : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] (f : IncidenceAlgebra 𝕜 α)
  (h : ∀ ⦃a b : α⦄, ¬a ≤ b → f a b = 0), { toFun := ⇑f, eq_zero_of_not_le' := h } = f
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_eq_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {f : M →ₗ[R] M'}
  [inst_5 : IsLocalizedModule S f] {m : M} {s : ↥S} {m' : M'}, IsLocalizedModule.mk' f m s = m' ↔ f m = s • m'
-- Init.Data.Nat.Basic
Nat.lt_pred_of_succ_lt : ∀ {n m : ℕ}, n.succ < m → n < m.pred
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aeval_comp_val_eq : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T],
  MvPolynomial.aeval (Q.comp P.toGenerators).val =
    (MvPolynomial.aevalTower (IsScalarTower.toAlgHom R S T) Q.val).comp (Algebra.Presentation.aux✝ Q P)
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The associator in the localized monoidal category `LocalizedMonoidal L W ε`.  -/
CategoryTheory.Localization.Monoidal.associator : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.bifunctorComp₁₂ (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε)
                          (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε) ≅
                        CategoryTheory.bifunctorComp₂₃ (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε)
                          (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The continuous linear map from `realSpace K` to `mixedSpace K` which is the identity at real
places and the natural map `ℝ → ℂ` at complex places.
 -/
NumberField.mixedEmbedding.mixedSpaceOfRealSpace : {K : Type u_1} → [inst : Field K] → NumberField.mixedEmbedding.realSpace K →L[ℝ] NumberField.mixedEmbedding.mixedSpace K
-- Std.Time.Duration
Std.Time.Duration.ext_iff : ∀ {x y : Std.Time.Duration}, x = y ↔ x.second = y.second ∧ x.nano = y.nano
-- Mathlib.Data.Multiset.AddSub
Multiset.add_right_inj : ∀ {α : Type u_1} {s t u : Multiset α}, s + t = s + u ↔ t = u
-- Mathlib.FieldTheory.Minpoly.Field
/-- Given field extensions `E/F` and `K/F`, with `E/F` finite, there are finitely many `F`-algebra
homomorphisms `E →ₐ[K] K`.  -/
minpoly.AlgHom.fintype : (F : Type u_3) →
  (E : Type u_4) →
    (K : Type u_5) →
      [inst : Field F] →
        [inst_1 : Ring E] →
          [inst_2 : CommRing K] →
            [IsDomain K] →
              [inst_4 : Algebra F E] → [inst_5 : Algebra F K] → [FiniteDimensional F E] → Fintype (E →ₐ[F] K)
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.parity_simps_proc : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.integrate.congr_simp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ φ_1 : A →* B}
  (e_φ : φ = φ_1) {ψ ψ_1 : B →* C} (e_ψ : ψ = ψ_1) (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A]
  [inst_7 : IsTopologicalGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A]
  (μA μA_1 : MeasureTheory.Measure A) (e_μA : μA = μA_1) [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalGroup C] [inst_13 : LocallyCompactSpace B] [inst_14 : MeasurableSpace C]
  [inst_15 : BorelSpace C] (μC μC_1 : MeasureTheory.Measure C) (e_μC : μC = μC_1) [hμC : μC.IsHaarMeasure],
  H.integrate μA μC = ⋯.integrate μA_1 μC_1
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_univ : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α], MulAction.stabilizer G Set.univ = ⊤
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s → ∀ (m k : ℕ), iteratedDerivWithin k (fun x => x ^ m) s x = ↑(m.descFactorial k) * x ^ (m - k)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.Const.toArray_eq_toArray_map_toListModel : ∀ {α : Type u} {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  Std.DHashMap.Raw.Const.toArray m =
    (List.map
        (fun x =>
          match x with
          | ⟨k, v⟩ => (k, v))
        (Std.DHashMap.Internal.toListModel m.buckets)).toArray
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq : ∀ (z : UpperHalfPlane),
  Filter.Tendsto (fun N => ∑ n ∈ Finset.Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)))
    Filter.atTop (nhds (-2 * ↑Real.pi * Complex.I / ↑z))
-- Mathlib.Order.Disjointed
disjoint_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α), Pairwise (Function.onFun Disjoint (disjointed f))
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.mem_pin : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q → x ∈ pinGroup Q
-- Mathlib.Data.List.Chain
List.isChain_eq_iff_eq_replicate : ∀ {α : Type u_1} {l : List α}, List.IsChain (fun x1 x2 => x1 = x2) l ↔ ∀ a ∈ l.head?, l = List.replicate l.length a
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Presentation.tensor_R : ∀ {A : Type u} [inst : CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module A M₁] [inst_4 : Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂),
  (pres₁.tensor pres₂).R = (pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R)
-- Lean.Log
/-- Log the message `msgData` at the position provided by `ref` with the given `severity`.
If `getRef` has position information but `ref` does not, we use `getRef`.
We use the `fileMap` to find the line and column numbers for the error message.
 -/
Lean.logAt : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] →
        [Lean.MonadOptions m] →
          Lean.Syntax →
            Lean.MessageData → optParam Lean.MessageSeverity Lean.MessageSeverity.error → optParam Bool false → m Unit
-- Std.Tactic.Do.Syntax
/-- `mframe` infers which hypotheses from the stateful context can be moved into the pure context.
This is useful because pure hypotheses "survive" the next application of modus ponens
(`Std.Do.SPred.mp`) and transitivity (`Std.Do.SPred.entails.trans`).

It is used as part of the `mspec` tactic.

```lean
example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
  mintro _
  mframe
  /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/
  mcases h with hP
  mexact h
```
 -/
Lean.Parser.Tactic.mframe : Lean.ParserDescr
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.switch : Lean.Meta.Match.Extension.State → Lean.Meta.Match.Extension.State
-- Init.Data.Int.DivMod.Bootstrap
Int.neg_dvd : ∀ {a b : ℤ}, -a ∣ b ↔ a ∣ b
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- The trace in a quadratic algebra, as an `R`-linear map.  -/
QuadraticAlgebra.trace : {R : Type u_2} → {a b : R} → [inst : CommRing R] → QuadraticAlgebra R a b →ₗ[R] R
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.mem_ker_truncate : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R),
  x ∈ RingHom.ker (WittVector.truncate n) ↔ ∀ i < n, x.coeff i = 0
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSets_iff : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (s1 s2 : Set (Set Ω)),
  (∀ s ∈ s1, MeasurableSet s) →
    (∀ s ∈ s2, MeasurableSet s) →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ ↔
          ∀ (t1 t2 : Set Ω),
            t1 ∈ s1 →
              t2 ∈ s2 →
                μ[(t1 ∩ t2).indicator fun ω => 1 | m'] =ᵐ[μ]
                  μ[t1.indicator fun ω => 1 | m'] * μ[t2.indicator fun ω => 1 | m']
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive commutative monoid with multiplication, a finite sum of sums of squares
is a sum of squares.
 -/
IsSumSq.sum : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R] {ι : Type u_2} {I : Finset ι} {s : ι → R},
  (∀ i ∈ I, IsSumSq (s i)) → IsSumSq (∑ i ∈ I, s i)
-- Init.Data.String.Length
List.length_asString : ∀ {l : List Char}, (String.ofList l).length = l.length
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), p.radius = ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_pairwiseDisjoint_range_vadd`. -/
AddAction.IsBlock.pairwiseDisjoint_range_vadd : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X},
  AddAction.IsBlock G B → (Set.range fun g => g +ᵥ B).PairwiseDisjoint id
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_sdiff_Ioc_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → Set.Icc b a \ Set.Ioc b a = {b}
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongrLinearEquiv'_symm_apply : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂] {ι' : Type u_1}
  (σ : ι ≃ ι') (f : MultilinearMap R (fun i => M₁ (σ.symm i)) M₂),
  (MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ).symm f =
    { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.Tactic.Push
Mathlib.Tactic.Push.not_iff : ∀ (p q : Prop), ¬(p ↔ q) ↔ p ∧ ¬q ∨ ¬p ∧ q
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted.
This is an abbreviation for `SimpleGraph.Walk.toDeleteEdges`.  -/
SimpleGraph.Walk.toDeleteEdge : {V : Type u} →
  {G : SimpleGraph V} → {v w : V} → (e : Sym2 V) → (p : G.Walk v w) → e ∉ p.edges → (G.deleteEdges {e}).Walk v w
-- Mathlib.Data.List.GetD
/-- An empty list can always be decidably checked for the presence of an element.
Not an instance because it would clash with `DecidableEq α`.  -/
List.decidableGetDNilNe : {α : Type u} → (a : α) → DecidablePred fun i => [].getD i a ≠ a