mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Get the tail of the binomial heap after removing the minimum element.  -/
Batteries.BinomialHeap.Imp.Heap.tail? : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → Option (Batteries.BinomialHeap.Imp.Heap α)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.continuous_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α), Continuous pkg.coe
-- Mathlib.Order.Bounds.Image
isLUB_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set (α × β)} {p : α × β},
  IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.ComposableArrows.threeδ₂Toδ₁.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ f₂_1 : j ⟶ k) (e_f₂ : f₂ = f₂_1)
  (f₃ : k ⟶ l) (f₁₂ : i ⟶ k) (f₂₃ : j ⟶ l) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃),
  CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ =
    CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂_1 f₃ f₁₂ f₂₃ ⋯ ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `univ α ≃ α` as measurable spaces.  -/
MeasurableEquiv.Set.univ : (α : Type u_6) → [inst : MeasurableSpace α] → ↑Set.univ ≃ᵐ α
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.tail_map : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ')
  (l : Turing.ListBlank Γ), (Turing.ListBlank.map f l).tail = Turing.ListBlank.map f l.tail
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
UniformContinuousOn.comp_tendstoLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β]
  {F : ι → α → β} {f : α → β} {p : Filter ι} [inst_2 : UniformSpace γ] {g : β → γ} {t : Set β},
  UniformContinuousOn g t →
    TendstoLocallyUniformly F f p →
      (∀ (x : α), f x ∈ t) →
        (∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t) → TendstoLocallyUniformly (fun x => g ∘ F x) (g ∘ f) p
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesColimit₂.nonempty_isColimit_mapCocone₂ : ∀ {J₁ : Type u_1} {J₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} J₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} J₂} {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C₁} {inst_3 : CategoryTheory.Category.{v_4, u_4} C₂}
  {inst_4 : CategoryTheory.Category.{v_5, u_5} C} {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)}
  [self : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cocone K₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone K₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂), Nonempty (CategoryTheory.Limits.IsColimit (G.mapCocone₂ c₁ c₂))
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Let `K : ι → Set X` be a locally finite family of closed sets in an emetric space. Let
`U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then for any point
`x : X`, for sufficiently small `r : ℝ≥0∞` and for `y` sufficiently close to `x`, for all `i`, if
`y ∈ K i`, then `Metric.closedEBall y r ⊆ U i`.  -/
Metric.eventually_nhds_zero_forall_closedEBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∀ (x : X), ∀ᶠ (p : ENNReal × X) in nhds 0 ×ˢ nhds x, ∀ (i : ι), p.2 ∈ K i → Metric.closedEBall p.2 p.1 ⊆ U i
-- Std.Data.ExtDHashMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.ExtDHashMap.Const.modify : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [EquivBEq α] →
        [LawfulHashable α] → {β : Type v} → (Std.ExtDHashMap α fun x => β) → α → (β → β) → Std.ExtDHashMap α fun x => β
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Build an isomorphism in the category `CommHopfAlgCat R` from a `BialgEquiv` between
`HopfAlgebra`s.  -/
CommHopfAlgCat.isoMk : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      {x : CommRing X} →
        {x_1 : CommRing Y} →
          {x_2 : HopfAlgebra R X} →
            {x_3 : HopfAlgebra R Y} →
              (X ≃ₐc[R] Y) →
                ({ X := X, commRing := x, hopfAlgebra := x_2 } ≅ { X := Y, commRing := x_1, hopfAlgebra := x_3 })
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Basis.prod_apply_inr_fst : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι'), ((b.prod b') (Sum.inr i)).1 = 0
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_lt_of_lt_mul_inv : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < c → a < b * c⁻¹ → a * c < b
-- Mathlib.RingTheory.MvPolynomial.Groebner
/-- Reduce a polynomial modulo a polynomial with unit leading term (for some monomial order)  -/
MonomialOrder.reduce : {σ : Type u_1} →
  (m : MonomialOrder σ) →
    {R : Type u_2} →
      [inst : CommRing R] → {b : MvPolynomial σ R} → IsUnit (m.leadingCoeff b) → MvPolynomial σ R → MvPolynomial σ R
-- Init.Data.List.MinMaxOn
List.le_apply_minOn_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []) {b : β}, b ≤ f (List.minOn f xs h) ↔ ∀ x ∈ xs, b ≤ f x
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_eq_zero_of_subsingleton : ∀ {α : Type u_1} {G : SimpleGraph α} [Subsingleton α], G.ediam = 0
-- Std.Time.Duration
_private.Std.Time.Duration.0.Std.Time.Duration.ofNanoseconds.tdiv_neg : ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → a.tdiv b ≤ 0
-- Init.Data.UInt.Lemmas
UInt16.sub_eq_add_neg : ∀ (a b : UInt16), a - b = a + -b
-- Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
/-- The isomorphism between the kernel of the zeroth differential and
the invariants of a representation.  -/
ContinuousCohomology.d₀kerIso : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              (X : TopRep k G) → ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker ≃L[k] ↥X.ρ.invariants
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associativity_unitIso : ∀ (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],
  (CategoryTheory.prod.associativity C D E).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id ((C × D) × E))
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable on `(∞, a]`, and `f =O[atBot] g`, for some
`g` integrable at `atBot`, then `f` is integrable on `(∞, a]`.  -/
MeasureTheory.LocallyIntegrableOn.integrableOn_of_isBigO_atBot : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F} {a : α}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : LinearOrder α] [CompactIccSpace α] [Filter.atBot.IsMeasurablyGenerated],
  MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ →
    f =O[Filter.atBot] g →
      MeasureTheory.IntegrableAtFilter g Filter.atBot μ → MeasureTheory.IntegrableOn f (Set.Iic a) μ
-- Mathlib.Analysis.Normed.Field.Lemmas
NormedField.continuousAt_inv : ∀ {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, ContinuousAt Inv.inv x ↔ x ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.bypass_isPath : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), p.bypass.IsPath
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.brecOn : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N}
  {motive : (a a_1 : List (Symbol T N)) → r.Rewrites a a_1 → Prop} {a a_1 : List (Symbol T N)} (t : r.Rewrites a a_1),
  (∀ (a a_2 : List (Symbol T N)) (t : r.Rewrites a a_2), ContextFreeRule.Rewrites.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.cechConerve_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (n : SimplexCategory),
  f.cechConerve.obj n = CategoryTheory.Limits.widePushout f.left (fun x => f.right) fun x => f.hom
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State.mk.injEq : ∀ (patterns : Array Lean.Expr) (done : Bool) (patterns_1 : Array Lean.Expr) (done_1 : Bool),
  ({ patterns := patterns, done := done } = { patterns := patterns_1, done := done_1 }) =
    (patterns = patterns_1 ∧ done = done_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.face_le_horn_iff : ∀ {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)),
  SSet.stdSimplex.face S ≤ SSet.horn (n + 1) j ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ
-- Mathlib.Data.Real.ConjExponents
NNReal.holderTriple_iff : ∀ (p q r : NNReal), p.HolderTriple q r ↔ p⁻¹ + q⁻¹ = r⁻¹ ∧ 0 < p ∧ 0 < q
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_eq_toSignedMeasure_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν], μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.adj_unit_app : ∀ (X : CategoryTheory.Cat), CategoryTheory.Codiscrete.adj.unit.app X = (CategoryTheory.Codiscrete.unitApp ↑X).toCatHom
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((a : α) × β a)} {k a : α}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = true} (hl : Std.Internal.List.DistinctKeys l),
  Std.Internal.List.getKey a (Std.Internal.List.eraseKey k l) h = Std.Internal.List.getKey a l ⋯
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_sum_le_of_forall_le : ∀ {ι : Type w} (s : Finset ι) {S : Type u_1} [inst : Semiring S] {n : ℕ} (f : ι → Polynomial S),
  (∀ i ∈ s, (f i).natDegree ≤ n) → (∑ i ∈ s, f i).natDegree ≤ n
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux_X : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  (Q : Algebra.Generators S T ι) (i : ι), (Algebra.Generators.H1Cotangent.δAux R Q) (MvPolynomial.X i) = 0
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is full on `R`-Hopf algebras.  -/
AlgebraicGeometry.hopfSpec.instFull : ∀ {R : CommRingCat}, (AlgebraicGeometry.hopfSpec R).Full
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.instFintypeOne : {α : Type u_2} → [inst : One α] → Fintype ↑1
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeRule.sizeOf_spec : ∀ (r : Aesop.SafeRule), sizeOf (Aesop.BaseRuleSetMember.safeRule r) = 1 + sizeOf r
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.isSetBernoulli_congr : ∀ {ι : Type u_1} {Ω : Type u_2} {m : MeasurableSpace Ω} {X Y : Ω → Set ι} {u : Set ι} {p : ↑unitInterval}
  {P : MeasureTheory.Measure Ω},
  X =ᵐ[P] Y → (ProbabilityTheory.IsSetBernoulli X u p P ↔ ProbabilityTheory.IsSetBernoulli Y u p P)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems : Type
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.reflectsColimitsOfShape : ∀ (R : Type w) [inst : Ring R] (J : Type u) [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat],
  CategoryTheory.Limits.ReflectsColimitsOfShape J (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.baseEmbedding_le_sSupFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {c : Set (HahnEmbedding.Partial seed)},
  c.Nonempty → ∀ (hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c), seed.baseEmbedding ≤ HahnEmbedding.Partial.sSupFun hc
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.zero_comp : ∀ {E : Type u_3} {F : Type u_4} [inst : AddGroup E] [inst_1 : AddGroup F] (f : F →+ E), AddGroupSeminorm.comp 0 f = 0
-- Mathlib.Order.Cover
not_covBy_iff_nonempty_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → (¬a ⋖ b ↔ (Set.Ioo a b).Nonempty)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.containsThenInsertIfNew.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → t.containsThenInsertIfNew a b = t_1.containsThenInsertIfNew a b_1
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr_smul : ∀ {R : Type u_3} {N : Type u_5} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] {b : Module.Basis n R N}
  {Q : QuadraticForm R N} (a : R), QuadraticForm.discr b (a • Q) = a ^ Fintype.card n * QuadraticForm.discr b Q
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Extended distance between two points  -/
PseudoMetricSpace.edist : {α : Type u} → [self : PseudoMetricSpace α] → α → α → ENNReal
-- Init.Data.Range.Polymorphic.RangeIterator
/-- The pure function mapping a range iterator of type `Iter` to the next step of the iterator.
 -/
Std.Rxi.Iterator.step : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Iter α → Std.IterStep (Std.Iter α) α
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₃'.congr_simp : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))))
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂ =
    X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂
-- Std.Time.Zoned.ZoneRules
/-- Create a TimeZone from a Transition.
 -/
Std.Time.TimeZone.Transition.createTimeZoneFromTransition : Std.Time.TimeZone.Transition → Std.Time.TimeZone
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.exists_mem_nhds : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u → ∀ (a : X), ∃ i, ↑(u i) ∈ nhds a
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f g : M ≃+ N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_mono : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} [L.NeBot],
  Summable f L → Summable g L → f ≤ g → ∑'[L] (n : ι), f n ≤ ∑'[L] (n : ι), g n
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- `NonUnitalSubring` closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
NonUnitalSubring.closure_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] ⦃s t : Set R⦄,
  s ⊆ t → NonUnitalSubring.closure s ≤ NonUnitalSubring.closure t
-- Mathlib.Algebra.Ring.Action.Group
MulSemiringAction.toRingEquiv_apply_symm_apply : ∀ (G : Type u_1) [inst : Group G] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (x : G) (a : R),
  ((MulSemiringAction.toRingEquiv G R) x).symm a = x⁻¹ • a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedGeneratorNode : Inhabited Lean.Meta.SynthInstance.GeneratorNode
-- Lean.Parser.Types
/-- Maximal (and function application) precedence.
In the standard lean language, no parser has precedence higher than `maxPrec`.

Note that nothing prevents users from using a higher precedence, but we strongly
discourage them from doing it.  -/
Lean.Parser.maxPrec : ℕ
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.inl_apply : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (i : M₁),
  (QuadraticMap.Isometry.inl Q₁ Q₂) i = (i, 0)
-- Mathlib.Order.BoundedOrder.Monotone
StrictAnti.apply_eq_top_iff : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : Preorder β] {f : α → β} {a : α},
  StrictAnti f → (f a = f ⊤ ↔ a = ⊤)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α}, k ∈ Std.ExtDHashMap.Const.ofList l ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instCommSemigroup : {𝕜 : Type u_1} → [inst : SeminormedCommRing 𝕜] → CommSemigroup ↑(Metric.ball 0 1)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.rootSet_C_mul_X_pow : ∀ {R : Type u} {S : Type v} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra R S] {n : ℕ},
  n ≠ 0 → ∀ {a : R}, a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).rootSet S = {0}
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Convert a multiseries to a function.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.toFun : {basis : Tactic.ComputeAsymptotics.Basis} → Tactic.ComputeAsymptotics.MultiseriesExpansion basis → ℝ → ℝ
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_of_le_one : ∀ {o : Ordinal.{u}}, o ≤ 1 → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Mathlib.Order.Hom.Lattice
LatticeHom.subtypeVal_coe : ∀ {β : Type u_3} [inst : Lattice β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y))
  (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)), ⇑(LatticeHom.subtypeVal Psup Pinf) = Subtype.val
-- Mathlib.Data.Matrix.Composition
Matrix.comp_map_transpose : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)),
  (Matrix.comp I J L K R) (M.map fun x => x.transpose) = ((Matrix.comp J I K L R) M.transpose).transpose
-- Std.Sync.RecursiveMutex
/-- Unlocks a `BaseRecursiveMutex`. The owning thread must make as many `unlock` calls as `lock` and
`tryLock` calls in order to fully relinquish ownership of the mutex.

The current thread must have already locked the mutex at least once.
Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseRecursiveMutex.unlock : Std.BaseRecursiveMutex → BaseIO Unit
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Additive.toMul_le`. -/
Additive.toMul_mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : Additive α}, a ≤ b → Additive.toMul a ≤ Additive.toMul b
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_add_const_Icc : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => x + a) '' Set.Icc b c = Set.Icc (b + a) (c + a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.keys_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → Bool},
  (Std.TreeMap.filter (fun k x => f k) t).keys = List.filter f t.keys
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.get?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, t₁.Equiv t₂ → t₁.get? k = t₂.get? k
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_norm : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup α] [OpensMeasurableSpace α], Measurable norm
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.ofModuleMonoidAlgebra_obj_coe : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] (M : ModuleCat (MonoidAlgebra k G)),
  ↑(Rep.ofModuleMonoidAlgebra.obj M) = RestrictScalars k (MonoidAlgebra k G) ↑M
-- Mathlib.RingTheory.Finiteness.Small
Algebra.FiniteType.small : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Small.{u, u_1} R] [Algebra.FiniteType R S], Small.{u, u_2} S
-- Mathlib.Geometry.Manifold.BumpFunction
/-- Given a smooth manifold modelled on a finite-dimensional space `E`,
`f : SmoothBumpFunction I M` is a smooth function on `M` such that in the extended chart `e` at
`f.c`:

* `f x = 1` in the closed ball of radius `f.rIn` centered at `f.c`;
* `f x = 0` outside of the ball of radius `f.rOut` centered at `f.c`;
* `0 ≤ f x ≤ 1` for all `x`.

The structure contains data required to construct a function with these properties. The function is
available as `⇑f` or `f x`. Formal statements of the properties listed above involve some
(pre)images under `extChartAt I f.c` and are given as lemmas in the `SmoothBumpFunction`
namespace.  -/
SmoothBumpFunction : {E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          ModelWithCorners ℝ E H → {M : Type uM} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Type
-- Init.Data.UInt.Bitwise
UInt8.not_inj : ∀ {a b : UInt8}, ~~~a = ~~~b ↔ a = b
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.tidy?.match_1.eq_1 : ∀ (motive : Option (Lean.Omega.Constraint × Lean.Omega.Coeffs) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (s' : Lean.Omega.Constraint) → (x' : Lean.Omega.Coeffs) → motive (some (s', x'))),
  (match none with
    | none => h_1 ()
    | some (s', x') => h_2 s' x') =
    h_1 ()
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_comp_of_injective : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Ring R] [inst_1 : Semiring S] [inst_2 : Semiring T] (g : T →+* R)
  {f : R →+* S}, Function.Injective ⇑f → RingHom.ker (f.comp g) = RingHom.ker g
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.reflexion_comp_right : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion
    CategoryTheory.Limits.WalkingReflexivePair.Hom.right =
  CategoryTheory.CategoryStruct.id CategoryTheory.Limits.WalkingReflexivePair.zero
-- Mathlib.Algebra.Group.ULift
ULift.group : {α : Type u} → [Group α] → Group (ULift.{u_1, u} α)
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.toSubsemiringClass : ∀ {S : Type u_1} {R : outParam (Type u)} {inst : NonAssocRing R} {inst_1 : SetLike S R} [self : SubringClass S R],
  SubsemiringClass S R