mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le : ∀ {X Y : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {f : X ⟶ Y} {J : Y.IdealSheafData},
  J ≤ I.map f ↔ J.comap f ≤ I
-- Mathlib.Analysis.Convex.Jensen
ConcaveOn.bddBelow_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {f : E → β} {s t : Set E},
  s ⊆ t → ConcaveOn 𝕜 t f → BddBelow (f '' s) → BddBelow (f '' (convexHull 𝕜) s)
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instInhabited : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → Inhabited (L.DefinableSet A α)
-- Mathlib.LinearAlgebra.RootSystem.Basic
_private.Mathlib.LinearAlgebra.RootSystem.Basic.0.RootPairing.coroot_eq_coreflection_of_root_eq' : ∀ {ι : 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] [Finite ι] [CharZero R] [IsDomain R]
  [Module.IsTorsionFree R M] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N),
  (∀ (i : ι), (p (root i)) (coroot i) = 2) →
    (∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) →
      (∀ (i : ι),
          Set.MapsTo (⇑(Module.preReflection (coroot i) (p (root i)))) (Set.range ⇑coroot) (Set.range ⇑coroot)) →
        ∀ {i j k : ι},
          root k = (Module.preReflection (root i) (p.flip (coroot i))) (root j) →
            coroot k = (Module.preReflection (coroot i) (p (root i))) (coroot j)
-- Mathlib.Topology.UniformSpace.Ultra.Basic
UniformSpace.isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity : ∀ {X : Type u_1} [inst : UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans],
  V ∈ uniformity X → IsClopen (UniformSpace.ball x V)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.instHasPullbackUnopOfHasPushoutOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.Limits.HasPushout f g], CategoryTheory.Limits.HasPullback f.unop g.unop
-- Mathlib.Topology.Compactness.Compact
/-- A set `s` is compact if for every open cover of `s`, there exists a finite subcover.  -/
isCompact_of_finite_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  (∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i) → IsCompact s
-- Mathlib.Order.Defs.PartialOrder
le_of_eq_or_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b ∨ a < b → a ≤ b
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = true → motive true) → (x = false → motive false) → motive x
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_zsmul : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedCommRing 𝔸]
  [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (z : ℤ) (A : Matrix m m 𝔸), NormedSpace.exp (z • A) = NormedSpace.exp A ^ z
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- We can turn any limit cone over a pair into a bicone.  -/
CategoryTheory.Limits.BinaryBicone.ofLimitCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} →
          CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.BinaryBicone X Y
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a multiplication with unit `M` is the set of elements that commute with everything
in `M`  -/
Submonoid.center : (M : Type u_1) → [inst : MulOneClass M] → Submonoid M
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insert : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), (f.insert c).assignments.size = f.assignments.size
-- Init.Data.UInt.Bitwise
UInt16.ofNatLT_shiftLeft : ∀ {a b : ℕ} (ha : a <<< b < UInt16.size) (hb : b < 16),
  UInt16.ofNatLT (a <<< b) ha = UInt16.ofNatLT a ⋯ <<< UInt16.ofNatLT b ⋯
-- Mathlib.Data.Matrix.Composition
/-- `Matrix.comp` as `LinearEquiv`  -/
Matrix.compLinearEquiv : (I : Type u_1) →
  (J : Type u_2) →
    (K : Type u_3) →
      (L : Type u_4) →
        (R : Type u_5) →
          (R₀ : Type u_7) →
            [inst : Semiring R₀] →
              [inst_1 : AddCommMonoid R] →
                [inst_2 : Module R₀ R] → Matrix I J (Matrix K L R) ≃ₗ[R₀] Matrix (I × K) (J × L) R
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_left_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y_1).left.right.as =
    PUnit.unit
-- Init.Data.Fin.Basic
Fin.val_congr : ∀ {n : ℕ} {a b : Fin n}, a = b → ↑a = ↑b
-- Mathlib.Data.Set.Basic
Set.exists_mem_of_nonempty : ∀ (α : Type u_1) [Nonempty α], ∃ x, x ∈ Set.univ
-- Lean.Meta.CoeAttr
Lean.Meta.instToExprCoeFnInfo : Lean.ToExpr Lean.Meta.CoeFnInfo
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2], W.Δ = W.a₃ ^ 4
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.orderEmbeddingVal_apply : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α], ⇑AddUnits.orderEmbeddingVal = AddUnits.val
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.toDistribLattice.eq_1 : ∀ {α : Type u} [inst : Order.Coframe α],
  Order.Coframe.toDistribLattice = { toLattice := inst.toLattice, le_sup_inf := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Given `X : T`, to upgrade a functor `F : S ⥤ T` to a functor `S ⥤ Over X`, it suffices to
provide maps `F.obj Y ⟶ X` for all `Y` making the obvious triangles involving all `F.map g`
commute.  -/
CategoryTheory.Functor.toOver : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {S : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} S] →
        (F : CategoryTheory.Functor S T) →
          (X : T) →
            (f : (Y : S) → F.obj Y ⟶ X) →
              (∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) →
                CategoryTheory.Functor S (CategoryTheory.Over X)
-- Init.Data.UInt.Lemmas
UInt8.toFin_sub : ∀ (a b : UInt8), (a - b).toFin = a.toFin - b.toFin
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.of_tail : ∀ {hd : ℝ} {tl : Tactic.ComputeAsymptotics.UnitMonomial},
  hd = 0 → tl.AllZero → Tactic.ComputeAsymptotics.UnitMonomial.AllZero (hd :: tl)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_append : ∀ {m n : ℤ}, m < n → (m...n).toList = (m...n - 1).toList ++ [n - 1]
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.IsGood.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {P : HomotopicalAlgebra.PathObject A}
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C],
  autoParam (HomotopicalAlgebra.Fibration P.p) HomotopicalAlgebra.PathObject.IsGood.fibration_p._autoParam → P.IsGood
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
CategoryTheory.Limits.WalkingMulticospan.instFintype : {J : CategoryTheory.Limits.MulticospanShape} →
  [Fintype J.L] → [Fintype J.R] → Fintype (CategoryTheory.Limits.WalkingMulticospan J)
-- Batteries.Data.UInt
UInt64.ext_iff : ∀ {x y : UInt64}, x = y ↔ x.toNat = y.toNat
-- Mathlib.Analysis.Fourier.AddCircle
fourier_neg' : ∀ {T : ℝ} {n : ℤ} {x : AddCircle T}, ↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.any_filterMap : ∀ {α β β' : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Option β'} {p : β' → Bool},
  Std.Iter.any p (Std.Iter.filterMap f it) =
    Std.Iter.any
      (fun x =>
        match f x with
        | some fx => p fx
        | none => false)
      it
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.subgraphOfAdj_eq_induce : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), G.subgraphOfAdj hvw = ⊤.induce {v, w}
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.refl_trans : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), (OpenPartialHomeomorph.refl X).trans e = e
-- Mathlib.Topology.Neighborhoods
/-- A predicate is true in a neighborhood of `x` iff it is true for all the points in an open set
containing `x`.  -/
eventually_nhds_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop},
  (∀ᶠ (y : X) in nhds x, p y) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t
-- Mathlib.Topology.Path
Path.symm_continuous_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_4} [inst_1 : TopologicalSpace ι] {a b : ι → X}
  (γ : (t : ι) → Path (a t) (b t)), Continuous ↿γ → Continuous ↿fun t => (γ t).symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst : Int.Internal.Linear.Var →
  Lean.Meta.Grind.Arith.Cutsat.EqCnstr →
    Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_apply : ∀ {X : TopCat} (x : ↑X), (CategoryTheory.ConcreteCategory.hom TopCat.ι₁) x = (x, 1)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.mk.injEq : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (toGenerators : Algebra.Generators R S ι) (relation : σ → toGenerators.Ring)
  (span_range_relation_eq_ker : Ideal.span (Set.range relation) = toGenerators.ker)
  (toGenerators_1 : Algebra.Generators R S ι) (relation_1 : σ → toGenerators_1.Ring)
  (span_range_relation_eq_ker_1 : Ideal.span (Set.range relation_1) = toGenerators_1.ker),
  ({ toGenerators := toGenerators, relation := relation, span_range_relation_eq_ker := span_range_relation_eq_ker } =
      { toGenerators := toGenerators_1, relation := relation_1,
        span_range_relation_eq_ker := span_range_relation_eq_ker_1 }) =
    (toGenerators = toGenerators_1 ∧ relation = relation_1)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isSymm_iff_eq_flip : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, LinearMap.IsSymm B ↔ B = LinearMap.flip B
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of the reverse direction of `hnot_le_iff_codisjoint_right`. -/
Codisjoint.hnot_le_right : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, Codisjoint b a → ￢b ≤ a
-- Mathlib.Data.Fintype.Quotient
/-- `Trunc.finChoice` as an equivalence.  -/
Trunc.finChoiceEquiv : {ι : Type u_1} → [DecidableEq ι] → [Fintype ι] → {α : ι → Sort u_2} → ((i : ι) → Trunc (α i)) ≃ Trunc ((i : ι) → α i)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `hasExponent_iff` using `ExpChar`.  -/
IsPurelyInseparable.hasExponent_iff' : ∀ (K : Type u_2) (L : Type u_3) [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L] (p : ℕ) [ExpChar K p],
  IsPurelyInseparable.HasExponent K L ↔ ∃ e, ∀ (a : L), a ^ p ^ e ∈ (algebraMap K L).range
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z T : C} {a₁ a₂ a₁₂ : ℕ} (α : CategoryTheory.Abelian.Ext X Y a₁)
  (β : CategoryTheory.Abelian.Ext Y Z a₂) (γ : CategoryTheory.Abelian.Ext Z T 0) (h₁₂ : a₁ + a₂ = a₁₂),
  (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.precomp_map_heq : ∀ {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 G : CategoryTheory.Functor C D}
  (H : CategoryTheory.Functor E C),
  (∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) → ∀ {X Y : E} (f : X ⟶ Y), (H.comp F).map f ≍ (H.comp G).map f
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_id_apply : ∀ {K : Type u_1} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing M] (j : K →+* M) (p : ℕ) [inst_2 : ExpChar M p]
  [inst_3 : ExpChar K p] [inst_4 : PerfectRing M p] (x : K), (PerfectRing.lift (RingHom.id K) j p) x = j x
-- Mathlib.CategoryTheory.Balanced
CategoryTheory.isIso_of_mono_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Mono f] [CategoryTheory.Epi f], CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor Eᵒᵖ Cᵒᵖ} (α : F ≅ G),
  CategoryTheory.NatIso.unop (H.isoWhiskerLeft α) =
    H.unopComp G ≪≫ H.unop.isoWhiskerLeft (CategoryTheory.NatIso.unop α) ≪≫ (H.unopComp F).symm
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalRightDistrib.preservesBinaryCoproducts_tensorRight : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.IsMonoidalRightDistrib C] (X : C),
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
    (CategoryTheory.MonoidalCategory.tensorRight X)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso_trans : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : LinearOrderedCommGroupWithZero Γ''₀] [inst_3 : Ring R]
  {v : Valuation R Γ₀} {w : Valuation R Γ'₀} {u : Valuation R Γ''₀} (h : v.IsEquiv w) (h' : w.IsEquiv u),
  h.orderMonoidIso.trans h'.orderMonoidIso = ⋯.orderMonoidIso
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₁.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C},
  (∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₂ → P T.obj₃ → P.isoClosure T.obj₁) →
    P.IsTriangulatedClosed₁
-- Init.Sym.Lemmas
Lean.Sym.Int16.lt_eq_false : ∀ (a b : Int16), decide (a < b) = false → (a < b) = False
-- Mathlib.CategoryTheory.Presentable.Directed
/-- If `κ` is a cardinal, this structure contains the data of a `κ`-bounded diagram
with a unique terminal object in a category `J`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal : (J : Type w) → [CategoryTheory.SmallCategory J] → Cardinal.{w} → Type w
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.push_parentD : ∀ {i : ℕ} (arr : Array Batteries.UFNode),
  Batteries.UnionFind.parentD (arr.push { parent := arr.size, rank := 0 }) i = Batteries.UnionFind.parentD arr i
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced)
  (hr : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size),
  Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr =
    match l, hl, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hl, hlr =>
      { k := k, v := v, tree := { impl := r, balanced_impl := hr, size_impl := ⋯ } }
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr =>
      match Std.DTreeMap.Internal.Impl.minView k' v' l' r' ⋯ ⋯ ⋯ with
      | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
        { k := dk, v := dv,
          tree :=
            { impl := Std.DTreeMap.Internal.Impl.balanceRErase k v dt r ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ } }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instOne : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : PseudoMetricSpace β] → [One β] → One (BoundedContinuousFunction α β)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.X_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ}, CochainComplex.ConnectData.X K L 0 = L.X 0
-- Lean.PrettyPrinter.Delaborator.Metavariable
/-- Creates an action that creates a description of the metavariable and its status in Markdown format,
for use in the docstring in `DelabTermInfo`.
 -/
Lean.PrettyPrinter.Delaborator.mkDescribeMVar : Lean.MVarId → optParam Bool false → Lean.PrettyPrinter.Delaborator.DelabM (Lean.PPContext → IO String)
-- Init.Data.Fin.Lemmas
Fin.subNat_zero : ∀ {n : ℕ} (i : Fin n) (h : 0 ≤ ↑i), Fin.subNat 0 i h = i
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constSMul_symm : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [inst_3 : IsIsometricSMul G X] (c : G), (IsometryEquiv.constSMul c).symm = IsometryEquiv.constSMul c⁻¹
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of nodes associated with a 2-morphism. The position is counted from the
specified natural numbers.  -/
Mathlib.Tactic.BicategoryLike.WhiskerLeft.nodes : ℕ → ℕ → ℕ → Mathlib.Tactic.BicategoryLike.WhiskerLeft → List Mathlib.Tactic.Widget.StringDiagram.Node
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_filter_bne_zero : ∀ {M : Type u_4} [inst : AddMonoid M] [inst_1 : BEq M] [LawfulBEq M] (l : List M),
  (List.filter (fun x => x != 0) l).sum = l.sum
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C} {a' : ℤ}
  (f : CategoryTheory.ShiftedHom X Y a') (n a : ℤ) (h : n + a = a'),
  (CategoryTheory.ShiftedHom.opEquiv' n a a' h) f =
    (CategoryTheory.ShiftedHom.opEquiv n)
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorAdd' C a n a' ⋯).hom.app Y))
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.g_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  CategoryTheory.CategoryStruct.comp S₁.g self.h₃ = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mem_of_adj_spanningCoe : ∀ {V : Type u} {v w : V} {s : Set V} (G : SimpleGraph ↑s), G.spanningCoe.Adj v w → v ∈ s
-- Mathlib.RingTheory.Spectrum.Prime.Jacobson
PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace : ∀ {R : Type u_1} [inst : CommRing R], IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_of_zero_tmul : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  (a : 𝒜 0) (b : DirectSum ι fun i => ℬ i),
  (TensorProduct.gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 0) a ⊗ₜ[R] b) = b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 0) a
-- Lean.DocString.Parser
/-- Parses a definition list.  -/
Lean.Doc.Parser.definitionList : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.indCoindNatIso_hom_app : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G)
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (X : Rep.{max u w, u, v} k ↥S),
  (Rep.indCoindNatIso k S).hom.app X = X.indCoindIso.hom
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_natTrailingDegree_pred_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {hp : 0 < ↑p.natTrailingDegree},
  p.coeff (p.natTrailingDegree - 1) = 0
-- Mathlib.Order.Filter.Cofinite
/-- A filter is free iff it is smaller than the cofinite filter.  -/
le_cofinite_iff_ker : ∀ {α : Type u_2} {f : Filter α}, f ≤ Filter.cofinite ↔ f.ker = ∅
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopInverse_obj : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm),
  (HomologicalComplex.unopInverse V c).obj X = Opposite.op X.opSymm
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart.eq_1 : ∀ (x y : ℝ) [h : Fact (x < y)],
  IccRightChart x y =
    { toFun := fun z => ⟨WithLp.toLp 2 fun x_1 => y - ↑z, ⋯⟩, invFun := fun z => ⟨max (y - (↑z).ofLp 0) x, ⋯⟩,
      source := {z | x < ↑z}, target := {z | (↑z).ofLp 0 < y - x}, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯,
      right_inv' := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }
-- Lean.Elab.Tactic.Basic
/-- Runs `tactic` with only the first unsolved goal as the goal, and expects it leave no goals.
Fails if there are no goal to be solved.
 -/
Lean.Elab.Tactic.focusAndDone : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finite_of_finrank_pos : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], 0 < Module.finrank R M → Module.Finite R M
-- Mathlib.Topology.Separation.Regular
disjoint_nhdsSet_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s → IsClosed t → Disjoint s t → Disjoint (nhdsSet s) (nhdsSet t)
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.presheafIsGeneratedBy_of_isFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w))
  [inst_1 : CategoryTheory.PresheafIsFinite F],
  CategoryTheory.PresheafIsGeneratedBy F CategoryTheory.Subfunctor.IsFinite.x
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallWithContext.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (caller : ℕ) (params : Array Lean.Expr) (callee : ℕ) (args : Array Lean.Expr)
  (ctxt : Lean.Elab.WF.GuessLex.SavedLocalContext),
  sizeOf { ref := ref, caller := caller, params := params, callee := callee, args := args, ctxt := ctxt } =
    1 + sizeOf ref + sizeOf caller + sizeOf params + sizeOf callee + sizeOf args + sizeOf ctxt
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.eraseAddHom_apply : ∀ {ι : Type u} (β : ι → Type v) [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] (i : ι)
  (x : Π₀ (i : ι), β i), (DFinsupp.eraseAddHom β i) x = DFinsupp.erase i x