mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Parsec.ByteArray
/-- Parse zero or more ASCII digits into a `Nat`, continuing until non-digit or EOF.
 -/
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.digitsCore : ℕ → Std.Internal.Parsec.ByteArray.Parser ℕ
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forM.loop.eq_def : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (range : Std.Legacy.Range) (f : ℕ → m PUnit.{u_1 + 1}) (i : ℕ),
  Std.Legacy.Range.forM.loop✝ range f i =
    if i < range.stop then do
      f i
      have this : 0 < range.step := ⋯
      Std.Legacy.Range.forM.loop✝ range f (i + range.step)
    else pure PUnit.unit
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (X : F.Grothendieck),
  (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base
-- Init.Data.UInt.Bitwise
Bool.toUInt8.eq_1 : ∀ (b : Bool), b.toUInt8 = if b = true then 1 else 0
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the forward direction of `spectrum.algebraMap_mem_iff`. -/
spectrum.of_algebraMap_mem : ∀ (S : Type u_1) {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : A} {r : R},
  (algebraMap R S) r ∈ spectrum S a → r ∈ spectrum R a
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotation_swap' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ (o.rightAngleRotation x) y = -inner ℝ x (o.rightAngleRotation y)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.mem_iff_mem_rcc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxc.IsAlwaysFinite α] {a : α},
  a ∈ r ↔ a ∈ Std.PRange.UpwardEnumerable.least...=r.upper
-- Aesop.Tree.RunMetaM
Aesop.Goal.runMetaMInParentState' : {m : Type → Type} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Goal → m α
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.map_matrix : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J K : Type}
  [inst_2 : Finite J] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] [inst_4 : Finite K] {f g : J → C}
  {h : K → C} (m : (k : J) → f k ⟶ g k) (n : (j : J) → (k : K) → g j ⟶ h k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map m)
      (CategoryTheory.Limits.biproduct.matrix n) =
    CategoryTheory.Limits.biproduct.matrix fun j k => CategoryTheory.CategoryStruct.comp (m j) (n j k)
-- Mathlib.Logic.Equiv.PartialEquiv
/-- **Alias** of `PartialEquiv.image_source_subset`.

---

Variant of `e.map_source` and `map_source'`, stated for images of subsets of `source`.  -/
PartialEquiv.map_source'' : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), ↑e '' e.source ⊆ e.target
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Cfg.mk.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (l : Option Λ) (var : σ) (stk : (k : K) → List (Γ k))
  (l_1 : Option Λ) (var_1 : σ) (stk_1 : (k : K) → List (Γ k)),
  ({ l := l, var := var, stk := stk } = { l := l_1, var := var_1, stk := stk_1 }) =
    (l = l_1 ∧ var = var_1 ∧ stk = stk_1)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.trivial_ρ : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {V : Type w} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (g : G), (Rep.trivial k G V).ρ g = LinearMap.id
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_id' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasDerivAt (fun x => x) 1 x
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The completed L-function of a function `ZMod N → ℂ` is differentiable, with the following
exceptions: at `s = 1` if `∑ j, Φ j ≠ 0`; and at `s = 0` if `Φ 0 ≠ 0`.
 -/
ZMod.differentiableAt_completedLFunction : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ),
  s ≠ 0 ∨ Φ 0 = 0 → s ≠ 1 ∨ ∑ j, Φ j = 0 → DifferentiableAt ℂ (ZMod.completedLFunction Φ) s
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.Equicontinuous.closure` for a more familiar statement.  -/
Equicontinuous.closure' : ∀ {X : Type u_3} {Y : Type u_5} {α : Type u_6} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [uα : UniformSpace α]
  {A : Set Y} {u : Y → X → α}, Equicontinuous (u ∘ Subtype.val) → Continuous u → Equicontinuous (u ∘ Subtype.val)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerLevelMVarErrorInfo : Lean.Elab.Term.LevelMVarErrorInfo → Lean.Elab.TermElabM Unit
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeffNth.eq_1 : ∀ {R : Type u} [inst : Semiring R] (I : Ideal (Polynomial R)) (n : ℕ),
  I.leadingCoeffNth n = Submodule.map (Polynomial.lcoeff R n) (I.degreeLE ↑n)
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.Functor.Elements.hasInitial_iff_isCorepresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  CategoryTheory.Limits.HasInitial F.Elements ↔ F.IsCorepresentable
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_max_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp k (t.max ⋯)).isLE = true
-- Lean.Elab.MutualInductive
/-- Initializes the elaborator associated to the given syntax.
 -/
Lean.Elab.Command.mkInductiveView : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1
-- Init.System.IO
/-- Creates a temporary directory in the most secure manner possible, returning the new directory's
path. There are no race conditions in the directory’s creation. The directory is readable and
writable only by the creating user ID.

It is the caller's job to remove the directory after use. Use `withTempDir` to ensure that the
temporary directory is removed.
 -/
IO.FS.createTempDir : IO System.FilePath
-- Mathlib.Order.Partition.Equipartition
Finpartition.bot_isEquipartition : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), ⊥.IsEquipartition
-- Lean.Attributes
Lean.ParametricAttribute.attr : {α : Type} → Lean.ParametricAttribute α → Lean.AttributeImpl
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.hI : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (self : CategoryTheory.Limits.IndObjectPresentation A), CategoryTheory.IsFiltered self.I
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U)
  (V : TopCat.Presheaf.SheafCondition.OpensLeCover U),
  ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).obj V).obj.right.as = PUnit.unit
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.bialgHom_ext_iff : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] [inst_5 : AddMonoid M]
  {φ₁ φ₂ : AddMonoidAlgebra A M →ₐc[R] B},
  φ₁ = φ₂ ↔
    (∀ (m : M), φ₁ (AddMonoidAlgebra.single m 1) = φ₂ (AddMonoidAlgebra.single m 1)) ∧
      (↑φ₁).comp AddMonoidAlgebra.singleZeroAlgHom = (↑φ₂).comp AddMonoidAlgebra.singleZeroAlgHom
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.symm_neg : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : ContinuousNeg G],
  (Homeomorph.neg G).symm = Homeomorph.neg G
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonJson : Lean.ToJson Lean.Json
-- Init.Data.BitVec.Lemmas
BitVec.not_cons : ∀ {w : ℕ} (x : BitVec w) (b : Bool), ~~~BitVec.cons b x = BitVec.cons (!b) (~~~x)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.Internal.memcmpSlice : (lhs rhs : String.Slice) →
  (lstart rstart len : String.Pos.Raw) →
    len.offsetBy lstart ≤ lhs.rawEndPos → len.offsetBy rstart ≤ rhs.rawEndPos → Bool
-- Mathlib.Algebra.Ring.Action.Basic
/-- The tautological action by `R →+* R` on `R`.

This generalizes `Function.End.applyMulAction`.  -/
RingHom.applyMulSemiringAction : (R : Type v) → [inst : Semiring R] → MulSemiringAction (R →+* R) R
-- Std.Time.Format.Basic
/-- Configuration options for formatting behavior.
 -/
Std.Time.GenericFormat.config : {awareness : Std.Time.Awareness} → Std.Time.GenericFormat awareness → Std.Time.FormatConfig
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- The categorical equivalence between the category of matrices over a ring,
and the category of matrices over that ring considered as a single-object category.  -/
CategoryTheory.Mat.equivalenceSingleObj : (R : Type) → [inst : Ring R] → CategoryTheory.Mat R ≌ CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instHasDistribNeg : {𝕜 : Type u_1} → [inst : NonUnitalSeminormedRing 𝕜] → HasDistribNeg ↑(Metric.closedBall 0 1)
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.add_const : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {γ : Type u_7} {f : E → γ} [inst_4 : AddCommMonoid γ] [inst_5 : PartialOrder γ]
  [IsOrderedCancelAddMonoid γ] [inst_7 : Module 𝕜 γ],
  StrictConvexOn 𝕜 s f → ∀ (b : γ), StrictConvexOn 𝕜 s (f + fun x => b)
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.dNext_zero_chainComplex : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (f : (i j : ℕ) → P.X i ⟶ Q.X j), (dNext 0) f = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K} [IsGalois k K],
  NumberField.InfinitePlace.IsUnramified k w ↔ MulAction.stabilizer Gal(K/k) w = ⊥
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.Abelian.epi_kernel_map_of_isPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C}
  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (sq : CategoryTheory.IsPushout t l r b),
  CategoryTheory.Epi (CategoryTheory.Limits.kernel.map t b l r ⋯)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.instZLattice_unitLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], IsZLattice ℝ (NumberField.Units.unitLattice K)
-- Lean.Server.AsyncList
Lean.AsyncList.cons : {ε : Type u} → {α : Type v} → α → Lean.AsyncList ε α → Lean.AsyncList ε α
-- Mathlib.Topology.Order.WithTop
/-- If `ι` has a bot element, then `WithBot ι` is homeomorphic to `ι ⊕ Unit`.  -/
WithBot.sumHomeomorph : (ι : Type u_1) →
  [inst : LinearOrder ι] →
    [inst_1 : TopologicalSpace ι] → [inst_2 : OrderTopology ι] → [OrderBot ι] → WithBot ι ≃ₜ ι ⊕ Unit
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities.moduleHierarchyProvider? : Lean.Lsp.LeanServerCapabilities → Option Lean.Lsp.ModuleHierarchyOptions
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.modEq_iff_toIcoMod_eq_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] ↔ toIcoMod hp a b = a
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_map : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff n) ((PowerSeries.map f) φ) = f ((PowerSeries.coeff n) φ)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instZeroHom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → Zero (A ⟶ B)
-- Init.Data.List.ToArray
/-- Variant of `foldl_toArray` with a side condition for the `stop` argument.  -/
List.foldl_toArray' : ∀ {β : Type u_1} {α : Type u_2} {stop : ℕ} (f : β → α → β) (init : β) (l : List α),
  stop = l.toArray.size → Array.foldl f init l.toArray 0 stop = List.foldl f init l
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The 2-isomorphism `normalizeIso p f` is natural in `f`.  -/
CategoryTheory.FreeBicategory.normalize_naturality : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c}
  (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) η)
      (CategoryTheory.FreeBicategory.normalizeIso p g).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.normalizeIso p f).hom
      ((CategoryTheory.FreeBicategory.preinclusion B).map₂ (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.inclusion.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K),
  AddSubgroup.inclusion h = AddMonoidHom.mk' (fun x => ⟨↑x, ⋯⟩) ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.mul_dvd_mul : ∀ {a b c d : ℤ}, a ∣ b → c ∣ d → a * c ∣ b * d
-- Mathlib.Logic.Function.Conjugate
/-- If `fbc : β → γ` semiconjugates `gb` to `gc` and `fab : α → β` semiconjugates `ga` to `gb`,
then `fbc ∘ fab` semiconjugates `ga` to `gc`.

See also `Function.Semiconj.trans` for a version with reversed arguments.

**Backward compatibility note:** before 2024-01-13,
this lemma used to have the same order of arguments that `Function.Semiconj.trans` has now.  -/
Function.Semiconj.comp_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {fab : α → β} {fbc : β → γ} {ga : α → α} {gb : β → β} {gc : γ → γ},
  Function.Semiconj fbc gb gc → Function.Semiconj fab ga gb → Function.Semiconj (fbc ∘ fab) ga gc
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ0.eq_1 : ∀ (R : Type u_1) [inst : CommRing R], WeierstrassCurve.ofJ0 R = { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 }
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Left.self_lt_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a : α}, a < 0 → a < -a
-- Init.Data.SInt.Basic
instPowInt8Nat : Pow Int8 ℕ
-- Mathlib.Algebra.Free
FreeSemigroup.traverse_eq : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : FreeSemigroup α),
  FreeSemigroup.traverse F x = traverse F x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C},
  CategoryTheory.Limits.coconeRightOpOfConeEquiv.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
-- Mathlib.Topology.Defs.Basic
BaireSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)) → BaireSpace X
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete and then runs the `IO` action `f` on its result.
This new task has priority `prio`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped. Because `IO` actions
may throw an exception of type `IO.Error`, the result of the task is an `Except IO.Error α`.
 -/
IO.mapTask : {α : Type u_1} →
  {β : Type} →
    (α → IO β) →
      Task α → optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task (Except IO.Error β))
-- Mathlib.Algebra.Homology.Localization
/-- The homotopy category satisfies the universal property of the localized category
with respect to homotopy equivalences.  -/
ComplexShape.strictUniversalPropertyFixedTargetQuotient : {ι : Type u_1} →
  (c : ComplexShape ι) →
    (∀ (j : ι), ∃ i, c.Rel i j) →
      (C : Type u_2) →
        [inst : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_1 : CategoryTheory.Preadditive C] →
            [CategoryTheory.Limits.HasBinaryBiproducts C] →
              (E : Type u_3) →
                [inst_3 : CategoryTheory.Category.{v_2, u_3} E] →
                  CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c)
                    (HomologicalComplex.homotopyEquivalences C c) E
-- Batteries.Data.Int
Int.testBit.eq_1 : ∀ (x m : ℕ), (Int.ofNat m).testBit x = m.testBit x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (h : t.Balanced),
  Std.DTreeMap.Internal.Impl.erase k t h =
    match t, h with
    | Std.DTreeMap.Internal.Impl.leaf, h =>
      { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l r, h =>
      match compare k k' with
      | Ordering.lt =>
        match Std.DTreeMap.Internal.Impl.erase k l ⋯ with
        | { impl := l', balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ } =>
          { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l' r ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.gt =>
        match Std.DTreeMap.Internal.Impl.erase k r ⋯ with
        | { impl := r', balanced_impl := hr'₁, lb_le_size_impl := hr'₂, size_impl_le_ub := hr'₃ } =>
          { impl := Std.DTreeMap.Internal.Impl.balanceLErase k' v' l r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
            size_impl_le_ub := ⋯ }
      | Ordering.eq => { impl := l.glue r ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.Tactic.TermCongr
/-- A request for a type of congruence lemma from a `CongrResult`.  -/
Mathlib.Tactic.TermCongr.CongrType : Type
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_midpoint_midpoint_le' : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ p₃ p₄ : P),
  dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.ext : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Π₀ (i : ι), β i}, (∀ (i : ι), f i = g i) → f = g
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Membership in a free monoid element  -/
FreeMonoid.mem : {α : Type u_1} → FreeMonoid α → α → Prop
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {β : Type u_5} [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s + t).inf f = t.inf fun y => s.inf fun x => f (x + y)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {g : γ → ENNReal},
  Measurable g → ∫⁻ (c : γ), g c ∂κ.snd a = ∫⁻ (bc : β × γ), g bc.2 ∂κ a
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryExtensive.hasPullbacksOfInclusions : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C],
  CategoryTheory.HasPullbacksOfInclusions C
-- Mathlib.Probability.Martingale.Convergence
/-- A stochastic process that frequently visits below `a` and above `b` has infinite upcrossings.  -/
MeasureTheory.upcrossings_eq_top_of_frequently_lt : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω},
  a < b →
    (∃ᶠ (n : ℕ) in Filter.atTop, f n ω < a) →
      (∃ᶠ (n : ℕ) in Filter.atTop, b < f n ω) → MeasureTheory.upcrossings a b f ω = ⊤
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.GaloisCategory.hasFiberFunctor : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.GaloisCategory C],
  ∃ F, Nonempty (CategoryTheory.PreGaloisCategory.FiberFunctor F)
-- Mathlib.Order.Partition.Finpartition
Finpartition.instOrderBotFinset : {α : Type u_1} → [inst : DecidableEq α] → (s : Finset α) → OrderBot (Finpartition s)
-- Mathlib.Topology.Algebra.InfiniteSum.Real
/-- If a sequence `f` with non-negative terms is dominated by a sequence `g` with summable
series and at least one term of `f` is strictly smaller than the corresponding term in `g`,
then the series of `f` is strictly smaller than the series of `g`.  -/
Summable.tsum_lt_tsum_of_nonneg : ∀ {i : ℕ} {f g : ℕ → ℝ},
  (∀ (b : ℕ), 0 ≤ f b) → (∀ (b : ℕ), f b ≤ g b) → f i < g i → Summable g → ∑' (n : ℕ), f n < ∑' (n : ℕ), g n
-- Mathlib.CategoryTheory.Pi.Basic
/-- `pi C` gives the Cartesian product of an indexed family of categories.
 -/
CategoryTheory.pi : {I : Type w₀} →
  (C : I → Type u₁) →
    [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → CategoryTheory.Category.{max w₀ v₁, max u₁ w₀} ((i : I) → C i)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_map : ∀ {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Stream'.WSeq α}, a ∈ s → f a ∈ Stream'.WSeq.map f s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  (Std.ExtHashMap.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = true
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {p : (_ : α) × β},
  (t₁ ∪ t₂.insert p.fst p.snd).Equiv ((t₁ ∪ t₂).insert p.fst p.snd)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.conjGL_coe : ∀ (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  CongruenceSubgroup.conjGL Γ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) =
    ConjAct.toConjAct g⁻¹ • Γ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivisionCommMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : DivisionCommMonoid Mᵐᵒᵖ], DomMulAct.instDivisionCommMonoidOfMulOpposite = inst
-- Init.Data.String.Lemmas.TakeDrop
String.dropEnd_toSlice : ∀ {s : String} {n : ℕ}, s.toSlice.dropEnd n = s.dropEnd n
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F : CategoryTheory.Functor C D} {x y : F.OplaxMonoidal},
  CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.Functor.OplaxMonoidal.η F →
    CategoryTheory.Functor.OplaxMonoidal.δ F = CategoryTheory.Functor.OplaxMonoidal.δ F → x = y
-- Mathlib.Algebra.Group.PUnit
PUnit.instDiv_mathlib : Div PUnit.{u_1 + 1}
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.addSpan.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] (s : Finset α),
  s.addSpan = Finset.image (fun ε => ∑ a ∈ s, ε a • a) (Fintype.piFinset fun _a => {-1, 0, 1})