mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
ergodic_mul_left_of_denseRange_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [SecondCountableTopology G] [BorelSpace G] {g : G},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant],
      Ergodic (fun x => g * x) μ
-- Aesop.Search.Queue
Aesop.BestFirstQueue.popGoal : Aesop.BestFirstQueue → Option Aesop.GoalRef × Aesop.BestFirstQueue
-- Mathlib.Data.Sum.Order
Sum.Lex.linearOrder : {α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [LinearOrder β] → LinearOrder (α ⊕ₗ β)
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.mk : (α : Type u) →
  [isUniformSpace : UniformSpace α] → [isCompleteSpace : CompleteSpace α] → [isT0 : T0Space α] → CpltSepUniformSpace
-- Mathlib.Algebra.GCDMonoid.Basic
neg_gcd' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : HasDistribNeg α] [inst_2 : GCDMonoid α] {a b : α},
  Associated (gcd (-a) b) (gcd a b)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq_spec_1 : (Lean.Grind.Linarith.Poly.nil == Lean.Grind.Linarith.Poly.nil) = true
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_deriv_riemannZeta_add_inv_sub_sub_isBigO : (fun s => deriv riemannZeta s / riemannZeta s + (s - 1)⁻¹ - ↑Real.eulerMascheroniConstant) =O[nhdsWithin 1 {1}ᶜ]
  fun x => x - 1
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivAevalNegX_symm_apply : ∀ {R : Type u_3} [inst : CommRing R] (a : Polynomial R),
  Polynomial.algEquivAevalNegX.symm a = (Polynomial.aeval (-Polynomial.X)) a
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.card_nthRootsFinset : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  IsPrimitiveRoot ζ n → (Polynomial.nthRootsFinset n 1).card = n
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.strictMono_x : ∀ {a : ℕ} (a1 : 1 < a), StrictMono (Pell.xn a1)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `none` if no such key exists.
 -/
Std.TreeMap.getKeyGT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option α
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_comp_eq_of_mul_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0 → (p.comp q).natDegree = p.natDegree * q.natDegree
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxKeyD : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → α → α
-- Mathlib.Topology.Defs.Basic
IsOpenQuotientMap.mk : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Function.Surjective f → Continuous f → IsOpenMap f → IsOpenQuotientMap f
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n * log n). Map a function on a set. Unlike `map` this has no requirements on
`f`, and the resulting set may be smaller than the input if `f` is noninjective.
Equivalent elements are selected with a preference for smaller source elements.

```
image (fun x ↦ x + 2) {1, 2, 4} = {3, 4, 6}
image (fun x : ℕ ↦ x - 2) {1, 2, 4} = {0, 2}
```  -/
Ordnode.image : {α : Type u_2} → {β : Type u_3} → [inst : LE β] → [DecidableLE β] → (α → β) → Ordnode α → Ordnode β
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `c` is a colimit cokernel cofork for `f : X ⟶ Y`, `e : Y ≅ Y'` and `f' : X' ⟶ Y` is a
morphism, then there is a colimit cokernel cofork for `f'` with the same point as `c` if for any
morphism `φ : Y ⟶ W`, there is an equivalence `f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0`.  -/
CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {c : CategoryTheory.Limits.CokernelCofork f} →
            CategoryTheory.Limits.IsColimit c →
              {X' Y' : C} →
                (f' : X' ⟶ Y') →
                  (e : Y' ≅ Y) →
                    (iff :
                        ∀ ⦃W : C⦄ (φ : Y ⟶ W),
                          CategoryTheory.CategoryStruct.comp f φ = 0 ↔
                            CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp e.hom φ) = 0) →
                      CategoryTheory.Limits.IsColimit
                        (CategoryTheory.Limits.CokernelCofork.ofπ
                          (CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Cofork.π c)) ⋯)
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.instPowWithConvNat : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] →
            [inst_3 : Bialgebra R A] →
              [inst_4 : Bialgebra R C] → [Coalgebra.IsCocomm R C] → Pow (WithConv (C →ₐc[R] A)) ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.p_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp P.p₁ h
-- Mathlib.Order.Category.BddOrd
BddOrd.instCoeSortType : CoeSort BddOrd (Type u_1)
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- A *cocompact continuous map* is a continuous function between topological spaces which
tends to the cocompact filter along the cocompact filter. Functions for which preimages of compact
sets are compact always satisfy this property, and the converse holds for cocompact continuous maps
when the codomain is Hausdorff (see `CocompactMap.tendsto_of_forall_preimage` and
`CocompactMap.isCompact_preimage`).

Cocompact maps thus generalise proper maps, with which they correspond when the codomain is
Hausdorff.  -/
CocompactMap : (α : Type u) → (β : Type v) → [TopologicalSpace α] → [TopologicalSpace β] → Type (max u v)
-- Mathlib.Algebra.Group.TypeTags.Hom
Multiplicative.monoidHom_ext_iff : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] {f g : Multiplicative α →* β},
  f = g ↔ MonoidHom.toAdditiveRight f = MonoidHom.toAdditiveRight g
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The identity functor is also the identity on commutative group objects.  -/
CategoryTheory.Functor.mapCommGrpIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (CategoryTheory.Functor.id C).mapCommGrp ≅ CategoryTheory.Functor.id (CategoryTheory.CommGrp C)
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.le_upper' : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] (hi : ℤ),
  i.hi? = some hi → ∀ (a : α), ↑a + 1 ≤ hi
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.subsingleton_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G}, Subsingleton (G ⧸ N) ↔ N = ⊤
-- Init.Data.List.Lemmas
List.foldlM_pure : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] {f : β → α → β} {b : β}
  {l : List α}, List.foldlM (fun x1 x2 => pure (f x1 x2)) b l = pure (List.foldl f b l)
-- Init.Grind.AC
Lean.Grind.AC.Expr.denote_op : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (a b : Lean.Grind.AC.Expr),
  Lean.Grind.AC.Expr.denote ctx (a.op b) = ctx.op (Lean.Grind.AC.Expr.denote ctx a) (Lean.Grind.AC.Expr.denote ctx b)
-- Init.Data.Array.Count
/-- This lemma is only relevant for `grind`.  -/
Std.Internal.Array.not_of_countP_eq_zero_of_mem : ∀ {α : Type u_1} {p : α → Bool} {x : α} {xs : Array α}, Array.countP p xs = 0 → x ∈ xs → ¬p x = true
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The `0`-cocycle associated to a morphism in `CochainComplex C ℤ`.  -/
CochainComplex.HomComplex.Cocycle.ofHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} → (F ⟶ G) → CochainComplex.HomComplex.Cocycle F G 0
-- Lean.Parser.Command
/-- `include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all
theorems in the remainder of the current section, differing from the default behavior of
conditionally including variables based on use in the theorem header. Other commands are
not affected. `include` is usually followed by `in theorem ...` to limit the inclusion
to the subsequent declaration.
 -/
Lean.Parser.Command.include : Lean.Parser.Parser
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodProdProdComm_toEquiv : ∀ (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S'],
  ↑(RingEquiv.prodProdProdComm R R' S S') = Equiv.prodProdProdComm R R' S S'
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toStructuredArrow_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y),
  (CategoryTheory.Limits.Cocone.toStructuredArrow F).map f = CategoryTheory.StructuredArrow.homMk f.hom ⋯
-- Init.Data.Char.Ordinal
Char.succ?.fun_cases_unfolding : ∀ (c : Char) (motive : Option Char → Prop),
  (∀ (h : c.val < 55295), motive (some { val := c.val + 1, valid := ⋯ })) →
    (¬c.val < 55295 → c.val = 55295 → motive (some { val := 57344, valid := Char.succ?._proof_2✝ })) →
      (∀ (h : ¬c.val < 55295) (h_1 : ¬c.val = 55295) (h_2 : c.val < 1114111),
          motive (some { val := c.val + 1, valid := ⋯ })) →
        (¬c.val < 55295 → ¬c.val = 55295 → ¬c.val < 1114111 → motive none) → motive c.succ?
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂),
  (CategoryTheory.ComposableArrows.mk₂
        (R₁.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
          CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4)
        (R₁.map' 2 3 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4
          CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7)).Exact →
    (CategoryTheory.ComposableArrows.mk₂
          (R₂.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11)
          (R₂.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4)).Exact →
      R₂.map' 1 3 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7 =
          0 →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_13) →
          CategoryTheory.Epi
              (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4) →
            CategoryTheory.Mono
                (CategoryTheory.ComposableArrows.app' φ 3
                  CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7) →
              CategoryTheory.Epi
                (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertMany l).get? k = none
-- Mathlib.Algebra.RingQuot
RingQuot.instSMulOfAlgebra : {R : Type uR} →
  [inst : Semiring R] →
    {S : Type uS} → [inst_1 : CommSemiring S] → (r : R → R → Prop) → [Algebra S R] → SMul S (RingQuot r)
-- Mathlib.Data.Nat.DvdSequence
IsDvdSequence.id : ∀ (α : Type u_1) [inst : Dvd α], IsDvdSequence id
-- Mathlib.Order.Fin.Basic
Fin.revOrderIso_symm_apply : ∀ {n : ℕ} (i : Fin n), Fin.revOrderIso.symm i = OrderDual.toDual i.rev
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_ne_zero_iff : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  {x : G i}, RestrictedProduct.single A i x ≠ 0 ↔ x ≠ 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.upperBound?.eq_2 : ∀ {α : Type u_1} (cut : α → Ordering) (x : Option α) (c : RBTree.RBColor) (a : RBTree.RBNode α) (y : α)
  (b : RBTree.RBNode α),
  RBTree.RBNode.upperBound? cut (RBTree.RBNode.node c a y b) x =
    match cut y with
    | Ordering.lt => RBTree.RBNode.upperBound? cut a (some y)
    | Ordering.gt => RBTree.RBNode.upperBound? cut b x
    | Ordering.eq => some y
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_iInf : ∀ {ι : Sort u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] {x : M} {f : ι → ClosedSubmodule R M},
  x ∈ ⨅ i, f i ↔ ∀ (i : ι), x ∈ f i
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.not_cliqueFree_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, ¬G.CliqueFree 0
-- Mathlib.Control.Basic
joinM_map_map : ∀ {m : Type u → Type u} [inst : Monad m] [LawfulMonad m] {α β : Type u} (f : α → β) (a : m (m α)),
  joinM (Functor.map f <$> a) = f <$> joinM a
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a multifork, we may obtain a fork over `∏ᶜ I.left ⇉ ∏ᶜ I.right`.  -/
CategoryTheory.Limits.Multifork.toPiFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        {c : CategoryTheory.Limits.Fan I.left} →
          CategoryTheory.Limits.IsLimit c →
            {d : CategoryTheory.Limits.Fan I.right} →
              (hd : CategoryTheory.Limits.IsLimit d) →
                CategoryTheory.Limits.Multifork I →
                  CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.leval_apply : ∀ (R : Type u_1) {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : Module R S] [inst_3 : Monoid S]
  (x : Sˣ) (f : LaurentPolynomial R), (LaurentPolynomial.leval R x) f = f.smeval x
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_top : ∀ {α : Type u_1} [inst : LE α], ↑⊤ = ∅
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
/-- The braiding operation for tensor products of externally `ι`-graded algebras.

This sends $a ⊗ b$ to $(-1)^{\deg a' \deg b} (b ⊗ a)$.  -/
TensorProduct.gradedComm : (R : Type u_1) →
  {ι : Type u_2} →
    [inst : CommSemiring ι] →
      [Module ι (Additive ℤˣ)] →
        [DecidableEq ι] →
          (𝒜 : ι → Type u_3) →
            (ℬ : ι → Type u_4) →
              [inst : CommRing R] →
                [inst_1 : (i : ι) → AddCommGroup (𝒜 i)] →
                  [inst_2 : (i : ι) → AddCommGroup (ℬ i)] →
                    [inst_3 : (i : ι) → Module R (𝒜 i)] →
                      [inst_4 : (i : ι) → Module R (ℬ i)] →
                        TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i) ≃ₗ[R]
                          TensorProduct R (DirectSum ι fun i => ℬ i) (DirectSum ι fun i => 𝒜 i)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- An abbreviation for `Π J, HasColimitsOfShape (Discrete J) C`  -/
CategoryTheory.Limits.HasCoproducts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.GroupWithZero.Action.Defs
AddMonoid.natSMulWithZero : {A : Type u_7} → [inst : AddMonoid A] → SMulWithZero ℕ A
-- Mathlib.Topology.Connected.CardComponents
/-- If `f : X → Y` is continuous, open and closed with finite fibers and `Y` has finitely many
connected components, so does `X`.  -/
IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f →
    IsClosedMap f →
      ∀ [Finite (ConnectedComponents Y)],
        Continuous f → (∀ (y : Y), (f ⁻¹' {y}).Finite) → Finite (ConnectedComponents X)
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerCongr_apply_coe : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (e : G ≃* H) (r : ↥(Subsemigroup.center G)),
  ↑((Subgroup.centerCongr e) r) = e ↑r
-- Batteries.Recycling.MonadSatisfying.Basic
_private.Batteries.Recycling.MonadSatisfying.Basic.0.SatisfiesM_EStateM_eq.match_1_3.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 :
    (a_1 : α) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.ok a_1 s'_1 → motive (EStateM.Result.ok a_1 s'_1))
  (h_2 :
    (e : ε) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.error e s'_1 → motive (EStateM.Result.error e s'_1)),
  (match q : EStateM.Result.ok a s' with
    | EStateM.Result.ok a_1 s'_1 => h_1 a_1 s'_1 q
    | EStateM.Result.error e s'_1 => h_2 e s'_1 q) =
    h_1 a s' ⋯
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instSmallPropQCPrecoverage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.propQCPrecoverage P).Small
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- We say that a topology on `R` is valuative if the neighborhoods of `0` in `R`
are determined by the valuative relation `· ≤ᵥ ·`.  -/
IsValuativeTopology : (R : Type u_1) → [inst : Ring R] → [ValuativeRel R] → [TopologicalSpace R] → Prop
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X Y : C} (p : X ⟶ Y) (f : F.obj ⊥ ⟶ X)
  (g : c.pt ⟶ Y) (j : Jᵒᵖ),
  (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g).obj j =
    CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g (Opposite.unop j)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_insertEntry_le_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k},
        (compare (Std.Internal.List.minKey! (Std.Internal.List.insertEntry k v l)) (Std.Internal.List.minKey! l)).isLE =
          true
-- Mathlib.Algebra.GradedMonoid
List.dProdIndex_eq_map_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddMonoid ι] (l : List α) (fι : α → ι), l.dProdIndex fι = (List.map fι l).sum
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder.name : Lean.Lsp.WorkspaceFolder → String
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.isLeft_left : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {c : γ},
  Sum.LiftRel r s x (Sum.inl c) → x.isLeft = true
-- Init.System.IO
IO.FS.DirEntry.mk : System.FilePath → String → IO.FS.DirEntry
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.wellFoundedLT' : ∀ {α : Type u_1} {N : Type u_3} [inst : AddMonoid N] [inst_1 : PartialOrder N] [IsBotZeroClass N] [WellFoundedLT N],
  WellFoundedLT (α →₀ N)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inr_toNormalization_normalizationCoprodIso_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme}
  (h :
    AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿
        AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iV f) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp iV
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).inv h)) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.zero_tensor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.tensorHom 0 f = 0
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.IsUnit.kronecker : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_3} {m : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] {x : Matrix n n R} {y : Matrix m m R},
  IsUnit x → IsUnit y → IsUnit (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y)
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_add_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (a : G),
  IsOpenMap fun x => a + x
-- Mathlib.Algebra.Free
FreeAddMagma.instAdd.eq_1 : ∀ {α : Type u}, FreeAddMagma.instAdd = { add := FreeAddMagma.add }
-- Init.Data.List.MinMaxIdx
List.apply_minOn_lt_apply_getElem_of_lt_minIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {k : ℕ} (hk : k < List.minIdxOn f xs h),
  f (List.minOn f xs h) < f xs[k]
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_nonneg : ∀ {x : ℝ}, 1 ≤ x → 0 ≤ Real.arcosh x
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_inv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Inv γ] (f : α → β) (g : α → γ) (e : β → γ),
  Function.extend f g⁻¹ e⁻¹ = (Function.extend f g e)⁻¹
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveMessageProps.mk.injEq : ∀ (msg msg_1 : Lean.Server.WithRpcRef Lean.MessageData), ({ msg := msg } = { msg := msg_1 }) = (msg = msg_1)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between the negation of two vectors.  -/
InnerProductGeometry.angle_neg_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle (-x) (-y) = InnerProductGeometry.angle x y
-- Init.Data.Dyadic.Basic
Dyadic.neg_add_cancel : ∀ (x : Dyadic), -x + x = 0
-- Mathlib.Analysis.InnerProductSpace.PiL2
Fin.cast.hcongr_4 : ∀ (n n' : ℕ),
  n = n' →
    ∀ (m m' : ℕ),
      m = m' →
        ∀ (eq : n = m) (eq' : n' = m'), eq ≍ eq' → ∀ (i : Fin n) (i' : Fin n'), i ≍ i' → Fin.cast eq i ≍ Fin.cast eq' i'
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_mem_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {x : α}, x ∈ l → l.formPerm x ∈ l
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.basis_one : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (hdeg : 1 < f.natDegree), h.basis ⟨1, hdeg⟩ = h.root
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α], ↑⊤ = Set.univ