mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_toOrderIso_inv : ∀ (f : CircleDeg1Liftˣ), ⇑(CircleDeg1Lift.toOrderIso f)⁻¹ = ⇑↑f⁻¹
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.Context.mk : Bool → Lean.Meta.AbstractNestedProofs.Context
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mk : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {n : ℕ∞} →
                (toFun : E → F) →
                  ContDiff ℝ (↑n) toFun → HasCompactSupport toFun → tsupport toFun ⊆ ↑Ω → TestFunction Ω F n
-- Init.Core
Lean.Name.num.inj : ∀ {pre : Lean.Name} {i : ℕ} {pre_1 : Lean.Name} {i_1 : ℕ}, pre.num i = pre_1.num i_1 → pre = pre_1 ∧ i = i_1
-- Mathlib.Topology.Homotopy.LocallyContractible
StronglyLocallyContractibleSpace.mk : ∀ {X : Type u_4} [inst : TopologicalSpace X],
  (∀ (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ ContractibleSpace ↑s) id) → StronglyLocallyContractibleSpace X
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `X` is an affine scheme, every closed set of `X` is the zero locus
of a set of global sections.  -/
AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (s : Set ↥X), IsClosed s ↔ ∃ I, s = X.zeroLocus ↑I
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.toRightDerivedZero'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Abelian D] {X : C}
  (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  P.toRightDerivedZero' F =
    ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).liftCycles (F.map (P.ι.f 0)) 1
      CategoryTheory.InjectiveResolution.toRightDerivedZero'._proof_1 ⋯
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowHom.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {F' G' : HomologicalComplex C c} (φ' : F' ⟶ G')
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] (H : ∀ (j : ι), ∃ i, c.Rel i j)
  (α : CategoryTheory.Arrow.mk φ ⟶ CategoryTheory.Arrow.mk φ'),
  HomologicalComplex.homotopyCofiber.mapArrowHom φ φ' H α =
    HomologicalComplex.homotopyCofiber.desc φ
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right α)
        (HomologicalComplex.homotopyCofiber.inr φ'))
      ((Homotopy.ofEq ⋯).trans
        (((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ' H).compLeft (CategoryTheory.Arrow.Hom.left α)).trans
          (Homotopy.ofEq ⋯)))
-- Mathlib.Analysis.Convex.Deriv
StrictConvexOn.slope_lt_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f y → slope f x y < deriv f y
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.empty_inner : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering}, Std.DTreeMap.Internal.Cell.empty.inner = none
-- Mathlib.RingTheory.PolynomialAlgebra
/-- The `R`-algebra isomorphism `A[X] ≃ₐ[R] (A ⊗[R] R[X])`.
 -/
polyEquivTensor : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Polynomial A ≃ₐ[R] TensorProduct R A (Polynomial R)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.MatcherKey.mk : Lean.Expr → Bool → Bool → Lean.Meta.Match.MatcherKey✝
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.discreteSieve_apply : ∀ (α x : Type u) (f : x ⟶ α),
  (CategoryTheory.discreteSieve α).arrows f = ∃ x_1, ∀ (y : x), (CategoryTheory.ConcreteCategory.hom f) y = x_1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- Making an object of `FreeSimplexQuiver` out of a natural number.  -/
FreeSimplexQuiver.mk : ℕ → FreeSimplexQuiver
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.instLawfulOperatorRefMkNotCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref Std.Sat.AIG.mkNotCached
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.comm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Mathlib.Topology.NhdsKer
nhdsKer_biUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_3} (s : Set ι) (t : ι → Set X),
  nhdsKer (⋃ i ∈ s, t i) = ⋃ i ∈ s, nhdsKer (t i)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.homCategory : {B : Type u} →
  [inst : Quiver B] → (a b : CategoryTheory.FreeBicategory B) → CategoryTheory.Category.{max u v, max u v} (a ⟶ b)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_apply_eq_zero_iff : ∀ {m : Type u_3} {n : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_7} {M₁ : Type u_8}
  {M₂ : Type u_9} [inst_2 : Finite m] [inst_3 : CommRing R] [inst_4 : AddCommGroup M₁] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] {v₁ : Module.Basis n R M₁} {v₂ : Module.Basis m R M₂} {A : Matrix m n R}
  {x : M₁}, ((Matrix.toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), A.mulVec (⇑(v₁.repr x)) j = 0
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_vecAlt0 : ∀ {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α),
  Matrix.vecAlt0 h (Matrix.vecCons x (Matrix.vecCons y u)) = Matrix.vecCons x (Matrix.vecAlt0 ⋯ u)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.congr_fun₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, f = g → ∀ (x : M) (y : N), (f x) y = (g x) y
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_coe : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {J : Ideal R},
  J ≠ 0 → FractionalIdeal.count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries.map`. -/
lowerCentralSeries.map : ∀ {G : Type u_1} [inst : Group G] {K : Type u_2} [inst_1 : Group K] (f : G →* K) (n : ℕ),
  Subgroup.map f (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
-- Std.Time.Zoned.Database.TzIf
/-- The number of transition times in the file.
 -/
Std.Time.TimeZone.TZif.Header.timecnt : Std.Time.TimeZone.TZif.Header → UInt32
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_id_inv_isIso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) {a b : 𝒳} (φ : a ⟶ b) [inst_2 : CategoryTheory.IsIso φ]
  [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ],
  p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.inv φ)
-- Mathlib.Data.Analysis.Filter
/-- Transfer a filter realizer to another realizer on a different base type.  -/
Filter.Realizer.ofEquiv : {α : Type u_1} → {τ : Type u_4} → {f : Filter α} → (F : f.Realizer) → F.σ ≃ τ → f.Realizer
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The proposed colimit cocone is a colimit in `CommGrpCat`.  -/
CommGrpCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J CommGrpCat) →
        CategoryTheory.Limits.IsColimit (CommGrpCat.FilteredColimits.colimitCocone F)
-- Lean.DocString.Syntax
/-- A _role_: an extension to the Verso document language in an inline position.

Text is given a role using the following syntax: `{NAME ARGS*}[CONTENT]`. The `NAME` is an
identifier that determines which role is being used, akin to a function name. Each of the `ARGS` may
have the following forms:
* A value, which is a string literal, natural number, or identifier
* A named argument, of the form `(NAME := VALUE)`
* A flag, of the form `+NAME` or `-NAME`

The `CONTENT` is a sequence of inline content. If there is only one piece of content and it has
beginning and ending delimiters (e.g. code literals, links, or images, but not ordinary text), then
the `[` and `]` may be omitted. In particular, `` {NAME ARGS*}`x` `` is equivalent to
``{NAME ARGS*}[`x`]``.
 -/
Lean.Doc.Syntax.role : Lean.ParserDescr
-- Mathlib.Analysis.Meromorphic.Order
/-- The order is additive when multiplying scalar-valued and vector-valued meromorphic functions.  -/
meromorphicOrderAt_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : NormedRing R] [NoZeroDivisors R] [inst_5 : Module R E]
  [IsBoundedSMul R E] [Module.IsTorsionFree R E] {x : 𝕜} [inst_8 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {f : 𝕜 → R}
  {g : 𝕜 → E},
  MeromorphicAt f x → MeromorphicAt g x → meromorphicOrderAt (f • g) x = meromorphicOrderAt f x + meromorphicOrderAt g x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.union_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonOneHom.eq_1 : ∀ {α : Type u_2} [inst : One α], Set.singletonOneHom = { toFun := singleton, map_one' := ⋯ }
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addLeft_symm : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] (a : α),
  (OrderIso.addLeft a).symm = OrderIso.addLeft (-a)
-- Init.Data.UInt.Lemmas
USize.le_or_lt : ∀ (a b : USize), a ≤ b ∨ b < a
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.hom_ext : ∀ {R : Type u} [inst : Semiring R] {X Y : CategoryTheory.Mat R} (f g : X ⟶ Y),
  (∀ (i : X.obj) (j : Y.obj), f i j = g i j) → f = g
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toBialgHom_inj : ∀ {R : Type u} {A : Type v} {B : Type w} [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]
  {e₁ e₂ : A ≃ₐc[R] B}, ↑e₁ = ↑e₂ ↔ e₁ = e₂
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.instNonempty : ∀ {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], Nonempty (HahnEmbedding.ArchimedeanStrata K M)
-- Mathlib.Tactic.ProdAssoc
/-- Construct the equivalence between iterated products of the same type, associated
in possibly different ways.  -/
Lean.Expr.mkProdEquiv : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarRight_apply_tmul_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {ι : Type u_5}
  [inst_7 : DecidableEq ι] (m : M) (p : ι →₀ R) (i : ι),
  ((TensorProduct.finsuppScalarRight R S M ι) (m ⊗ₜ[R] p)) i = p i • m
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData : (α : Type u) → [Ord α] → Type u
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.exists_pow_eq' : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {a b : α}, s.Finite → f.IsCycleOn s → a ∈ s → b ∈ s → ∃ n, (f ^ n) a = b
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.funMap_add : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] {v : Fin 2 → M},
  FirstOrder.Language.Structure.funMap FirstOrder.presburgerFunc.add v = v 0 + v 1
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.soln_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) {ε : ℝ},
  ε > 0 → ∃ N, ∀ {i : ℕ}, i ≥ N → ‖soln_gen✝ hnorm - ↑(newton_cau_seq✝ hnorm) i‖ < ε
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.mk.inj : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {I₂₃ : Type u_11}
  {p : I₂ × I₃ → I₂₃} {q : I₁ × I₂₃ → J} {hpq : ∀ (i : I₁ × I₂ × I₃), q (i.1, p i.2) = r i} {I₂₃_1 : Type u_11}
  {p_1 : I₂ × I₃ → I₂₃_1} {q_1 : I₁ × I₂₃_1 → J} {hpq_1 : ∀ (i : I₁ × I₂ × I₃), q_1 (i.1, p_1 i.2) = r i},
  { I₂₃ := I₂₃, p := p, q := q, hpq := hpq } = { I₂₃ := I₂₃_1, p := p_1, q := q_1, hpq := hpq_1 } →
    I₂₃ = I₂₃_1 ∧ p ≍ p_1 ∧ q ≍ q_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_one_iff_of_pos : ∀ {x y : ℝ}, 0 < x → (x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.zero_le_one : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R], 0 ≤ 1
-- Mathlib.Data.Finite.Set
Finite.Set.finite_of_finite_image : ∀ {α : Type u} {β : Type v} (s : Set α) {f : α → β}, Set.InjOn f s → ∀ [Finite ↑(f '' s)], Finite ↑s
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_natCast : ∀ {d : ℤ} (n : ℕ), (↑n).im = 0
-- Std.Do.SPred.Laws
Std.Do.SPred.imp_elim : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ Q → R) → P ∧ Q ⊢ₛ R
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.mk.sizeOf_spec : ∀ (aesopStx : Lean.Syntax) (fileName : String) (position? : Option Lean.Position) (stats : Aesop.Stats),
  sizeOf { aesopStx := aesopStx, fileName := fileName, position? := position?, stats := stats } =
    1 + sizeOf aesopStx + sizeOf fileName + sizeOf position? + sizeOf stats
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.minKey_eq_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered → ∀ {he : l.isEmpty = false}, l.minKey he = Std.Internal.List.minKey l.toListModel ⋯
-- Mathlib.RingTheory.IdealFilter.Basic
/-- A filter of ideals is *uniform* if it is closed under colon by singletons.  -/
IdealFilter.IsUniform : {A : Type u_1} → [inst : Ring A] → IdealFilter A → Prop
-- Mathlib.Topology.ContinuousMap.Compact
/-- The distance between two functions is controlled by the supremum of the pointwise distances.  -/
ContinuousMap.dist_le : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)} {C : ℝ}, 0 ≤ C → (dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.sum_adj : ∀ {V : Type u_3} {W : Type u_5} (G : SimpleGraph V) (H : SimpleGraph W) (x x_1 : V ⊕ W),
  (G ⊕g H).Adj x x_1 =
    match x, x_1 with
    | Sum.inl u, Sum.inl v => G.Adj u v
    | Sum.inr u, Sum.inr v => H.Adj u v
    | x, x_2 => False
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    AlgebraicGeometry.PresheafedSpace.GlueData C → CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C)
-- Mathlib.Data.Sum.Interval
Sum.Ioi_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderTop β] (a : α), Finset.Ioi (Sum.inl a) = Finset.map Function.Embedding.inl (Finset.Ioi a)
-- Init.Data.Float.Float
/-- Computes the natural logarithm `ln x` of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`log`.
 -/
Float.log : Float → Float
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.get : ∀ {m₁ : List Char} {c : Char} {m₂ : List Char} {s : Substring.Raw},
  s.Valid → s.toString.toList = m₁ ++ c :: m₂ → s.get { byteIdx := String.utf8Len m₁ } = c
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_zero_of_dvd : ∀ {a : ℕ} {b : ℤ}, ↑a ∣ b → b.bmod a = 0
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_singleton_append_iff : ∀ {xs : Array ℤ} {m n a : ℤ}, (m<...n).toArray = #[a] ++ xs ↔ m + 1 = a ∧ m + 1 < n ∧ ((m + 1)<...n).toArray = xs
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- Given a signed measure `s`, `s.toJordanDecomposition` is the Jordan decomposition `j`,
such that `s = j.toSignedMeasure`. This property is known as the Jordan decomposition
theorem, and is shown by
`MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition`.  -/
MeasureTheory.SignedMeasure.toJordanDecomposition : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → MeasureTheory.JordanDecomposition α
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.eraseMany : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.DTreeMap.Raw α β cmp}, t.WF → (t.eraseMany l).WF
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limit_ext' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F' : CategoryTheory.Functor J (Type v))
  (x y : CategoryTheory.Limits.limit F'),
  (∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) y) →
    x = y
-- Mathlib.Analysis.LocallyConvex.Bounded
QuasiCompleteSpace.mk : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : Zero E] [inst_1 : UniformSpace E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E], (∀ ⦃s : Set E⦄, Bornology.IsVonNBounded 𝕜 s → IsClosed s → IsComplete s) → QuasiCompleteSpace 𝕜 E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan_pos : ∀ {x : ℝ}, 0 < Real.sin (Real.arctan x) ↔ 0 < x
-- Mathlib.Order.WithBot
WithTop.le_untopA_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithTop α} [inst_1 : Nonempty α], x ≠ ⊤ → (a ≤ x.untopA ↔ ↑a ≤ x)
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- An idempotent operator is positive if and only if it is self-adjoint.  -/
ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {p : E →L[𝕜] E}, IsIdempotentElem p → (p.IsPositive ↔ IsSelfAdjoint p)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.contains a = true → t.getKey? a = some (t.getKey! a)
-- Lean.Widget.Basic
Lean.Widget.instTypeNameLocalContext : TypeName Lean.LocalContext
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.mul_ite_zero''' : ∀ {w : ℕ} {c : Bool} {a t : BitVec w}, (bif c then t else 0#w) * a = bif c then t * a else 0#w
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instCommRing : {R : Type u_1} → [CommRing R] → CommRing (Lex R)
-- Lean.Data.Options
Lean.OptionDecl.defValue : Lean.OptionDecl → Lean.DataValue
-- Mathlib.LinearAlgebra.Basis.Fin
/-- Let `b` be a basis for a submodule `N ≤ O`. If `y ∈ O` is linear independent of `N`
and `y` and `N` together span the whole of `O`, then there is a basis for `O`
whose basis vectors are given by `Fin.snoc b y`.  -/
Module.Basis.mkFinSnocOfLE : {R : Type u_3} →
  {M : Type u_5} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {n : ℕ} →
            {N O : Submodule R M} →
              Module.Basis (Fin n) R ↥N →
                N ≤ O →
                  (y : M) →
                    y ∈ O →
                      (∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) →
                        (∀ z ∈ O, ∃ c, z + c • y ∈ N) → Module.Basis (Fin (n + 1)) R ↥O
-- Lean.CoreM
Lean.Core.modifyInstLevelTypeCache : (Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache) → Lean.CoreM Unit
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_i : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_i._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).left.i =
    CategoryTheory.CategoryStruct.comp (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
      (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).inv
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.ruleTac : Lean.Name → Aesop.RuleTacDescr
-- Mathlib.Order.Defs.Unbundled
/-- A lower set in an order `α` is a set such that any element less than one of its
members is also a member. Also called down-set, downward-closed set.  -/
LowerSet : (α : Type u_1) → [LE α] → Type u_1
-- Init.Data.Iterators.Consumers.Partial
/-- A wrapper around an iterator that provides partial consumers. See `Iter.allowNontermination`.
 -/
Std.Iter.Partial : {α : Type w} → Type w → Type w
-- Mathlib.RingTheory.WittVector.Identities
_private.Mathlib.RingTheory.WittVector.Identities.0.WittVector.term𝕎 : Lean.ParserDescr
-- Mathlib.Data.Set.Lattice
Set.iUnion_ite : ∀ {α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [inst : DecidablePred p] (f g : ι → Set α),
  (⋃ i, if p i then f i else g i) = (⋃ i, ⋃ (_ : p i), f i) ∪ ⋃ i, ⋃ (_ : ¬p i), g i
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The colimit of `F ⋙ forget₂ CommMonCat MonCat` in the category `MonCat`.
In the following, we will show that this has the structure of a _commutative_ monoid.
 -/
CommMonCat.FilteredColimits.M : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J CommMonCat → MonCat
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.hasSameRoot : Lean.Meta.Grind.ENodeMap → Lean.Expr → Lean.Expr → Bool
-- Std.Data.TreeMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.TreeMap.erase : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Std.TreeMap α β cmp