mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.bddAbove_range_norm_comp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), BddAbove (Set.range (norm ∘ ⇑f))
-- Mathlib.Data.Multiset.Fold
Multiset.coe_fold_l : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (l : List α),
  Multiset.fold op b ↑l = List.foldl op b l
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_coe : ∀ (x : ℝ), (↑x).exp = ENNReal.ofReal (Real.exp x)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearEquiv_congrIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H),
  (TensorProduct.congrIsometry f g).toLinearEquiv = TensorProduct.congr f.toLinearEquiv g.toLinearEquiv
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_eq_sum_range : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {p : Polynomial R}
  (x : S), (Polynomial.aeval x) p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.le_order_subst_left : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {f : MvPowerSeries τ R} {φ : PowerSeries R},
  MvPowerSeries.constantCoeff f = 0 → φ.order ≤ (PowerSeries.subst f φ).order
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_le_sum_index : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : AddCommMonoid β]
  [inst_3 : Preorder β] [IsOrderedAddMonoid β] [inst_5 : DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β},
  f₁ ≤ f₂ →
    (∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)) → (∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) → f₁.sum h ≤ f₂.sum h
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_eq_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} (H : s.Nonempty)
  (f : β → α), s.sup' H f = s.sup f
-- Lean.Server.CodeActions.Provider
Lean.CodeAction.FindTacticResult.tacticSeq.sizeOf_spec : ∀ (preferred : Bool) (insertIdx : ℕ) (a : Lean.Syntax.Stack),
  sizeOf (Lean.CodeAction.FindTacticResult.tacticSeq preferred insertIdx a) =
    1 + sizeOf preferred + sizeOf insertIdx + sizeOf a
-- Mathlib.Combinatorics.Matroid.Sum
Equiv.sumEquivSigmaBool.eq_1 : ∀ (α β : Type u_9),
  Equiv.sumEquivSigmaBool α β =
    { toFun := fun s => Sum.elim (fun x => ⟨false, x⟩) (fun x => ⟨true, x⟩) s,
      invFun := fun s =>
        match s with
        | ⟨false, a⟩ => Sum.inl a
        | ⟨true, b⟩ => Sum.inr b,
      left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (n = 0 → motive 0) → ((k : ℕ) → n = k.succ → motive k.succ) → motive n
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesColimitsOfShape J F.unop
-- Mathlib.Algebra.Lie.Basis.Prod
/-- `LieAlgebra.Basis.prod` is equivalent to its right input algebra.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodEquivRight : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {K : Type u_5} →
                    [inst_4 : Field K] →
                      [CharZero K] →
                        [inst_6 : LieAlgebra K L₁] →
                          [FiniteDimensional K L₁] →
                            {H₁ : LieSubalgebra K L₁} →
                              (b₁ : LieAlgebra.Basis ι₁ H₁) →
                                [inst_8 : LieAlgebra K L₂] →
                                  [FiniteDimensional K L₂] →
                                    {H₂ : LieSubalgebra K L₂} →
                                      (b₂ : LieAlgebra.Basis ι₂ H₂) →
                                        (Matrix.reindex eι eι) b₁.A = b₂.A →
                                          [LieAlgebra.IsSimple K L₁] → ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂) ≃ₗ⁅K⁆ L₂
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.of_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} {pos : s.Pos}
  {pos' : t.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos →
    ∀ (h₁ : s.copy = t.copy), pos.cast h₁ = pos' → String.Slice.Pattern.Model.IsLongestRevMatch pat pos'
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehaviorSymbol.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_mul_of_coprime' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)]
  {a b p : Associates α},
  Irreducible p →
    (∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) →
      p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.instCategoryPath : {J : Type u_1} →
  [inst : LinearOrder J] → (i j : J) → CategoryTheory.Category.{u_1, u_1} (CategoryTheory.SimplicialThickening.Path i j)
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.eq_def : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (proof : Array Std.Tactic.BVDecide.LRAT.IntAction)
  (idx : ℕ),
  Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof idx =
    if h : idx < proof.size then
      have step := Std.Tactic.BVDecide.LRAT.Internal.intActionToDefaultClauseAction n proof[idx];
      match step with
      | none => Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1)
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) =>
        match
          Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f Std.Tactic.BVDecide.LRAT.Internal.Clause.empty
            rupHints with
        | (fst, checkSuccess) =>
          if checkSuccess = true then Std.Tactic.BVDecide.LRAT.Internal.Result.success
          else Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) =>
        match Std.Tactic.BVDecide.LRAT.Internal.Formula.performRupAdd f c rupHints with
        | (f, checkSuccess) =>
          if checkSuccess = true then Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1)
          else Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) =>
        if pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c then
          match Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c pivot rupHints ratHints with
          | (f, checkSuccess) =>
            if checkSuccess = true then Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1)
            else Std.Tactic.BVDecide.LRAT.Internal.Result.rupFailure
        else Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof (idx + 1)
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) =>
        Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids)
          proof (idx + 1)
    else Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t[a]? = none
-- Mathlib.Topology.UniformSpace.Defs
/-- **Alias** of the reverse direction of `UniformSpace.isCover_iff_subset_iUnion_ball`. -/
SetRel.IsCover.of_subset_iUnion_ball : ∀ {β : Type ub} {U : SetRel β β} [U.IsSymm] {s N : Set β}, s ⊆ ⋃ y ∈ N, UniformSpace.ball y U → U.IsCover s N
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f →
    MeasureTheory.IsStoppingTime ℱ fun ω => ↑(MeasureTheory.upperCrossingTime a b f N n ω)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_const_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) {s : Set α},
  MeasurableSet s → ((MeasureTheory.SimpleFunc.const α c).restrict s).lintegral μ = c * μ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.diff_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.diff m₂ = m₁ \ m₂
-- Init.Data.SInt.Lemmas
Int16.neg_ne_zero : ∀ {a : Int16}, -a ≠ 0 ↔ a ≠ 0
-- Init.Control.Lawful.Instances
EStateM.run_set : ∀ {σ ε : Type u_1} (s₁ s₂ : σ), (set s₁).run s₂ = EStateM.Result.ok PUnit.unit s₁
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ'_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0),
  (Module.Relations.Solution.ofπ' π hπ).π = π
-- Mathlib.Tactic.Measurability
/-- The tactic `measurability` solves goals of the form `Measurable f`, `AEMeasurable f`,
`StronglyMeasurable f`, `AEStronglyMeasurable f μ`, or `MeasurableSet s` by applying lemmas tagged
with the `measurability` user attribute.

Note that `measurability` uses `fun_prop` for solving measurability of functions, so statements
about `Measurable`, `AEMeasurable`, `StronglyMeasurable` and `AEStronglyMeasurable` should be tagged
with `fun_prop` rather that `measurability`. The `measurability` attribute is equivalent to
`fun_prop` in these cases for backward compatibility with the earlier implementation.
 -/
measurability! : Lean.ParserDescr
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_eq_extend' : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ {s : Set α}, P s → (MeasureTheory.inducedOuterMeasure m P0 m0) s = MeasureTheory.extend m s
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.lt_eq_isStrictMinor : ∀ {α : Type u_1}, (fun M M' => M < M') = Matroid.IsStrictMinor
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.mk.sizeOf_spec : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [inst_4 : SizeOf R] [inst_5 : SizeOf A] (val : A)
  (isGroupLikeElem_val : IsGroupLikeElem R val),
  sizeOf { val := val, isGroupLikeElem_val := isGroupLikeElem_val } = 1 + sizeOf val + sizeOf isGroupLikeElem_val
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RicSliceData α β)) Id (Std.DTreeMap.Internal.RxcIterator α β)
        ((a : α) × β a)
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a...b` by
varying the upper bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a`, the statement holds for the empty range `a...b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, if the
statement holds for `a...b`, it also holds for the larger range `a...(b + 1)`.

The following is an example reproving `length_toList_rco`.

```
example (a b : Int) : (a...b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_rco_right
  case base =>
    simp only [Int.toList_rco_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step a b hle ih =>
    rw [Int.toList_rco_eq_append (by omega),
      List.length_append, List.length_singleton, Int.add_sub_cancel, ih]
    omega
``` -/
Int.induct_rco_right : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a → motive a b) → (∀ (a b : ℤ), a ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℤ), motive a b
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddRightCancelMonoid : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddRightCancelMonoid α] → AddRightCancelMonoid (Matrix m n α)
-- Lean.Parser.Term
Lean.Parser.Term.leftact.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.mk : {X : Type u_5} →
  [inst : TopologicalSpace X] →
    (toSetoid : Setoid X) → (∀ (x : X), IsOpen (Set.ofPred (toSetoid x))) → DiscreteQuotient X
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.integral_prod_left : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (fun x => ∫ (y : β), f (x, y) ∂ν) μ
-- Lean.ParserCompiler
Lean.ParserCompiler.Context : Type → Type
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t) (j : J) {Z : C} (h : s.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.ι.app j)
      (CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv h) =
    CategoryTheory.CategoryStruct.comp (s.ι.app j) h
-- Mathlib.Algebra.Ring.Associated
Associated.neg_left : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : HasDistribNeg M] {a b : M}, Associated a b → Associated (-a) b
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The normed algebra structure on `Matrix n n 𝕜` arising from the operator norm given by the
identification with (continuous) linear endomorphisms of `EuclideanSpace 𝕜 n`.  -/
Matrix.instL2OpNormedAlgebra : {𝕜 : Type u_1} →
  {n : Type u_3} → [inst : RCLike 𝕜] → [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → NormedAlgebra 𝕜 (Matrix n n 𝕜)
-- Mathlib.LinearAlgebra.Matrix.ToLin
DistribMulAction.toLinearEquiv.congr_simp : ∀ (R : Type u_1) {S : Type u_4} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Group S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s s_1 : S),
  s = s_1 → DistribMulAction.toLinearEquiv R M s = DistribMulAction.toLinearEquiv R M s_1
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lsmul_eq_distribSMultoLinearMap : ∀ {R : Type u_2} [inst : CommSemiring R] (M : Type u_5) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R),
  (LinearMap.lsmul R M) r = DistribSMul.toLinearMap R M r
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_maxKey?_of_isSome_maxKey?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  (Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l)).isSome = true →
    (Std.Internal.List.maxKey? l).isSome = true
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrow`. -/
CategoryTheory.Classifier.χ_pullback_obj_mk_truth_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (𝒞 : CategoryTheory.Subobject.Classifier C) {X : C} (φ : X ⟶ 𝒞.Ω),
  𝒞.χ ((CategoryTheory.Subobject.pullback φ).obj 𝒞.truth_as_subobject).arrow = φ
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_fp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (o : Ordinal.{u}), f (Ordinal.deriv f o) = Ordinal.deriv f o
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.id : Lean.Expr → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Std.Data.ExtDTreeMap.Basic
/-- Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.ExtDTreeMap.containsThenInsert : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → β a → Bool × Std.ExtDTreeMap α β cmp
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.multiples_le : ∀ {M : Type u_1} [inst : AddMonoid M] {n : M} {P : AddSubmonoid M}, AddSubmonoid.multiples n ≤ P ↔ n ∈ P
-- Mathlib.Geometry.Manifold.Instances.Sphere
surjective_stereographic : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  Function.Surjective ↑(stereographic hv)
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.lt.eq_1 : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α},
  Localization.lt = { lt := fun a b => a.liftOn₂ b (fun a₁ a₂ b₁ b₂ => ↑b₂ * a₁ < ↑a₂ * b₁) ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {a : α} {fallback : β}, Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = m.getD a fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.maxKey!_alter_eq_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.maxKey! = k ↔
      (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.DoElemCont.mkUnit : Lean.Elab.Do.DoElabM Lean.Expr → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldrM f init t = Array.foldrM (fun a b => f a.fst a.snd b) init t.toArray
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.topEquivalence_unitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.ObjectProperty.topEquivalence C).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id ⊤.FullSubcategory)
-- Mathlib.Topology.UniformSpace.Defs
isOpen_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α}, IsOpen s ↔ ∀ x ∈ s, {p | p.1 = x → p.2 ∈ s} ∈ uniformity α
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.rclikeToReal_realToRCLike : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, ℝ)),
  (ContinuousMap.realToRCLike 𝕜 f).rclikeToReal = f
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- We can characterize morphisms out of a tensor product via their precomposition with `inl` and
`inr`.  -/
AugmentedSimplexCategory.tensorObj_hom_ext : ∀ {x y z : AugmentedSimplexCategory} (f g : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟶ z),
  CategoryTheory.CategoryStruct.comp (x.inl y) f = CategoryTheory.CategoryStruct.comp (x.inl y) g →
    CategoryTheory.CategoryStruct.comp (x.inr y) f = CategoryTheory.CategoryStruct.comp (x.inr y) g → f = g
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrimeAlgebra : {K : Type u} →
  [inst : Field K] → (A : ValuationSubring K) → (P : Ideal ↥A) → [inst_1 : P.IsPrime] → Algebra ↥A ↥(A.ofPrime P)
-- Init.Grind.Interactive
/-- `expose_names` renames all inaccessible variables with accessible names, making them available
for reference in generated tactics. However, this renaming introduces machine-generated names
that are not fully under user control. `expose_names` is primarily intended as a preamble for
generated `grind` tactic scripts.
 -/
Lean.Parser.Tactic.Grind.exposeNames : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceLErasePrecond_zero_iff : ∀ {n : ℕ}, Std.DTreeMap.Internal.Impl.BalanceLErasePrecond 0 n ↔ n ≤ 1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_add : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  (a b : A), D (a + b) = D a + D b
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
/-- Given two finsets, find all trees that can be formed with
left child in `a` and right child in `b`  -/
BinaryTree.pairwiseNode : Finset (BinaryTree Unit) → Finset (BinaryTree Unit) → Finset (BinaryTree Unit)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_snd : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))]
  (h : CategoryTheory.Limits.IsTerminal Y₃),
  (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).snd =
    (CategoryTheory.Limits.IsTerminal.isTerminalObj (G.obj (Opposite.op Y₁)) Y₃ h).from
      ((G.obj (Opposite.op X₁)).obj X₃)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- The type of derivations with values in a `B`-module `M` relative
to a morphism `f : A ⟶ B` in the category `CommRingCat`.  -/
ModuleCat.Derivation : {A B : CommRingCat} → ModuleCat ↑B → (A ⟶ B) → Type (max v u)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cocone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coneOfCoconeLeftOp : {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.Cocone F.leftOp → CategoryTheory.Limits.Cone F
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_mul_add : ∀ {a b c : ℤ}, a ∣ a * b + c ↔ a ∣ c