mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.IsPrimePow
isPrimePow_nat_iff_bounded_log : ∀ (n : ℕ), IsPrimePow n ↔ ∃ k ≤ Nat.log 2 n, 0 < k ∧ ∃ p ≤ n, n = p ^ k ∧ Nat.Prime p
-- Init.Classical
Classical.exists_or_forall_not : ∀ {α : Sort u_1} (P : α → Prop), (∃ a, P a) ∨ ∀ (a : α), ¬P a
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalFactorizationRing.factor₁_mul_factor₂ : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  ↑(Polynomial.UniversalFactorizationRing.factor₁ m k hn p) *
      ↑(Polynomial.UniversalFactorizationRing.factor₂ m k hn p) =
    ↑(Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p)
-- Mathlib.Order.RelSeries
RelSeries.append_length : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r),
  (p.append q connect).length = p.length + q.length + 1
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrixAux_apply : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} (B : LinearMap.BilinForm R₁ M₁) (b : n → M₁) (i j : n),
  (LinearMap.BilinForm.toMatrixAux b) B i j = (B (b i)) (b j)
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
affineSpan_eq_top_of_nonempty_interior : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {s : Set V},
  (interior ((convexHull ℝ) s)).Nonempty → affineSpan ℝ s = ⊤
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_of_subset_diagSet : ∀ {V : Type u_1} {s : Set (Sym2 V)} (G : SimpleGraph V), s ⊆ Sym2.diagSet → G.deleteEdges s = G
-- Lean.Data.Lsp.Extra
/-- `$/lean/moduleHierarchy/importedBy` client->server request.

Response type: `Array LeanImport`
 -/
Lean.Lsp.LeanModuleHierarchyImportedByParams : Type
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_mul_le : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal} [f.NeBot],
  0 ≤ᶠ[f] u →
    0 ≤ᶠ[f] v →
      Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤ →
        Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0 → Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.Discrete.sumEquiv.match_1.eq_1 : ∀ {J : Type u_1} {K : Type u_2} (motive : J ⊕ K → Sort u_3) (j : J) (h_1 : (j : J) → motive (Sum.inl j))
  (h_2 : (k : K) → motive (Sum.inr k)),
  (match Sum.inl j with
    | Sum.inl j => h_1 j
    | Sum.inr k => h_2 k) =
    h_1 j
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.stdGaussian_map : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {F : Type u_3} [inst_5 : NormedAddCommGroup F]
  [inst_6 : InnerProductSpace ℝ F] [inst_7 : MeasurableSpace F] [BorelSpace F] (f : E ≃ₗᵢ[ℝ] F),
  MeasureTheory.Measure.map (⇑f) (ProbabilityTheory.stdGaussian E) = ProbabilityTheory.stdGaussian F
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
point, and all functions in the series are differentiable with a summable bound on the derivatives,
then the series is differentiable and its derivative is the sum of the derivatives.  -/
hasDerivAt_tsum : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {y₀ : 𝕜},
  Summable u →
    (∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) →
      (∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) →
        (Summable fun n => g n y₀) → ∀ (y : 𝕜), HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul_nc.go.eq_def : ∀ (p₂ p₁ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ acc =
    match p₁ with
    | Lean.Grind.CommRing.Poly.num k => acc.combine (Lean.Grind.CommRing.Poly.mulConst k p₂)
    | Lean.Grind.CommRing.Poly.add k m p₁ =>
      Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ (acc.combine (Lean.Grind.CommRing.Poly.mulMon_nc k m p₂))
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : N ≃* P} (x : N),
  (f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k)) x = k x
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.norm_mul_sin_arg : ∀ (x : ℂ), ‖x‖ * Real.sin x.arg = x.im
-- Lean.Widget.InteractiveDiagnostic
/-- An interactive goal display.  -/
Lean.Widget.MsgEmbed.goal : Lean.Widget.InteractiveGoal → Lean.Widget.MsgEmbed
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `B` is a faithfully flat `A`-module and `M` is any `A`-module, the canonical
map `M →ₗ[A] B ⊗[A] M` is injective.

See also `Module.Flat.tensorProduct_mk_injective`.  -/
Module.FaithfullyFlat.tensorProduct_mk_injective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B] (M : Type u_3) [inst_4 : AddCommGroup M] [inst_5 : Module A M],
  Function.Injective ⇑((TensorProduct.mk A B M) 1)
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- The inclusion of the image sheaf to the target.  -/
CategoryTheory.Sheaf.imageι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F F' : CategoryTheory.Sheaf J (Type w)} → (f : F ⟶ F') → CategoryTheory.Sheaf.image f ⟶ F'
-- Lean.Meta.Tactic.Grind.Types
/-- `hasLambdas := true` if the equivalence class contains lambda expressions.  -/
Lean.Meta.Grind.ENode.hasLambdas : Lean.Meta.Grind.ENode → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.right.sizeOf_spec : sizeOf CategoryTheory.Limits.WalkingPair.right = 1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_inv_hom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y),
  CategoryTheory.CategoryStruct.comp (F.map f.inv) (F.map f.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_map_toList : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M), (List.map f s.toList).prod = s.prod f
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The homotopy group at `x` indexed by a singleton is isomorphic to the fundamental group,
i.e. the loops based at `x` up to homotopy.  -/
HomotopyGroup.homotopyGroupOfUniqueMulEquivFundamentalGroup : {X : Type u_2} →
  [inst : TopologicalSpace X] →
    {x : X} → (N : Type u_3) → [inst_1 : Unique N] → HomotopyGroup N X x ≃* FundamentalGroup X x
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.unify_sigma_mk_self : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [DirectedSystem G fun i j h => ⇑(f i j h)] {α : Type u_1} {i : ι}
  {x : α → G i},
  FirstOrder.Language.DirectLimit.unify f (fun a => FirstOrder.Language.Structure.Sigma.mk f i (x a)) i ⋯ = x
-- Init.Data.Nat.Basic
Nat.lt_add_one_of_lt : ∀ {a b : ℕ}, a < b → a < b + 1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_subset_div_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s t : Finset α}, 1 ∈ s → t⁻¹ ⊆ s / t
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instOrderTopOfOrderBot.eq_1 : ∀ (α : Type u) [inst : LE α] [h : OrderBot α],
  OrderDual.instOrderTopOfOrderBot α = { toTop := OrderDual.instTopOfBot α, le_top := ⋯ }
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_zero : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q),
  ContinuousLinearMap.ofIsTopCompl h 0 0 = 0
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Std.Internal.Do.Except.wpInst.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (el : ε) → motive (Except.error el)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error el => h_2 el) =
    h_1 a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Unitization.complex_cfcₙ_eq_cfc_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] (a : A) (f : ℂ → ℂ),
  autoParam (f 0 = 0) Unitization.complex_cfcₙ_eq_cfc_inr._auto_1 → ↑(cfcₙ f a) = cfc f ↑a
-- Mathlib.CategoryTheory.Generator.Sheaf
/-- The bijection `(Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X))`
when `F : Sheaf J A`, `X : C` and `M : A`.  -/
CategoryTheory.Sheaf.freeYonedaHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          [inst_2 : CategoryTheory.Limits.HasCoproducts A] →
            [inst_3 : CategoryTheory.HasWeakSheafify J A] →
              {X : C} →
                {M : A} →
                  {F : CategoryTheory.Sheaf J A} →
                    (CategoryTheory.Sheaf.freeYoneda J X M ⟶ F) ≃ (M ⟶ F.obj.obj (Opposite.op X))
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- A `𝕜`-affine isometric embedding of one normed add-torsor over a normed `𝕜`-space into
another, denoted as `f : P →ᵃⁱ[𝕜] P₂`.  -/
AffineIsometry : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      (P : Type u_10) →
        (P₂ : Type u_11) →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [NormedSpace 𝕜 V₂] →
                        [inst : PseudoMetricSpace P₂] →
                          [NormedAddTorsor V₂ P₂] → Type (max (max (max u_10 u_11) u_2) u_5)
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.throwInvalidPattern : {α : Type} → Lean.Expr → Lean.MetaM α
-- Init.Data.Fin.Fold
Fin.foldl_zero : ∀ {α : Sort u_1} (f : α → Fin 0 → α) (x : α), Fin.foldl 0 f x = x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The horn inclusion corresponding to a cell of a rank function
for a proper pairing of a subcomplex of a simplicial set.  -/
SSet.Subcomplex.Pairing.RankFunction.basicCell : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) →
            [inst_1 : P.IsProper] → (i : ι) → (c : f.Cell i) → c.horn.toSSet ⟶ SSet.stdSimplex.obj { len := c.dim + 1 }
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiff.continuous_deriv : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F}, ContDiff 𝕜 n f → 1 ≤ n → Continuous (deriv f)
-- Mathlib.Data.Semiquot
Semiquot.partialOrder : {α : Type u_1} → PartialOrder (Semiquot α)
-- Init.Data.SInt.Lemmas
ISize.minValue_div_neg_one : ISize.minValue / -1 = ISize.minValue
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_Ici : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.image (Fin.natAdd m) (Finset.Ici i) = Finset.Ici (Fin.natAdd m i)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_apply_of_notMem : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B},
  b ∉ e.baseSet → ∀ (y : F), e.symm b y = Classical.arbitrary (E b)
-- Mathlib.Data.Nat.Bitwise
Nat.even_xor : ∀ {m n : ℕ}, Even (m ^^^ n) ↔ (Even m ↔ Even n)
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
ConvexOn.integrable_comp_rnDeriv_map : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} {g : 𝓧 → 𝓨},
  μ.AbsolutelyContinuous ν →
    Measurable g →
      MeasureTheory.StronglyMeasurable f →
        ConvexOn ℝ (Set.Ici 0) f →
          ContinuousWithinAt f (Set.Ici 0) 0 →
            MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
              MeasureTheory.Integrable
                (fun x => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) x).toReal)
                (MeasureTheory.Measure.map g ν)
-- Mathlib.Topology.MetricSpace.Gluing
/-- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
with each factor.
If the two spaces are bounded, one can say for instance that each point in the first is at distance
`diam X + diam Y + 1` of each point in the second.
Instead, we choose a construction that works for unbounded spaces, but requires basepoints,
chosen arbitrarily.
We embed isometrically each factor, set the basepoints at distance 1,
arbitrarily, and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
their respective basepoints, plus the distance 1 between the basepoints.
Since there is an arbitrary choice in this construction, it is not an instance by default.  -/
Metric.Sum.dist : {X : Type u} → {Y : Type v} → [MetricSpace X] → [MetricSpace Y] → X ⊕ Y → X ⊕ Y → ℝ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insertMany_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instCommMonoid : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : CommMonoid R] → [BoundedMul R] → [ContinuousMul R] → CommMonoid (BoundedContinuousFunction α R)
-- Mathlib.MeasureTheory.Function.SimpleFunc
_private.Mathlib.MeasureTheory.Function.SimpleFunc.0.MeasureTheory.SimpleFunc.eapproxDiff.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Grind.Interactive
/-- `exact e` closes the main goal if its target type matches that of `e`.  -/
Lean.Parser.Tactic.Grind.grindExact_ : Lean.ParserDescr
-- Lean.DocString.Markdown
/-- Render the `b` and its contents to Markdown lines, given recursive renderers
for inline and block content.
 -/
Lean.Doc.MarkdownBlock.toMarkdown : {i : Type u} →
  {b : Type v} →
    [self : Lean.Doc.MarkdownBlock i b] →
      (Lean.Doc.Inline i → Lean.Doc.MarkdownM (Array String)) →
        (Lean.Doc.Block i b → Lean.Doc.MarkdownM (Array String)) →
          b → Array (Lean.Doc.Block i b) → Lean.Doc.MarkdownM (Array String)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.erase_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {k : α} {c : ℕ},
  (Std.HashSet.Raw.emptyWithCapacity c).erase k = Std.HashSet.Raw.emptyWithCapacity c
-- Mathlib.Data.Nat.Factors
_private.Mathlib.Data.Nat.Factors.0.Nat.primeFactorsList.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_1 ()
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rco_eq_some : ∀ {m n i : ℕ}, i < n - m → (m...n).toList[i]? = some (m + i)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensParams : Lean.ToJson Lean.Lsp.SemanticTokensParams
-- Mathlib.Logic.Basic
ite_eq_or_eq : ∀ {α : Sort u_1} (P : Prop) [inst : Decidable P] (a b : α), (if P then a else b) = a ∨ (if P then a else b) = b
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.deterministic_id_map : ∀ (X Y : SFinKer) (f : X.carrier → Y.carrier),
  Measurable f → CategoryTheory.Deterministic { hom := ProbabilityTheory.Kernel.id.map f, property := ⋯ }
-- Std.Async.ContextAsync
/-- Waits for the current context to be cancelled.
 -/
Std.Async.ContextAsync.awaitCancellation : Std.Async.ContextAsync Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Data exhibiting that a morphism `f` has an image.  -/
CategoryTheory.Limits.ImageFactorisation.isImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Limits.ImageFactorisation f) → CategoryTheory.Limits.IsImage self.F
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.exists_adj_iff_not_isIsolated : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, (∃ u, G.Adj v u) ↔ ¬G.IsIsolated v
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instToStreamStream : {α : Type u_1} → Std.ToStream (RBTree.RBNode α) (RBTree.RBNode.Stream α)
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.instBEqHead.beq : Mathlib.Tactic.Push.Head → Mathlib.Tactic.Push.Head → Bool
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {b : β},
  xs.mapFinIdx f = #[b] ↔ ∃ a, ∃ (w : xs = #[a]), f 0 a ⋯ = b
-- Mathlib.Data.Real.Pointwise
Real.sSup_smul_of_nonneg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : MulActionWithZero α ℝ]
  [IsOrderedModule α ℝ] {a : α}, 0 ≤ a → ∀ (s : Set ℝ), sSup (a • s) = a • sSup s
-- Mathlib.Data.Set.Subset
Set.image_val_sInter : ∀ {α : Type u_2} {A : Set α} {T : Set (Set ↑A)},
  T.Nonempty → Subtype.val '' ⋂₀ T = ⋂₀ {x | ∃ B ∈ T, Subtype.val '' B = x}
-- Mathlib.GroupTheory.Submonoid.Center
AddSubsemigroup.centerCongr.eq_1 : ∀ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N),
  AddSubsemigroup.centerCongr e =
    { toFun := fun r => ⟨e ↑r, ⋯⟩, invFun := fun s => ⟨e.symm ↑s, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Connected.PathConnected
Joined.refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), Joined x x
-- Init.Data.Float.Model.Float
/-- Compute the ordering between two `Float.Model` as specified by IEEE. Returns an
`Option Ordering` to account for the fact that `NaN` is incomparable with everything.
Also, positive and negative zero are equal.
 -/
Float.Model.compare : Float.Model → Float.Model → Option Ordering
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α) (cut : α → Ordering) (lb : Option α),
  RBTree.RBNode.lowerBound? cut t.reverse lb = RBTree.RBNode.upperBound? (fun x => (cut x).swap) t lb
-- Mathlib.Analysis.Convex.Function
ConvexOn.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConvexOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x ≤ r}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_negY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Affine R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (x y : A), (W'.baseChange B).negY (f x) (f y) = f ((W'.baseChange A).negY x y)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_mk : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (e : α ≃ β)
  (h : Isometry e.toFun), ⇑{ toEquiv := e, isometry_toFun := h } = ⇑e
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (M M_1 : Matroid α) (e_M : M = M_1) (f f_1 : α → β) (e_f : f = f_1)
  (hf : Set.InjOn f M.E), M.map f hf = M_1.map f_1 ⋯
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.toMetricSpace : {E : Type u_8} → [self : NormedCommGroup E] → MetricSpace E
-- Init.Data.Vector.Lemmas
Vector.foldr_add_const : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a b : ℕ}, Vector.foldr (fun x x_1 => x_1 + a) b xs = b + a * n
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  (g : sInfHom βᵒᵈ γᵒᵈ) (f : sInfHom αᵒᵈ βᵒᵈ),
  sSupHom.dual.symm (g.comp f) = (sSupHom.dual.symm g).comp (sSupHom.dual.symm f)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The additive congruence relation used to localize an `AddCommMonoid` at a submonoid can be
expressed equivalently as an infimum (see `AddLocalization.r`) or explicitly
(see `AddLocalization.r'`).  -/
AddLocalization.r_eq_r' : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization.r S = AddLocalization.r' S
-- Init.Data.Nat.Basic
Nat.instNeZeroSucc : ∀ {n : ℕ}, NeZero (n + 1)
-- Mathlib.Order.Ideal
Order.Cofinal.mk.sizeOf_spec : ∀ {P : Type u_2} [inst : Preorder P] [inst_1 : SizeOf P] (carrier : Set P) (isCofinal : IsCofinal carrier),
  sizeOf { carrier := carrier, isCofinal := isCofinal } = 1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplex_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_3),
  (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = X.δ f₁ f₂ n₁ n₂ ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.denoteTerm : {α : Type u_1} → [Lean.Grind.Ring α] → Lean.Grind.CommRing.Context α → ℤ → Lean.Grind.CommRing.Mon → α
-- Mathlib.Probability.Distributions.Exponential
/-- The pdf of the exponential distribution, as a function valued in `ℝ≥0∞`  -/
ProbabilityTheory.exponentialPDF : ℝ → ℝ → ENNReal
-- Mathlib.Order.Bounds.Basic
le_of_isGLB_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {b : α} (a : α), IsGLB (Set.Ioi a) b → a ≤ b
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eval_neg : ∀ {R : Type u_2} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : Ring R] [inst_2 : Module R M]
  (l : Mathlib.Tactic.Module.NF R M), (-l).eval = -l.eval
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [F.PreservesFiniteEffectiveEpiFamilies] [F.ReflectsFiniteEffectiveEpiFamilies] [F.Full] [F.Faithful]
  [F.EffectivelyEnough] [inst_7 : CategoryTheory.Precoherent D] (X : C) (S : CategoryTheory.Sieve X),
  (∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ (F.inducedTopology (CategoryTheory.coherentTopology D)) X
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_pow : ∀ {k : ℕ} (n : ℕ), k ≠ 0 → (n ^ k).primeFactors = n.primeFactors