mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.mk.injEq : ∀ {α : Type u} (toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α)
  (ord :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this := toPreorderOfLEArgs.decidableLE;
      Ord α)
      Std.Packages.LinearPreorderOfLEArgs.ord._autoParam)
  (le_total : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam)
  (isLE_compare :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this_1 := toPreorderOfLEArgs.decidableLE;
      let this_2 := ord;
      ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
      Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam)
  (isGE_compare :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this_1 := toPreorderOfLEArgs.decidableLE;
      have this_2 := le_total;
      let this_3 := ord;
      ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
      Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam)
  (toPreorderOfLEArgs_1 : Std.Packages.PreorderOfLEArgs α)
  (ord_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      let this := toPreorderOfLEArgs_1.decidableLE;
      Ord α)
      Std.Packages.LinearPreorderOfLEArgs.ord._autoParam)
  (le_total_1 : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam)
  (isLE_compare_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      let this_1 := toPreorderOfLEArgs_1.decidableLE;
      let this_2 := ord_1;
      ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
      Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam)
  (isGE_compare_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      let this_1 := toPreorderOfLEArgs_1.decidableLE;
      have this_2 := le_total_1;
      let this_3 := ord_1;
      ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
      Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam),
  ({ toPreorderOfLEArgs := toPreorderOfLEArgs, ord := ord, le_total := le_total, isLE_compare := isLE_compare,
        isGE_compare := isGE_compare } =
      { toPreorderOfLEArgs := toPreorderOfLEArgs_1, ord := ord_1, le_total := le_total_1,
        isLE_compare := isLE_compare_1, isGE_compare := isGE_compare_1 }) =
    (toPreorderOfLEArgs = toPreorderOfLEArgs_1 ∧ ord = ord_1)
-- Mathlib.Topology.Separation.Regular
/-- A topological space is called a *regular space* if for any closed set `s` and `a ∉ s`, there
exist disjoint open sets `U ⊇ s` and `V ∋ a`. We formulate this condition in terms of `Disjoint`ness
of filters `𝓝ˢ s` and `𝓝 a`.  -/
RegularSpace : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.rightUnitor_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).hom.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
-- Mathlib.Order.Monotone.Defs
Subtype.strictMono_coe : ∀ {α : Type u} [inst : Preorder α] (p : α → Prop), StrictMono Subtype.val
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mul_eq_smul : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ R β), s.mul t = s.smul t
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.comp_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {Z : C}, CategoryTheory.CategoryStruct.comp f 0 = 0
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.IsTopCompl.mk : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (isCompl : IsCompl p q),
  Continuous ⇑(p.projection q isCompl) → Submodule.IsTopCompl p q
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmoothOfRelativeDimension_holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmoothOfRelativeDimension 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X A B Y : C} (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (CategoryTheory.Over.pullback f)
            (CategoryTheory.Over.mk gA) (CategoryTheory.Over.mk gB)).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst gA gB) gA) f)
        (CategoryTheory.Limits.pullback.fst gA gB)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd gA f)
        (CategoryTheory.Limits.pullback.snd gB f))
      (CategoryTheory.Limits.pullback.fst gA f)
-- Mathlib.Topology.Separation.Basic
Pi.instT0Space : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T0Space (X i)],
  T0Space ((i : ι) → X i)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- A comonad in a bicategory `B` is a 1-morphism `t : a ⟶ a` together with 2-morphisms
`Δ : t ⟶ t ≫ t` and `ε : t ⟶ 𝟙 a` satisfying the comonad laws.  -/
CategoryTheory.Bicategory.Comonad : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a : B} → (a ⟶ a) → Type w
-- Mathlib.Data.PNat.Factors
instInhabitedPrimeMultiset : Inhabited PrimeMultiset
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.encoding_decode : ∀ {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.encoding.decode l = (FirstOrder.Language.BoundedFormula.listDecode l)[0]?
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instDecidableEqOffset : DecidableEq Std.Time.Minute.Offset
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
DistribMulActionHom.comp.congr_simp : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {P : Type u_3} [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : M →* P} {A : Type u_4} [inst_3 : AddMonoid A] [inst_4 : DistribMulAction M A] {B : Type u_5}
  [inst_5 : AddMonoid B] [inst_6 : DistribMulAction N B] {C : Type u_7} [inst_7 : AddMonoid C]
  [inst_8 : DistribMulAction P C] [κ : φ.CompTriple ψ χ] (g g_1 : B →ₑ+[ψ] C),
  g = g_1 → ∀ (f f_1 : A →ₑ+[φ] B), f = f_1 → g.comp f = g_1.comp f_1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal : ∀ {R : Type u} [inst : CommSemiring R] (Z : Set (PrimeSpectrum R)),
  IsClosed Z ↔ ∃ I, I.IsRadical ∧ Z = PrimeSpectrum.zeroLocus ↑I
-- Mathlib.Topology.Order.LeftRight
continuousWithinAt_inter_Ioi_iff_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β} {s : Set α}, ContinuousWithinAt f (s ∩ Set.Ioi a) a ↔ ContinuousWithinAt f (s ∩ Set.Ici a) a
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zero_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R] (z : ℤ),
  z ≠ 0 → 0 ^ z = 0
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.integral_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β},
      MeasurableSet s → ∫ (x : γ), κ.densityProcess ν n a x s ∂ν a = (κ a).real (Set.univ ×ˢ s)
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsIntegral.comap_lt_comap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] {I J : Ideal A} [I.IsPrime],
  I < J → Ideal.comap (algebraMap R A) I < Ideal.comap (algebraMap R A) J
-- Mathlib.Data.Nat.Log
Nat.clog.go_spec : ∀ {n b fuel : ℕ},
  1 < n →
    1 < b →
      n < b ^ fuel →
        (Nat.clog.go n b fuel).1 = b ^ ((Nat.clog.go n b fuel).2 + 1) / n ∧
          b ^ (Nat.clog.go n b fuel).2 < n ∧ n ≤ b ^ ((Nat.clog.go n b fuel).2 + 1)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C).comp
          (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C) ≅
        CategoryTheory.Functor.id (CategoryTheory.AddMon C)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.sub_section : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M},
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) u →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (s - t) x⟩) u
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.isIso_toSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P : CategoryTheory.Functor Cᵒᵖ D},
  CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.IsIso (J.toSheafify P)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.mk.sizeOf_spec : ∀ (carrier : Type u) [str : Semigroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.instInhabited : Inhabited Semigrp
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.comul_mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal] (a : A),
  CoalgebraStruct.comul ((Ideal.Quotient.mk I) a) =
    (TensorProduct.map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap)
      (CoalgebraStruct.comul a)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- An orthonormal basis on E is an identification of `E` with its dimensional-matching
`EuclideanSpace 𝕜 ι`.  -/
OrthonormalBasis : (ι : Type u_1) →
  (𝕜 : Type u_3) →
    [inst : RCLike 𝕜] →
      (E : Type u_4) →
        [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → [Fintype ι] → Type (max (max u_1 u_3) u_4)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R],
  ⌊0⌋₊ = 0
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.ext_iff : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI hI' : DividedPowers I},
  hI = hI' ↔ ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.tendsto_measure_Ico_atTop : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : Preorder α] [NoMaxOrder α] [Filter.atTop.IsCountablyGenerated]
  (μ : MeasureTheory.Measure α) (a : α), Filter.Tendsto (fun x => μ (Set.Ico a x)) Filter.atTop (nhds (μ (Set.Ici a)))
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.extendWith_zero : ∀ {ι : Type u} {α : Option ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : Option ι) → Zero (α i)] (x : α none),
  DFinsupp.extendWith x 0 = fun₀ | none => x
-- Batteries.Linter.UnreachableTactic
/-- A list of blacklisted syntax kinds, which are expected to have subterms that contain
unevaluated tactics.
 -/
Batteries.Linter.UnreachableTactic.ignoreTacticKindsRef : IO.Ref Lean.NameHashSet
-- Mathlib.RingTheory.Jacobson.Ideal
/-- The standard radical and Jacobson radical of an ideal `I` of `R` are equal if and only if
the nilradical and Jacobson radical of the quotient ring `R/I` coincide  -/
Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The lemma  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma.name : Mathlib.Tactic.ClickSuggestions.ApplyAtLemma → Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A}
  {f g : Φ.presheafFiber.obj P ⟶ T},
  (∀ (X : C) (x : Φ.fiber.obj X),
      CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) f =
        CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) g) →
    f = g
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
RingEquiv.mapTwoSidedIdeal_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (e : R ≃+* S)
  (I : TwoSidedIdeal R), e.mapTwoSidedIdeal I = (TwoSidedIdeal.comap e.symm) I
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_eq_head_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.minKey he = t.keys.head ⋯
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCyclesIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j j_1 : ι) (e_j : j = j_1) (hj : c.next i = j)
  (h : K.d i j = 0) [inst_2 : K.HasHomology i], K.iCyclesIso i j hj h = K.iCyclesIso i j_1 ⋯ ⋯
-- Mathlib.Geometry.Manifold.Sheaf.Basic
StructureGroupoid.LocalInvariantProp.section_spec : ∀ {H : Type u_1} [inst : TopologicalSpace H] {H' : Type u_2} [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [inst_2 : TopologicalSpace M]
  [inst_3 : ChartedSpace H M] (M' : Type u) [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M']
  (hG : G.LocalInvariantProp G' P) (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
  (f : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).obj.obj U), ChartedSpace.LiftProp P ↑f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
/-- Given a presheaf of types `F : Cᵒᵖ ⥤ Type u`, this is the presheaf
of modules over `R` which sends `X : Cᵒᵖ` to the free `R.obj X`-module on `F.obj X`.  -/
PresheafOfModules.freeObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → CategoryTheory.Functor Cᵒᵖ (Type u) → PresheafOfModules R
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β) (sz : ℕ) (k' : α) (v' : β)
  (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) (hl_2 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.Const.alter k f (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hl_2 =
    match compare k k' with
    | Ordering.lt =>
      match Std.DTreeMap.Internal.Impl.Const.alter k f l' ⋯ with
      | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balance k' v' d r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.gt =>
      match Std.DTreeMap.Internal.Impl.Const.alter k f r' ⋯ with
      | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balance k' v' l' d ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.eq =>
      match f (some v') with
      | none => { impl := l'.glue r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
      | some v =>
        { impl := Std.DTreeMap.Internal.Impl.inner sz k v l' r', balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
-- Mathlib.Data.Finset.Lattice.Prod
Finset.sup_product_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f (i, i')
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.apply : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a })
  (a : ε), (ep.subtypeCongr en) a = if h : p a then ↑(ep ⟨a, h⟩) else ↑(en ⟨a, h⟩)
-- Mathlib.Order.Cover
covBy_iff_Ioo_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b ↔ a < b ∧ Set.Ioo a b = ∅
-- Lean.Data.JsonRpc
Lean.JsonRpc.instDecidableLtRequestID : (a b : Lean.JsonRpc.RequestID) → Decidable (a < b)
-- Mathlib.Analysis.Real.OfDigits
Real.summable_ofDigitsTerm : ∀ {b : ℕ} {digits : ℕ → Fin b}, Summable (Real.ofDigitsTerm digits)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.domCongrBialgEquiv.eq_1 : ∀ (R : Type u_1) (A : Type u_3) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N),
  MonoidAlgebra.domCongrBialgEquiv R A e = BialgEquiv.ofAlgEquiv (MonoidAlgebra.domCongr R A e) ⋯ ⋯
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.lift_unique : ∀ {V : Type u} [inst : Quiver V] {V' : Type u'} [inst_1 : CategoryTheory.Groupoid V'] (φ : V ⥤q V')
  (Φ : CategoryTheory.Functor (Quiver.FreeGroupoid V) V'),
  Quiver.FreeGroupoid.of V ⋙q Φ.toPrefunctor = φ → Φ = Quiver.FreeGroupoid.lift φ
-- Init.Data.SInt.Bitwise
Int64.neg_one_xor : ∀ {a : Int64}, -1 ^^^ a = ~~~a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a fallback : α},
  (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumComm_apply : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (a : V ⊕ W), SimpleGraph.Iso.sumComm a = a.swap
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toExtensionHom.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f f_1 : P.Hom P'), f = f_1 → f.toExtensionHom = f_1.toExtensionHom
-- Lean.Meta.Tactic.Grind.Core
/-- Reinserts parents into the congruence table and detect new equalities.
This is an auxiliary function performed while merging equivalence classes.
 -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.reinsertParents : Lean.Meta.Grind.ParentSet → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_union_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s \ t ∪ s ∩ t = s
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.union₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} (h₁ : m₁.WF)
  (h₂ : m₂.WF), (↑(Std.DHashMap.Internal.Raw₀.union ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩)).WF
-- Mathlib.Order.CompleteLattice.Basic
Antitone.sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : CompleteLattice β] {s : Set (α → β)},
  (∀ f ∈ s, Antitone f) → Antitone (sSup s)
-- Mathlib.Data.FunLike.IsApply
/-- `IsNegApply F α β` states for all `f : F` and `x : α`, `(-f) x = -f x`.  -/
IsNegApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Neg β] → [Neg F] → Prop
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- The space of continuous linear maps equipped with the topology of pointwise convergence,
sometimes also called the *strong operator topology*. We avoid this terminology since so many other
things share similar names, and using "pointwise convergence" in the name is more informative.

This topology is also known as the weak⋆-topology in the case that `σ = RingHom.id 𝕜` and `F = 𝕜`  -/
«term_→Lₚₜ[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesLimitPair.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G],
  CategoryTheory.Limits.PreservesLimitPair.iso G X Y = CategoryTheory.Limits.PreservesLimitPair.iso G X Y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_union_le_size_add_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Std.Http.Data.Headers.Name
/-- Creates a `Name` from a string, panicking with an error message if the string contains invalid
characters for HTTP header names or is empty.
 -/
Std.Http.Header.Name.ofString! : String → Std.Http.Header.Name
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.coe_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {M : Type u_7}
  [inst_6 : Monoid M] [inst_7 : DistribMulAction M F] [inst_8 : SMulCommClass S M F] (a : M) (f : E →ₛₗ.[σ] F),
  ↑(a • f) = a • ↑f
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The inf of two subrings is their intersection.  -/
Subring.instMin : {R : Type u} → [inst : NonAssocRing R] → Min (Subring R)
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instWithBotOfOrderTopology.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  TopologicalSpace.instWithBotOfOrderTopology = Preorder.topology (WithBot ι)