mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.mk.inj : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} {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}
  {form : LinearMap.BilinForm R M} {symm : LinearMap.IsSymm form}
  {ne_zero : ∀ (i : ι), (form (P.root i)) (P.root i) ≠ 0}
  {isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i)}
  {form_1 : LinearMap.BilinForm R M} {symm_1 : LinearMap.IsSymm form_1}
  {ne_zero_1 : ∀ (i : ι), (form_1 (P.root i)) (P.root i) ≠ 0}
  {isOrthogonal_reflection_1 : ∀ (i : ι), LinearMap.IsOrthogonal form_1 ⇑(P.reflection i)},
  { form := form, symm := symm, ne_zero := ne_zero, isOrthogonal_reflection := isOrthogonal_reflection } =
      { form := form_1, symm := symm_1, ne_zero := ne_zero_1, isOrthogonal_reflection := isOrthogonal_reflection_1 } →
    form = form_1
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- A continuous map of affine spaces  -/
ContinuousAffineMap : (R : Type u_1) →
  {V : Type u_2} →
    {W : Type u_3} →
      (P : Type u_4) →
        (Q : Type u_5) →
          [inst : Ring R] →
            [inst_1 : AddCommGroup V] →
              [Module R V] →
                [TopologicalSpace P] →
                  [AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [Module R W] → [TopologicalSpace Q] → [AddTorsor W Q] → Type (max (max (max u_2 u_3) u_4) u_5)
-- Std.Data.HashMap.Lemmas
/-- Variant of `getElem!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.getElem!_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → γ} {k : α},
  (Std.HashMap.map f m)[k]! = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).get!
-- Mathlib.Data.NNReal.Defs
Real.one_le_toNNReal : ∀ {r : ℝ}, 1 ≤ r.toNNReal ↔ 1 ≤ r
-- Mathlib.Probability.Process.LocalProperty
/-- A localizing sequence is a sequence of stopping times that is almost surely increasing and
tends almost surely to infinity.  -/
ProbabilityTheory.IsLocalizingSequence : {ι : Type u_1} →
  {Ω : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        [inst_1 : TopologicalSpace ι] →
          [OrderTopology ι] →
            MeasureTheory.Filtration ι mΩ →
              (ℕ → Ω → WithTop ι) →
                autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsLocalizingSequence._auto_1 → Prop
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioo_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioo (Fin.castLE h a) (Fin.castLE h b), f i = ∑ i ∈ Finset.Ioo a b, f (Fin.castLE h i)
-- Mathlib.Algebra.GCDMonoid.Basic
/-- A cancellative monoid with zero always admits a `NormalizationMonoid` structure.  -/
instNonemptyNormalizationMonoidOfIsLeftCancelMulZero : ∀ (α : Type u_2) [inst : MonoidWithZero α] [IsLeftCancelMulZero α], Nonempty (NormalizationMonoid α)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ico_add_one_left_eq_Ioo : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] (a b : α),
  Set.Ico (a + 1) b = Set.Ioo a b
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Composition as a semigroup homomorphism.  -/
ZeroAtInftyContinuousMap.compMulHom : {β : Type v} →
  {γ : Type w} →
    {δ : Type u_2} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : MulZeroClass δ] →
              [inst_4 : ContinuousMul δ] →
                CocompactMap β γ → ZeroAtInftyContinuousMap γ δ →ₙ* ZeroAtInftyContinuousMap β δ
-- Mathlib.Data.List.Cycle
List.next_cons_concat : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y : α),
  x ≠ y → x ∉ l → ∀ (h : optParam (x ∈ y :: l ++ [x]) ⋯), (y :: l ++ [x]).next x h = y
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialFibrations_sub_fibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialFibrations C ≤ HomotopicalAlgebra.fibrations C
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_le_lift : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α},
  Cardinal.lift.{u, v} (Cardinal.mk ↑(f '' s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)
-- Mathlib.Analysis.Convex.Strict.Extreme
/-- In a strictly convex space, the sphere is contained in the extreme points of the closed ball
when the radius is nonzero.
In a nontrivial space, they are equal, see `extremePoints_closedBall_eq_sphere`.  -/
StrictConvexSpace.sphere_subset_extremePoints_closedBall : ∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : NormedSpace ℝ A] [StrictConvexSpace ℝ A] (a : A) {r : ℝ},
  r ≠ 0 → Metric.sphere a r ⊆ Set.extremePoints ℝ (Metric.closedBall a r)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_le_vertexCoverNum_of_injective : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G →g H),
  Function.Injective ⇑f → G.vertexCoverNum ≤ H.vertexCoverNum
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.IsStableUnderCobaseChangeAlong f` states that for any morphism satisfying `P` with the same
codomain as `f`, any pullback of that morphism along `f` also satisfies `P`.  -/
CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter m₂ ⋯) k = none
-- Mathlib.Data.Set.Basic
Set.mem_ite_univ_right : ∀ {α : Type u} (p : Prop) [inst : Decidable p] (t : Set α) (x : α), (x ∈ if p then t else Set.univ) ↔ p → x ∈ t
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) ⁻¹' Set.Ioo b c = Set.Ioo (a / c) (a / b)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal.inj : ∀ {R : Type u_1} {Γ₀ : Type u_2} {inst : LinearOrderedCommGroupWithZero Γ₀} {inst_1 : Ring R} {v : Valuation R Γ₀}
  {ofVal ofVal_1 : R}, WithVal.toVal v ofVal = WithVal.toVal v ofVal_1 → ofVal = ofVal_1
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For `1 ≤ r`, the characteristic function is non-negative.
 -/
ValueDistribution.characteristic_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {a : WithTop E} {r : ℝ},
  1 ≤ r → 0 ≤ ValueDistribution.characteristic f a r
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn : ∀ {p : ℝ},
  p ≠ 0 →
    Asymptotics.IsEquivalent Filter.atTop (deriv fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) fun z =>
      p * z ^ (p - 1)
-- Mathlib.CategoryTheory.Grothendieck
/-- If `F : C ⥤ Cat` is a functor and `t : c ⟶ d` is a morphism in `C`, then `transport` maps each
`c`-based element `x` of `Grothendieck F` to a `d`-based element `x.transport t`.

`toTransport` is the morphism `x ⟶ x.transport t` induced by `t` and the identity on fibers.
 -/
CategoryTheory.Grothendieck.toTransport : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      (x : CategoryTheory.Grothendieck F) → {c : C} → (t : x.base ⟶ c) → x ⟶ x.transport t
-- Lean.Elab.Tactic.Doc
/-- The user-facing name to display (typically the first keyword token)  -/
Lean.Elab.Tactic.Doc.TacticDoc.userName : Lean.Elab.Tactic.Doc.TacticDoc → String
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.isoMk_hom_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber),
  (CategoryTheory.Grothendieck.isoMk e₁ e₂).hom.base = e₁.hom
-- Mathlib.Computability.Partrec
Partrec.map_encode_iff : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ},
  (Partrec fun a => Part.map Encodable.encode (f a)) ↔ Partrec f
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- subsemigroup closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
Subsemigroup.closure_mono : ∀ {M : Type u_1} [inst : Mul M] ⦃s t : Set M⦄, s ⊆ t → Subsemigroup.closure s ≤ Subsemigroup.closure t
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Cardinal.lt_cof_ord_power`. -/
Cardinal.lt_cof_power : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → 1 < b → a < (b ^ a).ord.cof
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom_id : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C)
  (a : CategoryTheory.FreeBicategory B),
  CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.id a) =
    CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.lcomapDomain_eq_linearProjOfIsCompl : ∀ {R : Type u_1} {ι : Type u_3} [inst : Ring R] {α : Type u_4} {β : Type u_5} {u : α → ι} {v : β → ι}
  (hu : Function.Injective u) (h : IsCompl (Set.range u) (Set.range v)),
  Finsupp.lcomapDomain u hu =
    LinearMap.linearProjOfIsCompl (Submodule.span R (Set.range fun x => fun₀ | v x => 1)) (Finsupp.lmapDomain R R u) ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functoriality_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y),
  ((CategoryTheory.Limits.Cone.functoriality F G).map f).hom = G.map f.hom
-- Mathlib.Data.Set.FiniteExhaustion
/-- Given `K : FiniteExhaustion s` and `K' : FiniteExhaustion t`, `FiniteExhaustion.prod K K'`
is the finite exhaustion on `s ×ˢ t` given by the pointwise set product of the exhaustions.  -/
Set.FiniteExhaustion.prod : {α : Type u_1} →
  {s : Set α} → s.FiniteExhaustion → {β : Type u_2} → {t : Set β} → t.FiniteExhaustion → (s ×ˢ t).FiniteExhaustion
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.vcomp : {B : Type u} →
  [inst : Quiver B] →
    {a b : CategoryTheory.FreeBicategory B} →
      {f g h : a ⟶ b} →
        CategoryTheory.FreeBicategory.Hom₂ f g →
          CategoryTheory.FreeBicategory.Hom₂ g h → CategoryTheory.FreeBicategory.Hom₂ f h
-- Init.Data.SInt.Bitwise
Int32.zero_shiftLeft : ∀ {a : Int32}, 0 <<< a = 0
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_lt_of_eq` -/
ssubset_of_ssubset_of_eq : ∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LT α], a ⊂ b → b = c → a ⊂ c
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.cosh_dist' : ∀ (z w : UpperHalfPlane), Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.isUnit_divided_by_X_pow_order : ∀ {k : Type u_2} [inst : Field k] {f : PowerSeries k}, f ≠ 0 → IsUnit f.divXPowOrder
-- Batteries.Data.UInt
UInt64.max_def : ∀ (x y : UInt64), x ⊔ y = if x ≤ y then y else x
-- Mathlib.Tactic.Widget.StringDiagram
/-- **Alias** of `List.consecutivePairs`. -/
Mathlib.Tactic.BicategoryLike.pairs : {α : Type u_1} → List α → List (α × α)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- A lemma estimating the difference between $\frac{1}{2} * \log(\frac{1+x}{1-x})$ and its
Taylor series at `0`, where the bound tends to `0`. This bound is particularly useful for explicit
estimates of logarithms.

Note that thanks to the geometric series, the derivative has a particularly simple form, and means
that it is more convenient to avoid Taylor's theorem for this proof.
 -/
Real.sum_range_sub_log_div_le : ∀ {x : ℝ},
  |x| < 1 →
    ∀ (n : ℕ),
      |1 / 2 * Real.log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)| ≤
        |x| ^ (2 * n + 1) / (1 - x ^ 2)
-- Init.SizeOf
Lean.instSizeOfName : SizeOf Lean.Name
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ico_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Ico (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Ico a b, f (Fin.cast h i)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClassCircle_1 : SMulCommClass Complex.UnitClosedDisc Circle Complex.UnitClosedDisc
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one_eq_map_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithTop α} [inst : One β], 1 = WithTop.map f v ↔ ∃ x, v = ↑x ∧ f x = 1
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- If the input syntax is of the form `set_option <option> num in <string> cmd`,
where `<option>` contains `maxHeartbeats`, then it returns
* the `<option>`, as a name (typically, `maxHeartbeats` or `synthInstance.maxHeartbeats`);
* the number `num` and
* whatever is in `<string>`. Note that `<string>` can only consist of whitespace and comments.

Otherwise, it returns `none`.
 -/
_private.Mathlib.Tactic.Linter.DeprecatedSyntaxLinter.0.Mathlib.Linter.Style.getSetOptionMaxHeartbeatsComment : Lean.Syntax → Option (Lean.Name × ℕ × Substring.Raw)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The isomorphism `(M →+ N₁) ≃+ (M →+ N₂)` obtained by postcomposition with
an additive equivalence `e : N₁ ≃+ N₂`.  -/
AddEquiv.addMonoidHomCongrRight : {M : Type u_4} →
  {N₁ : Type u_9} →
    {N₂ : Type u_10} →
      [inst : AddZeroClass M] →
        [inst_1 : AddCommMonoid N₁] → [inst_2 : AddCommMonoid N₂] → N₁ ≃+ N₂ → (M →+ N₁) ≃+ (M →+ N₂)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.insert k v).get k ⋯ = v
-- Mathlib.Order.Fin.Basic
Fin.strictMono_natAdd : ∀ {m : ℕ} (n : ℕ), StrictMono (Fin.natAdd n)
-- Lean.Data.Lsp.Utf16
/-- Convert the Lean `DeclarationRange` to an LSP `Range` by turning the 1-indexed line numbering into a
0-indexed line numbering and converting the character offset within the line to a UTF-16 indexed
offset.
 -/
Lean.DeclarationRange.toLspRange : Lean.DeclarationRange → Lean.Lsp.Range
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.op
-- Batteries.Data.String.Lemmas
String.utf8PrevAux_of_valid : ∀ {cs cs' : List Char} {c : Char} {i p : ℕ},
  i + (String.utf8Len cs + c.utf8Size) = p →
    String.Pos.Raw.utf8PrevAux (cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + String.utf8Len cs }
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- Topology on the total space of the continuous `σ`-semilinear maps between two "normable" vector
bundles over the same base.  -/
Bundle.ContinuousAlternatingMap.instTopologicalSpaceTotalSpace : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [Fintype ι] →
        {B : Type u_3} →
          [inst_2 : TopologicalSpace B] →
            {F₁ : Type u_4} →
              [inst_3 : NormedAddCommGroup F₁] →
                [inst_4 : NormedSpace 𝕜 F₁] →
                  {E₁ : B → Type u_5} →
                    [inst_5 : (x : B) → AddCommGroup (E₁ x)] →
                      [inst_6 : (x : B) → Module 𝕜 (E₁ x)] →
                        [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
                          [inst_8 : (x : B) → TopologicalSpace (E₁ x)] →
                            [inst_9 : FiberBundle F₁ E₁] →
                              [VectorBundle 𝕜 F₁ E₁] →
                                {F₂ : Type u_6} →
                                  [inst_11 : NormedAddCommGroup F₂] →
                                    [inst_12 : NormedSpace 𝕜 F₂] →
                                      {E₂ : B → Type u_7} →
                                        [inst_13 : (x : B) → AddCommGroup (E₂ x)] →
                                          [inst_14 : (x : B) → Module 𝕜 (E₂ x)] →
                                            [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                                              [inst_16 : (x : B) → TopologicalSpace (E₂ x)] →
                                                [inst_17 : FiberBundle F₂ E₂] →
                                                  [VectorBundle 𝕜 F₂ E₂] →
                                                    [∀ (x : B), IsTopologicalAddGroup (E₂ x)] →
                                                      [∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] →
                                                        TopologicalSpace
                                                          (Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x =>
                                                            E₁ x [⋀^ι]→L[𝕜] E₂ x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.ofList l cmp) k' = some v
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_mk_iff_exists_subset : ∀ {c : Cardinal.{u}} {α : Type u} {s : Set α}, c ≤ Cardinal.mk ↑s ↔ ∃ p ⊆ s, Cardinal.mk ↑p = c
-- Init.Data.SInt.Bitwise
ISize.xor_neg_one : ∀ {a : ISize}, a ^^^ -1 = ~~~a
-- Mathlib.Tactic.Linter.EmptyLine
/-- `filter stx f` takes as input a `Syntax` `stx` and a function `f : Syntax → Bool`.
It produces the array of the syntax nodes in `stx` where `f` is `true`.

See also the similar `filterMap` and `filterMapM`.
 -/
Lean.Syntax.filter : Lean.Syntax → (Lean.Syntax → Bool) → Array Lean.Syntax
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a positive constant, `fun x ↦ f x * r` tends to negative infinity along a filter
if and only if `f` tends to negative infinity along the same filter.  -/
Filter.tendsto_mul_const_atBot_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → (Filter.Tendsto (fun x => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.elimArgs : Lean.Elab.Tactic.ElimApp.Result → Array Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.whiskeringObj.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.CosimplicialObject.Augmented.whiskeringObj C D F =
    {
      obj := fun X =>
        { left := F.obj (CategoryTheory.CosimplicialObject.Augmented.point.obj X),
          right :=
            ((CategoryTheory.CosimplicialObject.whiskering C D).obj F).obj
              (CategoryTheory.CosimplicialObject.Augmented.drop.obj X),
          hom :=
            CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Functor.constComp SimplexCategory
                  (CategoryTheory.CosimplicialObject.Augmented.point.obj X) F).inv
              (CategoryTheory.Functor.whiskerRight X.hom F) },
      map := fun {X Y} η => { left := F.map η.left, right := CategoryTheory.Functor.whiskerRight η.right F, w := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.Set.Lattice
Set.sInter_empty : ∀ {α : Type u_1}, ⋂₀ ∅ = Set.univ
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.IsGE.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {t : CategoryTheory.Triangulated.TStructure C} {X : C} {n : ℤ}, t.ge n X → t.IsGE X n
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.exists_eval₂_eq_zero : ∀ {K : Type v} [inst : Field K] {k : Type u_1} [inst_1 : CommRing k] [IsSimpleRing k] [IsSepClosed K] (f : k →+* K)
  (p : Polynomial k), p.degree ≠ 0 → p.Separable → ∃ x, Polynomial.eval₂ f x p = 0
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instMulOfFintypeOfAddCommMonoid : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [Mul A] → [AddCommMonoid A] → Mul (CStarMatrix n n A)
-- Mathlib.Logic.Relation
Relation.EqvGen.rel : ∀ {α : Type u_1} {r : α → α → Prop} (x y : α), r x y → Relation.EqvGen r x y
-- Mathlib.Data.Fintype.Fin
OrderIso.symm.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.symm = RelIso.symm e
-- Init.Data.List.SplitOn.Basic
List.splitOnP_eq_splitOnPTR : @List.splitOnP = @List.splitOnPTR
-- Mathlib.RingTheory.Extension.ExtendScalars
/-- `Extension.extendScalars` does not change the cotangent space of an extension.  -/
Algebra.Extension.cotangentExtendScalarsEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → P.extendScalars.Cotangent ≃ₗ[S] P.Cotangent
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instCategoryWithFibrationsOpposite : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] → HomotopicalAlgebra.CategoryWithFibrations Cᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.lastDart.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (p p_1 : G.Walk v w) (e_p : p = p_1) (hp : ¬p.Nil),
  p.lastDart hp = p_1.lastDart ⋯
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.comap_eval_le_generateFrom_squareCylinders_singleton : ∀ {ι : Type u_2} (α : ι → Type u_1) [m : (i : ι) → MeasurableSpace (α i)] (i : ι),
  MeasurableSpace.comap (Function.eval i) (m i) ≤
    MeasurableSpace.generateFrom ((fun t => {i}.pi t) '' Set.univ.pi fun i => {s | MeasurableSet s})
-- Lean.Elab.Import
Lean.Elab.HeaderSyntax.toModuleHeader : Lean.Elab.HeaderSyntax → Lean.ModuleHeader
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.eval_apply_apply : ∀ {M : Type uM} {N : Type uN} [inst : MulOneClass M] [inst_1 : CommMonoid N] (y : M) (x : M →* N),
  (MonoidHom.eval y) x = x y
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.LocallyQuasiFinite g],
  AlgebraicGeometry.LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Elab.Match
/-- Given `stx` a match-expression, return its alternatives.  -/
Lean.Elab.Term.getMatchAlts : (k : Lean.SyntaxNodeKinds) → Lean.Syntax → Array (Lean.Elab.Term.MatchAltView k)
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset_6 : HAdd Std.Time.Duration Std.Time.Millisecond.Offset Std.Time.Duration
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.Ioo_eq_ball : ∀ (x y : ℝ), Set.Ioo x y = Metric.ball ((x + y) / 2) ((y - x) / 2)