mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.BanachSteinhaus
/-- This is the standard Banach-Steinhaus theorem, or Uniform Boundedness Principle.
If a family of continuous linear maps from a Banach space into a normed space is pointwise
bounded, then the norms of these linear maps are uniformly bounded.

See also `WithSeminorms.banach_steinhaus` for the general statement in barrelled spaces.  -/
banach_steinhaus : ∀ {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {𝕜₂ : Type u_4} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {ι : Type u_5}
  [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}, (∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C) → ∃ C', ∀ (i : ι), ‖g i‖ ≤ C'
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.duple.eq_1 : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R] (x y : M)
  {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1),
  Convexity.StdSimplex.duple x y hs ht h = { weights := (fun₀ | x => s) + fun₀ | y => t, nonneg := ⋯, total := ⋯ }
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.ofLeanSearchJson? : Lean.Json → Option LeanSearchClient.SearchResult
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (es : Std.DHashMap.Internal.AssocList α β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true),
  Std.DHashMap.Internal.AssocList.getKey a (Std.DHashMap.Internal.AssocList.cons k v es) h =
    if hka : (k == a) = true then k else Std.DHashMap.Internal.AssocList.getKey a es ⋯
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed additive group.  -/
IsUltrametricDist.nnnorm_sub_eq_max_of_nnnorm_sub_ne_nnnorm_sub : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x y z : S),
  ‖x - y‖₊ ≠ ‖y - z‖₊ → ‖x - z‖₊ = max ‖x - y‖₊ ‖y - z‖₊
-- Init.Data.SInt.Lemmas
Int8.toBitVec_zero : Int8.toBitVec 0 = 0#8
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.equiv_symm_algebraMap_left : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_6)
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [inst_11 : Algebra.IsPushout R S R' S'] (a : S),
  (Algebra.IsPushout.equiv R S R' S').symm ((algebraMap S S') a) = a ⊗ₜ[R] 1
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.closed_C : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (self : Urysohns.CU P), IsClosed self.C
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_and : ∀ (a b : UInt16), (a &&& b).toUInt64 = a.toUInt64 &&& b.toUInt64
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instFaithfulChangeProp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P P' : CategoryTheory.MorphismProperty T}
  {Q Q' : CategoryTheory.MorphismProperty A} {W W' : CategoryTheory.MorphismProperty B} (hP : P ≤ P') (hQ : Q ≤ Q')
  (hW : W ≤ W') [inst_3 : Q.IsMultiplicative] [inst_4 : Q'.IsMultiplicative] [inst_5 : W.IsMultiplicative]
  [inst_6 : W'.IsMultiplicative], (CategoryTheory.MorphismProperty.Comma.changeProp L R hP hQ hW).Faithful
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- A module object for a monoid object in a monoidal category acting on the
ambient category.  -/
CategoryTheory.Mod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (D : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) → [CategoryTheory.MonObj A] → Type (max u₂ v₂)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocDiv hp a (b + ↑m * p) = toIocDiv hp a b + ↑m
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- The map from the direct sum of prime spectra to the prime spectrum of a direct product.  -/
PrimeSpectrum.primeSpectrumProdOfSum : (R : Type u) →
  (S : Type v) →
    [inst : CommSemiring R] → [inst_1 : CommSemiring S] → PrimeSpectrum R ⊕ PrimeSpectrum S → PrimeSpectrum (R × S)
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.List.lookup.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : α → List (α × β) → Sort u_3) (x : α) (h_1 : (x : α) → motive x [])
  (h_2 : (a k : α) → (b : β) → (as : List (α × β)) → motive a ((k, b) :: as)),
  (match x, [] with
    | x, [] => h_1 x
    | a, (k, b) :: as => h_2 a k b as) =
    h_1 x
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- An additive character is *primitive* iff all its multiplicative shifts by nonzero
elements are nontrivial.  -/
AddChar.IsPrimitive : {R : Type u} → [inst : CommRing R] → {R' : Type v} → [inst_1 : CommMonoid R'] → AddChar R R' → Prop
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sub : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ {s t : T}, ProbabilityTheory.HasGaussianLaw (X s - X t) P
-- Batteries.Logic
not_nonempty_empty : ¬Nonempty Empty
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_mono_infEDist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) {E : Set α} {x y : α},
  Metric.infEDist x E ≤ Metric.infEDist y E → thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeff_mul_le : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] (I J : Ideal (Polynomial R)),
  I.leadingCoeff * J.leadingCoeff ≤ (I * J).leadingCoeff
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.iso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (i : P ≅ Q),
  CategoryTheory.Projective P ↔ CategoryTheory.Projective Q
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_iff : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (p : Polynomial R) (n : ℕ),
  p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1
-- Mathlib.Order.SuccPred.Tree
/-- The immediate subtree of `t` containing `v`, or all of `t` if `v` is the root.
 -/
RootedTree.subtreeOf : (t : RootedTree) → [DecidableEq ↑t] → ↑t → SubRootedTree t
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hasForgetToAlgCat : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (CommAlgCat R) (AlgCat R)
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinal_iInter_mem : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s : ι → Set α},
  Cardinal.mk ι < c → (⋂ i, s i ∈ l ↔ ∀ (i : ι), s i ∈ l)
-- Lean.Parser.Extra
Lean.Parser.ppSpace.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
ModuleCat.projectiveDimension_eq_of_linearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N),
  CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N
-- Mathlib.Order.WellQuasiOrder
IsAntichain.finite_of_wellQuasiOrdered : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → WellQuasiOrdered r → s.Finite
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.congr_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → ∀ {t : Set E}, nhdsWithin x s = nhdsWithin x t → DifferentiableWithinAt 𝕜 f t x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.proj_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F}, x ∈ e.target → proj (↑e.symm x) = x.1
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.GenerateMeasurable.below.empty : ∀ {α : Type u_1} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.GenerateMeasurable s a → Prop},
  MeasurableSpace.GenerateMeasurable.below ⋯
-- Mathlib.Algebra.Order.AddTorsor
Monotone.smul : ∀ {G : Type u_1} {P : Type u_2} {γ : Type u_3} [inst : Preorder G] [inst_1 : Preorder P] [inst_2 : Preorder γ]
  [inst_3 : SMul G P] [IsOrderedSMul G P] {f : γ → G} {g : γ → P}, Monotone f → Monotone g → Monotone fun x => f x • g x
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instBool : Lean.Elab.ConfigEval.EvalExpr Bool
-- Mathlib.RingTheory.Discriminant
/-- Relation between `Algebra.discr A ι b` and
`Algebra.discr A (b ᵥ* P.map (algebraMap A B))`.  -/
Algebra.discr_of_matrix_vecMul : ∀ {A : Type u} {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B) (P : Matrix ι ι A),
  Algebra.discr A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.det ^ 2 * Algebra.discr A b
-- Mathlib.Algebra.Lie.Subalgebra
/-- The embedding of a Lie subalgebra into the ambient space as a morphism of Lie algebras.  -/
LieSubalgebra.incl : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (L' : LieSubalgebra R L) → ↥L' →ₗ⁅R⁆ L
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.exactAt_iff' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι),
  c.prev j = i → c.next j = k → (K.ExactAt j ↔ (K.sc' i j k).Exact)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_iff_toList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.pi_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] {γ : Type w} [Nonempty I]
  [inst_2 : AddZeroClass γ] (g : (i : I) → γ →+ f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddMonoidHom.pi g)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instBEq : {α : Type u_1} → [BEq α] → BEq (RBTree.RBNode α)
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.mul.sizeOf_spec : ∀ (a b : Nat.Internal.SOM.Expr), sizeOf (a.mul b) = 1 + sizeOf a + sizeOf b
-- Mathlib.Data.List.Basic
List.IsPrefix.idxOf_le : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α], l₁ <+: l₂ → ∀ (a : α), List.idxOf a l₁ ≤ List.idxOf a l₂
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryEquivClass.norm_map : ∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} {inst : Semiring R} {inst_1 : Semiring R₂}
  {σ₁₂ : outParam (R →+* R₂)} {σ₂₁ : outParam (R₂ →+* R)} {inst_2 : RingHomInvPair σ₁₂ σ₂₁}
  {inst_3 : RingHomInvPair σ₂₁ σ₁₂} {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)}
  {inst_4 : SeminormedAddCommGroup E} {inst_5 : SeminormedAddCommGroup E₂} {inst_6 : Module R E} {inst_7 : Module R₂ E₂}
  {inst_8 : EquivLike 𝓕 E E₂} [self : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E), ‖f x‖ = ‖x‖
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Fin.accumulate_last : ∀ {i n m : ℕ} (hin : i < n) (hmi : m = i + 1) (t : Fin n → ℕ),
  (∀ (j : Fin n), m ≤ ↑j → t j = 0) → (Fin.accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩
-- Mathlib.Data.Set.Lattice
Set.Iic_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} [inst : CompleteLattice α] (f : (i : ι) → κ i → α),
  Set.Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Set.Iic (f i j)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.MeasurePreserving.lintegral_map_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} (f : β → ENNReal) (g : α ≃ᵐ β),
  MeasureTheory.MeasurePreserving (⇑g) μ ν → ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ
-- Mathlib.Analysis.LConvolution
/-- Scoped notation for the multiplicative convolution of functions with respect to `volume`.  -/
MeasureTheory.«term_⋆ₘₗ_» : Lean.TrailingParserDescr
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomain_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {p : ι → Prop} [inst_1 : DecidablePred p],
  DFinsupp.subtypeDomain p 0 = 0
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemCont.mk.sizeOf_spec : ∀ (resultName : Lean.Name) (resultType : Lean.Expr) (k : Lean.Elab.Do.DoElabM Lean.Expr)
  (kind : Lean.Elab.Do.DoElemContKind),
  sizeOf { resultName := resultName, resultType := resultType, k := k, kind := kind } =
    1 + sizeOf resultName + sizeOf resultType + sizeOf kind
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_filterMap_le_size : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ}, m.WF → (Std.HashMap.Raw.filterMap f m).size ≤ m.size
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.reindex_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V]
  [inst_1 : AddTorsor V P] [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i' : ι'),
  (b.reindex e) i' = b (e.symm i')
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂.eq_1 : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (L : CategoryTheory.Functor C D) {F F' : CategoryTheory.Functor C H} (iso₂ : F ≅ F'),
  L.leftExtensionEquivalenceOfIso₂ iso₂ = CategoryTheory.StructuredArrow.mapIso iso₂
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- If `p` lies strictly between `p₁` and `p₂` on one line and strictly between `p₃` and `p₄`
on another line, and if `dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p`,
then the points `p₁`, `p₂`, `p₃`, and `p₄` are cospherical.  -/
EuclideanGeometry.cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ p₄ p : P},
  dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p →
    EuclideanGeometry.angle p₁ p p₂ = Real.pi →
      EuclideanGeometry.angle p₃ p p₄ = Real.pi →
        ¬Collinear ℝ {p₁, p, p₃} → EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubgroup_empty : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α], fixingAddSubgroup M ∅ = ⊤
-- Mathlib.Topology.Separation.Regular
Filter.HasBasis.nhdsSet_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {ι : Sort u_3} {u : Set X} {p : ι → Prop} {s : ι → Set X},
  IsClosed u → (nhdsSet u).HasBasis p s → (nhdsSet u).HasBasis p fun i => closure (s i)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copy_IsBase : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E)
  (hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (hI : ∀ (I : Set α), Indep I ↔ M.Indep I) (a : Set α),
  (M.copy E IsBase Indep hE hB hI).IsBase a = IsBase a
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLT.eq_def : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α),
  Std.DTreeMap.Internal.Impl.pruneLT✝ t lowerBound =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner sz k v l r =>
      match compare lowerBound k with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k v (Std.DTreeMap.Internal.Impl.pruneLT✝ l lowerBound) r
      | Ordering.eq => r
      | Ordering.gt => Std.DTreeMap.Internal.Impl.pruneLT✝ r lowerBound
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.maxEntry?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntry? = t₂.maxEntry?
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_mk : ∀ (z : ℂ) (h : 0 < z.im), ↑{ coe := z, coe_im_pos := h } = z
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_cast_Ico : ∀ {n m : ℕ} (h : n = m) (i j : Fin n),
  Finset.image (Fin.cast h) (Finset.Ico i j) = Finset.Ico (Fin.cast h i) (Fin.cast h j)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_mk_eq_max' : ∀ {α β : Type u} [Infinite β], Cardinal.mk α + Cardinal.mk β = max (Cardinal.mk α) (Cardinal.mk β)
-- Mathlib.Algebra.Order.Module.Defs
IsStrictOrderedModule.toSMulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  {inst_4 : Zero β} [self : IsStrictOrderedModule α β], SMulPosStrictMono α β
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.congrRight` as an `AlgEquiv`.  -/
LocallyConstant.congrRightₐ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        (R : Type u_7) →
          [inst_1 : CommSemiring R] →
            [inst_2 : Semiring Y] →
              [inst_3 : Algebra R Y] →
                [inst_4 : Semiring Z] →
                  [inst_5 : Algebra R Z] → (Y ≃ₐ[R] Z) → LocallyConstant X Y ≃ₐ[R] LocallyConstant X Z
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).getKey? k = if k ∈ t₂ then t₁.getKey? k else none
-- Mathlib.Topology.Sober
genericPoints.equiv_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T0Space α] [inst_2 : QuasiSober α] (x : ↑(genericPoints α)),
  genericPoints.equiv x = genericPoints.component x
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.finsupp_var : ∀ {A : Type u} [inst : Ring A] {N : Type v} [inst_1 : AddCommGroup N] [inst_2 : Module A N]
  (pres : Module.Presentation A N) (ι : Type w) [inst_3 : DecidableEq ι] [inst_4 : DecidableEq N] (i : ι) (g : pres.G),
  (pres.finsupp ι).var ⟨i, g⟩ = fun₀ | i => pres.var g
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- A typeclass mixin for `MeasurableSpace`s such that all sets are measurable.  -/
DiscreteMeasurableSpace : (α : Type u_7) → [MeasurableSpace α] → Prop
-- Mathlib.Data.Set.SMulAntidiagonal
Set.vaddAntidiagonal_mono_left : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s₁ s₂ : Set G} {t : Set P} {a : P},
  s₁ ⊆ s₂ → s₁.vaddAntidiagonal t a ⊆ s₂.vaddAntidiagonal t a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} [inst_1 : Inhabited (β k)],
  (Std.DHashMap.filter f m).get! k = (Option.filter (f k) (m.get? k)).get!
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_mul_add_one : ∀ {a b : Ordinal.{u_4}} (c : Ordinal.{u_4}), b + a = a → (a + b) * (c + 1) = a * (c + 1) + b
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonUnitalRing : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [NonUnitalRing β] → NonUnitalRing (MeasureTheory.SimpleFunc α β)
-- Mathlib.Data.Nat.Nth
Nat.nth_le_nth : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → ∀ {k n : ℕ}, Nat.nth p k ≤ Nat.nth p n ↔ k ≤ n
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.restrict_scalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NontriviallyNormedField 𝕜']
  [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F], ContDiffWithinAt 𝕜' n f s x → ContDiffWithinAt 𝕜 n f s x
-- Mathlib.RingTheory.Smooth.Kaehler
retractionOfSectionOfKerSqZero.congr_simp : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S]
  (g g_1 : S →ₐ[R] P) (e_g : g = g_1) (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥)
  (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S),
  retractionOfSectionOfKerSqZero g hf' hg = retractionOfSectionOfKerSqZero g_1 hf' ⋯
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.mem_submodule : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M) (f : PolynomialModule R M), f ∈ F.submodule ↔ ∀ (i : ℕ), f.coeff i ∈ F.N i
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddAction'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M β],
  Filter.Germ.instAddAction' = { toVAdd := Filter.Germ.instVAdd', add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable.mk : ∀ {b : ByteArray} {v : Array ℕ} (size_le : v.size ≤ b.size),
  (∀ (i : ℕ) (hi : i < v.size), v[i] = String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ b i ⋯) →
    String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ b v
-- Mathlib.Order.Closure
LowerAdjoint.mk.inj : ∀ {α : Type u_1} {β : Type u_4} {inst : Preorder α} {inst_1 : Preorder β} {u : β → α} {toFun : α → β}
  {gc' : GaloisConnection toFun u} {toFun_1 : α → β} {gc'_1 : GaloisConnection toFun_1 u},
  { toFun := toFun, gc' := gc' } = { toFun := toFun_1, gc' := gc'_1 } → toFun = toFun_1
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.uniqueBot : {R : Type u_1} → {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Unique ↥⊥
-- Batteries.Data.PairingHeap
/-- A forest consists of a root `a`, a forest `child` elements greater than `a`,
and another forest `sibling`.  -/
Batteries.PairingHeapImp.Heap.node : {α : Type u} → α → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α
-- Aesop.Options.Public
/-- (aesop) Warn when apply builder is applied to a rule with conclusion of the form A ↔ B.
 -/
Aesop.aesop.warn.applyIff : Lean.Option Bool
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_linearCombination : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (v : ι →₀ R), b.repr ((Finsupp.linearCombination R ⇑b) v) = v