mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.pair_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : MeasureTheory.SimpleFunc α γ) (a : α), (f.pair g) a = (f a, g a)
-- Mathlib.Tactic.Linter.TextBased
/-- Lint on any occurrences of the string "Adaptation note:" or variants thereof.  -/
Mathlib.Linter.TextBased.linter.adaptationNote : Lean.Option Bool
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.coe_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  (x : ↥H) (n : ℕ), ↑(n • x) = n • ↑x
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Estimate for `log⁺` of a sum. See `Real.posLog_add` for a variant involving
just two summands.  -/
Real.posLog_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℝ), (∑ t ∈ s, f t).posLog ≤ Real.log ↑s.card + ∑ t ∈ s, (f t).posLog
-- Std.Http.Data.Body.Any
/-- Erases a body of any `Http.Body` instance into a `Body.Any`.
 -/
Std.Http.Body.Any.ofBody : {α : Type} → [Std.Http.Body α] → α → Std.Http.Body.Any
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_eq_one_iff : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] {I : Ideal S},
  Ideal.absNorm I = 1 ↔ I = ⊤
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The measurable **Besicovitch covering theorem**.

Assume that, for any `x` in a set `s`, one is given a set of admissible closed balls centered at
`x`, with arbitrarily small radii. Then there exists a disjoint covering of almost all `s` by
admissible closed balls centered at some points of `s`. We can even require that the radius at `x`
is bounded by a given function `R x`. (Take `R = 1` if you don't need this additional feature).

This version requires the underlying measure to be sigma-finite, and the space to have the
Besicovitch covering property (which is satisfied for instance by normed real vector spaces).
 -/
Besicovitch.exists_disjoint_closedBall_covering_ae : ∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  (f : α → Set ℝ) (s : Set α),
  (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
    ∀ (R : α → ℝ),
      (∀ x ∈ s, 0 < R x) →
        ∃ t r,
          t.Countable ∧
            t ⊆ s ∧
              (∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧
                μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => Metric.closedBall x (r x)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- Partner function to `reduceCyclically`.
See `reduceCyclically.conj_conjugator_reduceCyclically`.  -/
FreeAddGroup.reduceCyclically.conjugator : {α : Type u} → [DecidableEq α] → List (α × Bool) → List (α × Bool)
-- Init.Data.String.PosRaw
String.Pos.Raw.addChar_eq : ∀ (p : String.Pos.Raw) (c : Char), p + c = { byteIdx := p.byteIdx + c.utf8Size }
-- Init.Data.Fin.Fold
Fin.foldl_succ_last : ∀ {α : Sort u_1} {n : ℕ} (f : α → Fin (n + 1) → α) (x : α),
  Fin.foldl (n + 1) f x = f (Fin.foldl n (fun x1 x2 => f x1 x2.castSucc) x) (Fin.last n)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_one : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {l : Filter α} {f : α → E} [ContinuousSMul 𝕜 E],
  f =o[𝕜; l] 1 ↔ Filter.Tendsto f l (nhds 0)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of the `n`th power of a field element `x` (with `n : ℕ`)
is the `n`th power of the multiplicative height of `x`.  -/
Height.mulHeight₁_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K) (n : ℕ),
  Height.mulHeight₁ (x ^ n) = Height.mulHeight₁ x ^ n
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toNonUnitalCStarAlgebra : (A : Type u_1) → [CStarAlgebra A] → NonUnitalCStarAlgebra A
-- Mathlib.RingTheory.Henselian
isLocalHom_of_le_jacobson_bot : ∀ {R : Type u_1} [inst : CommRing R], ∀ I ≤ ⊥.jacobson, IsLocalHom (Ideal.Quotient.mk I)
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.HoldsForLocalizationAway : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.PropertyIsLocal P →
    (RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P) → RingHom.HoldsForLocalizationAway P
-- Mathlib.LinearAlgebra.Basis.Defs
Finsupp.linearEquivFunOnFinite.congr_simp : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M], Finsupp.linearEquivFunOnFinite R M α = Finsupp.linearEquivFunOnFinite R M α
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_toFinset : ∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq β] (s : Finset α) (f : α → Multiset β),
  (s.sup f).toFinset = s.sup fun x => (f x).toFinset
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.algSpec.eq_1 : ∀ (R : CommRingCat),
  AlgebraicGeometry.algSpec R =
    (commAlgCatEquivUnder R).op.functor.comp
      ((CategoryTheory.Over.opEquivOpUnder R).inverse.comp (CategoryTheory.Over.post AlgebraicGeometry.Scheme.Spec))
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.mk_mem_interedges_comm : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} {a b : α},
  (a, b) ∈ G.interedges s t ↔ (b, a) ∈ G.interedges t s
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.symm_apply_eq : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b) {a_1 : H}
  {b_1 : G}, e.symm a_1 = b_1 ↔ a_1 = e b_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β] (f : α → β),
  Finset.sup 1 f = f 1
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s s' : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : Nonempty ↥s'] [inst_7 : s.direction.HasOrthogonalProjection]
  [inst_8 : s'.direction.HasOrthogonalProjection],
  s = s' → ∀ (p : P), ↑((EuclideanGeometry.orthogonalProjection s) p) = ↑((EuclideanGeometry.orthogonalProjection s') p)
-- Std.Http.Internal.ChunkedBuffer
/-- Writes a `ByteArray` to the `ChunkedBuffer`.
 -/
Std.Http.Internal.ChunkedBuffer.write : Std.Http.Internal.ChunkedBuffer → ByteArray → Std.Http.Internal.ChunkedBuffer
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : AlgebraicGeometry.SheafedSpace C) → TopologicalSpace ↑↑X.toPresheafedSpace
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_coe_sort : ∀ {ι : Type u_1} {M : Type u_4} (s : Finset ι) [inst : AddCommMonoid M] (f : ι → M), ∑ i, f ↑i = ∑ i ∈ s, f i
-- Mathlib.Data.Finsupp.Indicator
Finsupp.indicator.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (f : (i : ι) → i ∈ s → α),
  Finsupp.indicator s f =
    { support := Finset.map (Function.Embedding.subtype fun x => x ∈ s) {i | f ↑i ⋯ ≠ 0},
      toFun := fun i => if H : i ∈ s then f i H else 0, mem_support_toFun := ⋯ }
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (i : E.toPreOneHypercover.I₀),
  E.toSaturateOfHasPullbacks.h₀ i = CategoryTheory.CategoryStruct.id (E.toPreOneHypercover.X i)
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_eq : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  StarAlgebra.adjoin R ↑S = S
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_apply : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
  (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Π₀ (i : ι), β₁ i) (i : ι),
  (DFinsupp.mapRange f hf g) i = f i (g i)
-- Mathlib.NumberTheory.LucasLehmer
mersenne_pos : ∀ {p : ℕ}, 0 < mersenne p ↔ 0 < p
-- Mathlib.Data.Finset.Defs
Finset.val_inj : ∀ {α : Type u_1} {s t : Finset α}, s.val = t.val ↔ s = t
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isOpen_forall_imp_mem_of_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)],
  (∀ (i : ι), IsOpen (A i)) →
    ∀ {S : Set ι}, Filter.cofinite ≤ Filter.principal S → ∀ {p : ι → Prop}, IsOpen {f | ∀ (i : ι), p i → ↑f i ∈ A i}
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.F_union_I : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), ↑IF.F ∪ ↑IF.I = Set.univ
-- Mathlib.Topology.Algebra.Ring.Basic
Pi.instIsSemitopologicalSemiring : ∀ {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (R i)]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (R i)] [∀ (i : ι), IsSemitopologicalSemiring (R i)],
  IsSemitopologicalSemiring ((i : ι) → R i)
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_toAlgHom_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective BialgHom.toAlgHom
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_lt_of_contravariant_le : ∀ (N : Type u_2) (mu : N → N → N) [inst : LinearOrder N] [ContravariantClass N N mu fun x1 x2 => x1 ≤ x2],
  CovariantClass N N mu fun x1 x2 => x1 < x2
-- Mathlib.Topology.Compactness.Compact
Filter.cocompact_eq_cofinite : ∀ (X : Type u_2) [inst : TopologicalSpace X] [DiscreteTopology X], Filter.cocompact X = Filter.cofinite
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.mkSimpExt : autoParam Lean.Name Lean.Meta.mkSimpExt._auto_1 → IO Lean.Meta.SimpExtension
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod_add : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ g₁ : M₁ →L[R] M) (f₂ g₂ : M₂ →L[R] M),
  (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.write.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a : Γ → σ → Γ} {a_1 : Turing.TM1.Stmt Γ Λ σ} {a_2 : Γ → σ → Γ}
  {a_3 : Turing.TM1.Stmt Γ Λ σ}, Turing.TM1.Stmt.write a a_1 = Turing.TM1.Stmt.write a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsOpenImmersionMapWalkingSpanSchemeSpan : ∀ {U X Y : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsOpenImmersion g] {i j : CategoryTheory.Limits.WalkingSpan} (t : i ⟶ j),
  AlgebraicGeometry.IsOpenImmersion ((CategoryTheory.Limits.span f g).map t)
-- Mathlib.Order.WithBot
WithTop.coe_untopD_le : ∀ {α : Type u_1} [inst : Preorder α] (x : WithTop α) (b : α), ↑(WithTop.untopD b x) ≤ x
-- Init.Data.Array.Zip
Array.zip_unzip : ∀ {α : Type u_1} {β : Type u_2} (xs : Array (α × β)), xs.unzip.1.zip xs.unzip.2 = xs
-- Init.Prelude
/-- Get the underlying byte index of a `String.Pos.Raw`  -/
String.Pos.Raw.byteIdx : String.Pos.Raw → ℕ
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.restrictLocallyRingedSpaceIso_hom : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] (U : TopologicalSpace.Opens M),
  (ChartedSpace.restrictLocallyRingedSpaceIso U).hom =
    AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)
      ((ChartedSpace.locallyRingedSpace IM M).ofRestrict ⋯) ⋯
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Monad.comparison_obj_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D),
  ((CategoryTheory.Monad.comparison h).obj X).a = R.map (h.counit.app X)
-- Mathlib.Algebra.Group.Action.Basic
arrowAction_smul : ∀ {G : Type u_7} {A : Type u_8} {B : Type u_9} [inst : DivisionMonoid G] [inst_1 : MulAction G A] (g : G) (F : A → B)
  (a : A), SMul.smul g F a = F (g⁻¹ • a)
-- Mathlib.CategoryTheory.Core
/-- The hom-type between two objects of `Core C`.
It is defined as a one-field structure to prevent defeq abuses.  -/
CategoryTheory.CoreHom : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Core C → CategoryTheory.Core C → Type v₁
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge : ∀ {f : ℝ → ℝ} {b : ℝ},
  b ∈ Set.Ioo 0 1 →
    AkraBazziRecurrence.GrowsPolynomially f →
      ∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {m₁ m₂ : Std.DHashMap.Raw α fun x => Unit},
  m₁.WF → m₂.WF → (∀ (k : α), m₁.contains k = m₂.contains k) → m₁.Equiv m₂
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
NNReal.monotone_nnrpow_const : ∀ (y : NNReal), Monotone fun x => x.nnrpow y
-- Lean.Meta.WHNF
/-- Add auxiliary annotation to indicate expression `e` (a `match` alternative rhs) was successfully reduced by smart unfolding.  -/
Lean.Meta.markSmartUnfoldingMatchAlt : Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.cons_cons : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {p : α × Bool}, FreeGroup.Red L₁ L₂ → FreeGroup.Red (p :: L₁) (p :: L₂)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.isRkFinite_union_iff : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → (M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y)
-- Init.Data.UInt.Lemmas
UInt8.sub_eq_add_neg : ∀ (a b : UInt8), a - b = a + -b
-- Init.Data.BitVec.Lemmas
/-- Truncating to width 1 produces a bitvector equal to the least significant bit.  -/
BitVec.setWidth_one : ∀ {w : ℕ} {x : BitVec w}, BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)
-- Init.Data.String.Basic
String.slice.congr_simp : ∀ (s : String) (startInclusive startInclusive_1 : s.Pos) (e_startInclusive : startInclusive = startInclusive_1)
  (endExclusive endExclusive_1 : s.Pos) (e_endExclusive : endExclusive = endExclusive_1)
  (h : startInclusive ≤ endExclusive), s.slice startInclusive endExclusive h = s.slice startInclusive_1 endExclusive_1 ⋯
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (i : n)
  (a : ↥(rootsOfUnity (Fintype.card n) R)), ↑↑((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' i).symm a) = a • 1
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.hasSorry.go : Lean.MetavarContext → Lean.Expr → Bool
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
rank_span : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] {v : ι → M},
  LinearIndependent R v → Module.rank R ↥(Submodule.span R (Set.range v)) = Cardinal.mk ↑(Set.range v)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rii α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Array of trie entries. Should be owned by this trie.  -/
Lean.Meta.RefinedDiscrTree.tries : {α : Type} → Lean.Meta.RefinedDiscrTree α → Array (Lean.Meta.RefinedDiscrTree.Trie α)
-- Mathlib.FieldTheory.Relrank
/-- If `A ≤ B`, then `Subfield.relfinrank A B` is `[B : A]`.  -/
Subfield.relfinrank_eq_finrank_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E} (h : A ≤ B),
  A.relfinrank B = Module.finrank ↥A ↥(Subfield.extendScalars h)
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
CategoryTheory.ExponentialIdeal.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalClosed C],
  (∀ {B : C}, i.essImage B → ∀ (A : C), i.essImage (A ⟹ B)) → CategoryTheory.ExponentialIdeal i
-- Mathlib.Control.Basic
/-- Attempts to perform the computation, and returns `none` if it doesn't succeed.  -/
try? : {F : Type → Type v} → [Alternative F] → {α : Type} → F α → F (Option α)
-- Mathlib.Tactic.Explode.Datatypes
/-- How to display pipes (`│`) for this entry in the Fitch table .  -/
Mathlib.Explode.Status : Type
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_smul_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] {𝕝 : Type u_5}
  [inst_4 : CommSemiring 𝕝] [inst_5 : StarRing 𝕝] [inst_6 : Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜]
  [inst_8 : (i : ι) → Module 𝕝 (E i)] [∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : (i : ι) → E i),
  ⟪f, c • g⟫_[𝕜, w] = c • ⟪f, g⟫_[𝕜, w]
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.tryRecv : {α : Type} → Std.CloseableChannel.Zero✝ α → BaseIO (Option α)
-- Lean.Expr
/-- Return true if `e` contains universe level parameters.
This is a constant time operation.
 -/
Lean.Expr.hasLevelParam : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `H` is an equivalence, we invert `H.mapCone` and get a cone for `F` from a cone
for `F ⋙ H`.  -/
CategoryTheory.Functor.mapCoconeInv : {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] →
            (H : CategoryTheory.Functor C D) →
              {F : CategoryTheory.Functor J C} →
                [H.IsEquivalence] → CategoryTheory.Limits.Cocone (F.comp H) → CategoryTheory.Limits.Cocone F
-- Mathlib.Order.Filter.Map
Filter.frequently_pure : ∀ {α : Type u_1} {a : α} {p : α → Prop}, (∃ᶠ (x : α) in pure a, p x) ↔ p a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.δ_def : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Action (Type u) G},
  CategoryTheory.Functor.OplaxMonoidal.δ (Rep.linearization k G) X Y =
    Rep.ofHom (Representation.LinearizeMonoidal.δ X Y)
-- Mathlib.Tactic.GRewrite.Elab
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.instEvalExprConfig_mathlib.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Rewrite.Config
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_left_inj : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, c ≤ a → c ≤ b → (a - c = b - c ↔ a = b)
-- Init.Data.Float.Float
/-- Computes the hyperbolic cosine of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`cosh`.
 -/
Float.cosh : Float → Float
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_symm_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  {X : Cᵒᵖ} (x : F.obj X) (f : F ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm x) f =
    CategoryTheory.uliftYonedaEquiv.symm
      ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op (Opposite.unop X)))) x)
-- Mathlib.GroupTheory.ResiduallyFinite
Group.instResiduallyFiniteSubtypeMemSubgroup : ∀ {G : Type u_1} [inst : Group G] [Group.ResiduallyFinite G] {H : Subgroup G}, Group.ResiduallyFinite ↥H
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_cons : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] {v' : V} {p : G.Walk v' v} (hwp : w ∈ p.support),
  u ≠ w →
    ∀ (hadj : G.Adj u v'), (SimpleGraph.Walk.cons hadj p).takeUntil w ⋯ = SimpleGraph.Walk.cons hadj (p.takeUntil w hwp)
-- Mathlib.Algebra.Polynomial.Sequence
/-- Basis elements have strictly monotone natural degree.  -/
Polynomial.Sequence.basis_natDegree_strictMono : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) [inst_1 : IsDomain R]
  (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff), StrictMono (Polynomial.natDegree ∘ ⇑(S.basis hCoeff))
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.unique_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (fac fac' : W₁.MapFactorizationData W₂ f),
  fac.Z = fac'.Z
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.add : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f g : E → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth (f + g)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNegEquiv_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg),
  ↑((S.leftNegEquiv hS) x) + ↑x = 0
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.connected : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.Connected
-- Mathlib.NumberTheory.PrimesCongruentOne
Nat.frequently_atTop_modEq_one : ∀ {k : ℕ}, k ≠ 0 → ∃ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p ∧ p ≡ 1 [MOD k]
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.toExpr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.Expr
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Express `nndist` in terms of `dist`  -/
nndist_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), nndist x y = (dist x y).toNNReal