mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.straightLineExtS.tacticBuilder : Aesop.ExtResult → Aesop.Script.TacticBuilder
-- Init.Data.UInt.Lemmas
UInt16.add_zero : ∀ (a : UInt16), a + 0 = a
-- Mathlib.Data.Set.Lattice
Set.univ_pi_eq_iInter : ∀ {α : Type u_1} {π : α → Type u_12} (t : (i : α) → Set (π i)), Set.univ.pi t = ⋂ i, Function.eval i ⁻¹' t i
-- Mathlib.Analysis.Fourier.Notation
FourierSMul.mk : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : SMul R E] [inst_1 : SMul R F]
  [inst_2 : FourierTransform E F],
  (∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f) → FourierSMul R E F
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.injective_symm_of_target_eq_univ : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.target = Set.univ → Function.Injective ↑e.symm
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.equiv_of_restrict_eq : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialMap Y) {W₁ W₂ : X.Opens} {hW₁ : Dense ↑W₁} {hW₂ : Dense ↑W₂}
  {hW₁' : W₁ ≤ f.domain} {hW₂' : W₂ ≤ g.domain}, f.restrict W₁ hW₁ hW₁' = g.restrict W₂ hW₂ hW₂' → f.equiv g
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso : ∀ {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),
  α.naturality (CategoryTheory.CategoryStruct.id a) =
    CategoryTheory.Bicategory.whiskerRightIso (F.mapId a) (α.app a) ≪≫
      CategoryTheory.Bicategory.leftUnitor (α.app a) ≪≫
        (CategoryTheory.Bicategory.rightUnitor (α.app a)).symm ≪≫
          CategoryTheory.Bicategory.whiskerLeftIso (α.app a) (G.mapId a).symm
-- Lean.Syntax
Lean.Syntax.MonadTraverser.st : {m : Type → Type} → [self : Lean.Syntax.MonadTraverser m] → MonadState Lean.Syntax.Traverser m
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- An internal transitive relation in the category of types gives rise to a standard transitive
relation.  -/
TypeCat.isTrans_of_transitiveRelation : ∀ {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.TransitiveRelation p₁ p₂), IsTrans X (TypeCat.Rel.ofPair p₁ p₂)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.mk : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {J : Type u_4} →
        [inst : Zero I₂] →
          {r : I₁ × I₂ × I₃ → J} →
            {π : I₁ × I₃ → J} →
              (p₁₂ : I₁ × I₂ → I₁) →
                (∀ (i : I₁ × I₂ × I₃), π (p₁₂ (i.1, i.2.1), i.2.2) = r i) →
                  (p₂₃ : I₂ × I₃ → I₃) →
                    (∀ (i : I₁ × I₂ × I₃), π (i.1, p₂₃ i.2) = r i) →
                      (∀ (i₁ : I₁), p₁₂ (i₁, 0) = i₁) →
                        (∀ (i₃ : I₃), p₂₃ (0, i₃) = i₃) → CategoryTheory.GradedObject.TriangleIndexData r π
-- Mathlib.Algebra.Group.End
Equiv.mulLeft_one : ∀ {α : Type u_4} [inst : Group α], Equiv.mulLeft 1 = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toArray_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  (Std.DTreeMap.Raw.Const.toList t).toArray = Std.DTreeMap.Raw.Const.toArray t
-- Mathlib.NumberTheory.FLT.Three
/-- `FermatLastTheoremForThreeGen` is the statement that `a ^ 3 + b ^ 3 = u * c ^ 3` has no
nontrivial solutions in `𝓞 K` for all `u : (𝓞 K)ˣ` such that `¬ λ ∣ a`, `¬ λ ∣ b` and `λ ∣ c`.
The reason to consider `FermatLastTheoremForThreeGen` is to make a descent argument working.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen : {K : Type u_1} → [inst : Field K] → {ζ : K} → IsPrimitiveRoot ζ 3 → Prop
-- Mathlib.Data.Nat.Log
Nat.lt_pow_of_log_lt : ∀ {b x y : ℕ}, 1 < b → Nat.log b y < x → y < b ^ x
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Function.Injective ⇑f → Function.Injective (Polynomial.map f)
-- Mathlib.ModelTheory.PartialEquiv
/-- A partial `L`-equivalence, implemented as an equivalence between substructures.  -/
FirstOrder.Language.PartialEquiv : (L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max w w')
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nnnorm_fst_le : ∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.fst‖₊ ≤ ‖x‖₊
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y},
  e.IsImage s t →
    e.source ∩ s = e'.source ∩ s → Set.EqOn (↑e) (↑e') (e.source ∩ s) → Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- This is just composition of morphisms in `C`. Another way to express this would be
`(Over.map f).obj a`, but our definition has nicer definitional properties.  -/
CategoryTheory.Abelian.app : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {P Q : C} → (P ⟶ Q) → CategoryTheory.Over P → CategoryTheory.Over Q
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The trivial additive monoid algebra is the base ring.  -/
AddMonoidAlgebra.uniqueRingEquiv : {R : Type u_1} →
  (M : Type u_4) → [inst : Semiring R] → [inst_1 : AddMonoid M] → [Subsingleton M] → AddMonoidAlgebra R M ≃+* R
-- Batteries.Data.ByteArray
ByteArray.get.eq_1 : ∀ (x : ℕ) (bs : Array UInt8) (x_1 : x < { data := bs }.size), { data := bs }.get x x_1 = bs[x]
-- Batteries.Data.Array.Basic
/-- Find the first minimal element of an array. If the array is empty, `d` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.rangeMinD : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- The underlying rational map of a partial isomorphism.  -/
AlgebraicGeometry.Scheme.PartialIso.toRationalMap : {X Y : AlgebraicGeometry.Scheme} → X.PartialIso Y → X.RationalMap Y
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y),
  (CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqLitValue : BEq Lean.Compiler.LCNF.LitValue
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_union_distrib_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)
-- Mathlib.Topology.Instances.Matrix
Matrix.transpose_tsum : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [T2Space R] {f : X → Matrix m n R},
  (∑'[L] (x : X), f x).transpose = ∑'[L] (x : X), (f x).transpose
-- Mathlib.Data.Nat.Factorization.Root
Nat.factorization_ceilRoot : ∀ (n a : ℕ), (n.ceilRoot a).factorization = a.factorization ⌈/⌉ n
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- Subtraction preserves finiteness.  -/
Set.fintypeSub : {α : Type u_2} → [inst : Sub α] → [DecidableEq α] → (s t : Set α) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s - t)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The postcomposition of an homotopy with a relative morphism.  -/
SSet.RelativeMorphism.Homotopy.postcomp : {X Y Z : SSet} →
  {A : X.Subcomplex} →
    {B : Y.Subcomplex} →
      {φ : A.toSSet ⟶ B.toSSet} →
        {f g : SSet.RelativeMorphism A B φ} →
          {C : Z.Subcomplex} →
            {ψ : B.toSSet ⟶ C.toSSet} →
              f.Homotopy g →
                (f' : SSet.RelativeMorphism B C ψ) →
                  {φψ : A.toSSet ⟶ C.toSSet} →
                    (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ) → (f.comp f' fac).Homotopy (g.comp f' fac)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.integrable_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ),
  MeasureTheory.Integrable (fun b => ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)
-- Mathlib.Analysis.Real.OfDigits
Real.abs_ofDigits_sub_ofDigits_le : ∀ {b : ℕ} {x y : ℕ → Fin b} {n : ℕ}, (∀ i < n, x i = y i) → |Real.ofDigits x - Real.ofDigits y| ≤ (↑b ^ n)⁻¹
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.SearchStep.ofSliceFrom.eq_1 : ∀ {s : String.Slice} {p : s.Pos} (l r : (s.sliceFrom p).Pos),
  (String.Slice.Pattern.SearchStep.rejected l r).ofSliceFrom =
    String.Slice.Pattern.SearchStep.rejected (String.Slice.Pos.ofSliceFrom l) (String.Slice.Pos.ofSliceFrom r)
-- Mathlib.Topology.ContinuousMap.LocallyConstant
/-- The inclusion of locally-constant functions into continuous functions as a multiplicative
monoid hom.  -/
LocallyConstant.toContinuousMapMonoidHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → [inst_2 : Monoid Y] → [inst_3 : ContinuousMul Y] → LocallyConstant X Y →* C(X, Y)
-- Mathlib.Analysis.Complex.HasPrimitives
/-- The vertical integral of `f` from `w.re + z.im * I` to `w` is equal to `(w - z).im * f z`
up to `o(w - z)`, as `w` tends to `z`.  -/
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.hasDerivAt_wedgeIntegral_im_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E],
  ContinuousOn f (Metric.ball c r) →
    ∀ {z : ℂ},
      z ∈ Metric.ball c r →
        (fun w => (∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - (w - z).im • f z) =o[nhds z] fun w => w - z
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_sub_algebraMap_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, (f - (algebraMap R (Module.End R M)) μ).IsSemisimple ↔ f.IsSemisimple
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState.mk : ℕ → ℕ → Std.Sat.CNF.DimacsState✝
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UnifIntegrable.neg : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifIntegrable f p μ → MeasureTheory.UnifIntegrable (-f) p μ
-- Mathlib.Data.Rel
SetRel.preimage_inv : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α), R.inv.preimage s = R.image s
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.BoundaryGE.notMem : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {j : ι},
  e.BoundaryGE j → ∀ {i' : ι'}, c'.Rel i' (e.f j) → ∀ (a : ι), e.f a ≠ i'
-- Mathlib.Algebra.Module.Equiv.Basic
Units.symm_mulLeftLinearEquiv_apply : ∀ (R : Type u_9) {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a : Aˣ) (x : A), ((Units.mulLeftLinearEquiv R A) a).symm x = ↑a⁻¹ * x
-- Std.Data.DHashMap.Internal.Defs
/-- Copies all the entries from `buckets` into a new hash map with a larger capacity.  -/
Std.DHashMap.Internal.Raw₀.expand : {α : Type u} → {β : α → Type v} → [Hashable α] → { d // 0 < d.size } → { d // 0 < d.size }
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The zeroth cyclotomic polynomial is `1`.  -/
Polynomial.cyclotomic_zero : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 0 R = 1
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.glue_aux : ∀ {α : Type u_1} [inst : Preorder α] {l r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l o₂ →
    Ordnode.Valid' o₁ r o₂ →
      Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l →
        Ordnode.BalancedSz l.size r.size → Ordnode.Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size
-- Lean.Elab.Import
/-- Check imported modules for deprecation and emit warnings.

The `-- deprecated_module: ignore` comment can be placed on the `module` keyword to suppress
all warnings, or on individual `import` statements to suppress specific ones.
This follows the same pattern as `-- shake: keep` in Lake shake.

The `headerStx?` parameter carries the header syntax used for checking trailing comments.
When called from the Language Server, the main header syntax may have its trailing trivia
stripped by `unsetTrailing` for caching purposes, so `origHeaderStx?` can supply the original
(untrimmed) syntax to preserve `-- deprecated_module: ignore` annotations on the last import.
 -/
Lean.Elab.checkDeprecatedImports : Lean.Environment →
  Array Lean.Import →
    Lean.Options →
      Lean.Parser.InputContext →
        String.Pos.Raw →
          Lean.MessageLog →
            optParam (Option Lean.Elab.HeaderSyntax) none →
              optParam (Option Lean.Elab.HeaderSyntax) none → Lean.MessageLog
-- Batteries.Data.Fin.Lemmas
Fin.bind_findSome?_guard_isSome : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α},
  (Fin.findSome? (Option.guard fun i => (f i).isSome)).bind f = Fin.findSome? f
-- Mathlib.Data.Fin.Rev
Fin.val_rev_zero : ∀ {n : ℕ} [inst : NeZero n], ↑(Fin.rev 0) = n.pred
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flippingEquiv_symm_apply_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) {X Y : D} (f : X ⟶ Y),
  ((CategoryTheory.Functor.flippingEquiv.symm F).obj k).map f = (F.map f).app k
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.DTreeMap.Const.unitOfList l cmp).size = l.length
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget AddMonCat)
-- Init.GrindInstances.ToInt
Lean.Grind.instMulUInt8UintOfNatNat : Lean.Grind.ToInt.Mul UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.Order.Category.BddLat
BddLat.mk : (toLat : Lat) → [isBoundedOrder : BoundedOrder ↑toLat] → BddLat
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- When `s ≠ 0`, the map `n ↦ n^(-s)` is completely multiplicative and vanishes at zero.  -/
riemannZetaSummandHom : {s : ℂ} → s ≠ 0 → ℕ →*₀ ℂ
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.findAtom_eq_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] {r : α}, IsPredArchimedean.findAtom r = ⊥ ↔ r = ⊥
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.mk' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C}, Nonempty (CategoryTheory.Limits.LimitCone F) → CategoryTheory.Limits.HasLimit F
-- Init.Data.Vector.Lemmas
Vector.toArray_empty : ∀ {α : Type u_1}, #v[].toArray = #[]
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.le_pushforward_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve Y),
  R ≤ CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.pushforward f R)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec : Type
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceLErase.match_7.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size → Sort u_3)
  (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_1 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r) hrb hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hrb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
    | Std.DTreeMap.Internal.Impl.inner rs k v l_1 r, hrb, hlr => h_2 rs k v l_1 r hrb hlr) =
    h_1 hrb hlr
-- Mathlib.Data.WSeq.Basic
/-- Flatten a sequence of weak sequences. (Note that this allows
empty sequences, unlike `Seq.join`.)  -/
Stream'.WSeq.join : {α : Type u} → Stream'.WSeq (Stream'.WSeq α) → Stream'.WSeq α
-- Lean.Meta.Sym.SymM
/-- For functions that have proofs and `Decidable` arguments. For this kind of function we generate
a custom theorem.
Example: `Array.eraseIdx {α : Type u} (xs : Array α) (i : Nat) (h : i < xs.size) : Array α`.
The proof argument `h` depends on `xs` and `i`. To be able to rewrite `xs` and `i`, we use the
auto-generated theorem.
```
Array.eraseIdx.congr_simp {α : Type u} (xs xs' : Array α) (e_xs : xs = xs')
    (i i' : Nat) (e_i : i = i') (h : i < xs.size) : xs.eraseIdx i h = xs'.eraseIdx i' ⋯
```
 -/
Lean.Meta.Sym.CongrInfo.congrTheorem : Lean.Meta.CongrTheorem → Lean.Meta.Sym.CongrInfo
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.mul_bot : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithBot α}, a ≠ 0 → a * ⊥ = ⊥
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`.  -/
AddSubgroupClass.inclusion : {G : Type u_1} →
  [inst : AddGroup G] →
    {S : Type u_4} →
      [inst_1 : SetLike S G] →
        [inst_2 : AddSubgroupClass S G] → [inst_3 : LE S] → [IsConcreteLE S G] → {H K : S} → H ≤ K → ↥H →+ ↥K
-- Mathlib.Analysis.Normed.Group.Real
Real.le_norm_self : ∀ (r : ℝ), r ≤ ‖r‖
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- A bijection between the orbits under the action of an additive subgroup `H` on
`X`, and the orbits under the action of `H` on each orbit under the action of `G`.  -/
AddAction.equivAddSubgroupOrbits : {G : Type u} →
  (X : Type v) →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        (H : AddSubgroup G) →
          AddAction.orbitRel.Quotient (↥H) X ≃
            (ω : Quotient (AddAction.orbitRel G X)) ×
              AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω)
-- Mathlib.Algebra.Quaternion
Quaternion.imI_nnratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ≥0), (↑q).imI = 0
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisBlockImplicit : Lean.Options → Bool
-- Mathlib.Algebra.Category.MonCat.Basic
mulEquivIsoMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : Monoid X] [inst_1 : Monoid Y],
  mulEquivIsoMonCatIso =
    { hom := TypeCat.ofHom fun e => e.toMonCatIso, inv := TypeCat.ofHom fun i => i.monCatIsoToMulEquiv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of the image of a function is the span of the pairwise subtractions with a
given point on the left, excluding the subtraction of that point from itself.  -/
vectorSpan_image_eq_span_vsub_set_left_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) {s : Set ι} {i : ι},
  i ∈ s → vectorSpan k (p '' s) = Submodule.span k ((fun x => p i -ᵥ x) '' p '' (s \ {i}))
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [inst_6 : CharZero R] [inst_7 : IsDomain R] [inst_8 : Finite ι] {i j : ↥b.support},
  i ≠ j → b.cartanMatrix i j = -↑(RootPairing.chainTopCoeff ↑j ↑i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_le_size_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β}, m.size - 1 ≤ (Std.DHashMap.Const.alter m k f).size
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectPatternBVars.go : Lean.Expr → StateM (List ℕ) Unit
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instOrderBot : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [inst : LE β] → [OrderBot β] → OrderBot (l.Germ β)
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdAssoc_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : SimpleGraph α) (H : SimpleGraph β) (I : SimpleGraph γ)
  (p : α × β × γ), (RelIso.symm (G.boxProdAssoc H I)) p = ((p.1, p.2.1), p.2.2)
-- Mathlib.Data.Num.Lemmas
PosNum.of_to_nat : ∀ (n : PosNum), ↑↑n = Num.pos n
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), (↑z).imJ = 0
-- Mathlib.Topology.Order.HullKernel
GaloisConnection.closureOperator.congr_simp : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {l l_1 : α → β} (e_l : l = l_1)
  {u u_1 : β → α} (e_u : u = u_1) (gc : GaloisConnection l u), gc.closureOperator = ⋯.closureOperator
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNormEssSup_add_le : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {μ : MeasureTheory.Measure α} {f g : α → ε},
  MeasureTheory.eLpNormEssSup (f + g) μ ≤ MeasureTheory.eLpNormEssSup f μ + MeasureTheory.eLpNormEssSup g μ
-- Init.Data.List.Basic
List.isEmpty_cons : ∀ {α : Type u} {x : α} {xs : List α}, (x :: xs).isEmpty = false
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {f g : E → ℝ},
  UniformConvexOn s φ f → UniformConcaveOn s ψ g → UniformConvexOn s (φ + ψ) (f - g)
-- Mathlib.Data.Set.Basic
Set.sep_univ : ∀ {α : Type u} {p : α → Prop}, {x | x ∈ Set.univ ∧ p x} = {x | p x}
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- A wide subquiver `H` of `Symmetrify V` determines a wide subquiver of `V`, containing an
arrow `e` if either `e` or its reversal is in `H`.  -/
Quiver.wideSubquiverSymmetrify : {V : Type u_1} → [inst : Quiver V] → WideSubquiver (Quiver.Symmetrify V) → WideSubquiver V
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidCloseTextDocumentParams.toJson : Lean.Lsp.DidCloseTextDocumentParams → Lean.Json
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_inter_Ico_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] {a b c d : α},
  b ≤ c → Multiset.Ico a b ∩ Multiset.Ico c d = 0