mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Register a new `UnfoldBoundaryExt`.  -/
Mathlib.Tactic.UnfoldBoundary.registerUnfoldBoundaryExt : IO Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt
-- Mathlib.Data.Set.Inclusion
Set.inclusion_right : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t) (x : ↑t) (m : ↑x ∈ s), Set.inclusion h ⟨↑x, m⟩ = x
-- Mathlib.FieldTheory.Separable
Polynomial.count_roots_le_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] {p : Polynomial R},
  p.Separable → ∀ (x : R), Multiset.count x p.roots ≤ 1
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsLocalizedFullyFaithfulFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierRightLocalizing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C] [inst_7 : A.IsTriangulated]
  [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierRightLocalizing B],
  (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.biInf : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} (s : Set ι) {f : ι → δ → α},
  s.Countable → (∀ i ∈ s, Measurable (f i)) → Measurable fun b => ⨅ i ∈ s, f i b
-- Mathlib.Control.Functor
/-- Construct a term of `Comp F G α` from a term of `F (G α)`, which is the same type.
Can be used as a pattern to extract a term of `F (G α)`.  -/
Functor.Comp.mk : {F : Type u → Type w} → {G : Type v → Type u} → {α : Type v} → F (G α) → Functor.Comp F G α
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Ioc : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a b : R},
  0 ≤ a → 0 ≤ b → Nat.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊
-- Init.Data.AC
Lean.Data.AC.instEvalInformationContext : {α : Sort u_1} → Lean.Data.AC.EvalInformation (Lean.Data.AC.Context α) α
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotEquivQuotMap_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (I : Ideal R)
  (a : Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f}),
  (AdjoinRoot.quotEquivQuotMap f I).symm a = (AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f).symm a
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff_null : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  μ.real s₂ = 0 → autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_sdiff_null._auto_1 → μ.real (s₁ \ s₂) = μ.real s₁
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (G : CategoryTheory.Functor D H),
  CategoryTheory.CategoryStruct.comp (L.lanUnit.app (L.comp G)) (L.whiskerLeft ((L.lanAdjunction H).counit.app G)) =
    CategoryTheory.CategoryStruct.id (L.comp G)
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.mono_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂),
  (∀ (X : Cᵒᵖ), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (φ.hom.app X))) → CategoryTheory.Mono φ
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.smul_units_def : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] (f : A₁ ≃ₐ[R] A₁)
  (x : A₁ˣ), f • x = (Units.map ↑f) x
-- Mathlib.Algebra.MvPolynomial.Eval
/-- Version of `aeval` for defining algebra homs out of `MvPolynomial σ R` over a smaller base ring
than `R`.  -/
MvPolynomial.aevalTower : {R : Type u} →
  {σ : Type u_1} →
    [inst : CommSemiring R] →
      {S : Type u_2} →
        {A : Type u_3} →
          [inst_1 : CommSemiring S] →
            [inst_2 : CommSemiring A] →
              [inst_3 : Algebra S R] → [inst_4 : Algebra S A] → (R →ₐ[S] A) → (σ → A) → MvPolynomial σ R →ₐ[S] A
-- Lean.Syntax
Lean.Syntax.ifNode : {β : Sort u_1} → Lean.Syntax → (Lean.SyntaxNode → β) → (Unit → β) → β
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SimpCacheKey.extras : Lean.Elab.Tactic.Grind.SimpCacheKey → Array Lean.Elab.Tactic.Grind.ExtraTheorem
-- Mathlib.Data.DFinsupp.BigOperators
map_dfinsuppSum : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3}
  [inst_1 : (i : ι) → Zero (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid R]
  [inst_4 : AddCommMonoid S] [inst_5 : FunLike H R S] [AddMonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i → R), h (f.sum g) = f.sum fun a b => h (g a b)
-- Mathlib.Probability.Moments.Basic
/-- This is a trivial application of `IndepFun.comp` but it will come up frequently.  -/
ProbabilityTheory.IndepFun.exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (s t : ℝ), ProbabilityTheory.IndepFun (fun ω => Real.exp (s * X ω)) (fun ω => Real.exp (t * Y ω)) μ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Distance between two points  -/
Dist.dist : {α : Type u_3} → [self : Dist α] → α → α → ℝ
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.comap' : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter β} {m : α → β},
  Cauchy f →
    Filter.comap (fun p => (m p.1, m p.2)) (uniformity β) ≤ uniformity α →
      (Filter.comap m f).NeBot → Cauchy (Filter.comap m f)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_zsmul_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocDiv hp a (m • p + b) = m + toIocDiv hp a b
-- Mathlib.Computability.Primrec.Basic
Primrec.decode₂ : ∀ {α : Type u_1} [inst : Primcodable α], Primrec (Encodable.decode₂ α)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.preimage_image_mk_eq_mul : ∀ {α : Type u_1} [inst : Group α] (N : Subgroup α) (s : Set α), QuotientGroup.mk ⁻¹' QuotientGroup.mk '' s = s * ↑N
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Ω₀ Ω : C) →
      (truth : Ω₀ ⟶ Ω) →
        autoParam (CategoryTheory.Mono truth) CategoryTheory.Subobject.Classifier.mono_truth._autoParam →
          (χ₀ : (U : C) → U ⟶ Ω₀) →
            (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) →
              (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m],
                  CategoryTheory.IsPullback m (χ₀ U) (χ m) truth) →
                (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀} {χ' : X ⟶ Ω},
                    CategoryTheory.IsPullback m χ₀' χ' truth → χ' = χ m) →
                  CategoryTheory.Subobject.Classifier C
-- Mathlib.Topology.UniformSpace.Separation
eq_of_uniformity : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α] {x y : α},
  (∀ {V : Set (α × α)}, V ∈ uniformity α → (x, y) ∈ V) → x = y
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {f g : M → E'}, MDiffAt[s] f z → MDiffAt[s] g z → MDiffAt[s] (f - g) z
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldlM_eq_foldlM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.DTreeMap.Raw.foldlM f init t = Array.foldlM (fun a b => f a b.1 b.2) init (Std.DTreeMap.Raw.Const.toArray t)
-- Batteries.Data.List.Basic
List.replaceFTR.go.eq_def : ∀ {α : Type u_1} (f : α → Option α) (a : List α) (a_1 : Array α),
  List.replaceFTR.go f a a_1 =
    match a, a_1 with
    | [], acc => acc.toList
    | x :: xs, acc =>
      match f x with
      | none => List.replaceFTR.go f xs (acc.push x)
      | some a' => acc.toListAppend (a' :: xs)
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.whiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : CategoryTheory.Center C) → {Y₁ Y₂ : CategoryTheory.Center C} → (Y₁ ⟶ Y₂) → (X.tensorObj Y₁ ⟶ X.tensorObj Y₂)
-- Lean.Data.PersistentArray
Lean.PersistentArray.shift : {α : Type u} → Lean.PersistentArray α → USize
-- Mathlib.Data.Finset.Erase
Finset.erase_eq_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → s.erase a = s
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_comm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (f₁ - f₂) =O[𝕜; l] g ↔ (f₂ - f₁) =O[𝕜; l] g
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mrefinePat?_ : Lean.ParserDescr
-- Mathlib.Tactic.Translate.Reorder
/-- Return the minimum size of an array on which the given reorder is valid.  -/
Mathlib.Tactic.Translate.ArgReorder.range : Mathlib.Tactic.Translate.ArgReorder → ℕ
-- Mathlib.Topology.Closure
mem_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
-- Mathlib.Combinatorics.Quiver.Push
Quiver.Push.lift_obj : ∀ {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [inst_1 : Quiver W'] (φ : V ⥤q W')
  (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)), (Quiver.Push.lift σ φ τ h).obj = τ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter_eq_false_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) = false
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.sourceAffineLocally_isLocal : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P) →
        (AlgebraicGeometry.sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).IsLocal
-- Lean.Meta.Tactic.Apply
/-- Short-hand for applying a constant to the goal.  -/
Lean.MVarId.applyConst : Lean.MVarId → Lean.Name → optParam Lean.Meta.ApplyConfig { } → Lean.MetaM (List Lean.MVarId)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone K →
    ∀ (w : NumberField.InfinitePlace K), 0 < (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.map : ∀ {R : Type u} [inst : CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R},
  f.IsWeaklyEisensteinAt 𝓟 →
    ∀ {A : Type v} [inst_1 : CommSemiring A] (φ : R →+* A), (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)
-- Init.Data.Option.Lemmas
Option.max_filter_left : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {p : α → Bool} {o : Option α}, Option.filter p o ⊔ o = o
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Set.Basic
Set.nonempty_of_ssubset : ∀ {α : Type u} {s t : Set α}, s ⊂ t → (t \ s).Nonempty
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_le_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ∩ t ≤ s
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.exists_of_fg : ∀ {R : Type u} {M : Type u_1} {N : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (u : TensorProduct R M N),
  ∃ P, P.FG ∧ u ∈ (LinearMap.rTensor N P.subtype).range
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.pow_rpow_inv_natCast : ∀ (x : NNReal) {n : ℕ}, n ≠ 0 → (x ^ n) ^ (↑n)⁻¹ = x
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- The map `R ⟶ (X.normalizedChainComplex R).X n` for any `x : X _⦋n⦌`. Note that
this is zero if `x` is a degenerate simplex, see `ιNormalizedChainComplex_eq_zero`.  -/
SSet.ιNormalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → {R : C} → {n : ℕ} → X.obj (Opposite.op { len := n }) → (R ⟶ (X.normalizedChainComplex R).X n)
-- Mathlib.Topology.Instances.CantorSet
cantorSet.eq_1 : cantorSet = ⋂ n, preCantorSet n
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.append.eq_1 : ∀ (p₂ : Lean.Grind.Linarith.Poly), Lean.Grind.Linarith.Poly.nil.append p₂ = p₂
-- Lean.Meta.MkIffOfInductiveProp
/-- Drops the final element of a list.  -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.List.init : {α : Type u_1} → List α → List α
-- Lean.Server.Utils
/-- Current text of the document.
It is maintained such that it is normalized using `String.crlfToLf`, which preserves logical line/column numbers.
(Note: we assume that edit operations never split or merge `\r\n` line endings.)  -/
Lean.Server.DocumentMeta.text : Lean.Server.DocumentMeta → Lean.FileMap
-- Init.Data.UInt.Lemmas
USize.ofNatLT_finVal : ∀ (n : Fin USize.size), USize.ofNatLT ↑n ⋯ = USize.ofFin n
-- Mathlib.RepresentationTheory.Maschke
LinearMap.sumOfConjugatesEquivariant_apply : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [inst_10 : Fintype G] (v : W),
  (LinearMap.sumOfConjugatesEquivariant G π) v = ∑ g, (π.conjugate g) v
-- Mathlib.Algebra.Category.Grp.Limits
/-- We show that the forgetful functor `GrpCat ⥤ MonCat` creates limits.

All we need to do is notice that the limit point has a `Group` instance available, and then reuse
the existing limit.  -/
GrpCat.Forget₂.createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ GrpCat MonCat)
-- Mathlib.Logic.Equiv.Bool
Bool.not_leftInverse : Function.LeftInverse not not
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLawfulUpwardEnumerableLT : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerableLT (BitVec n)
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.mul_denote.go : ∀ (ctx : Nat.Internal.Linear.Context) (p₂ p₁ acc : Nat.Internal.SOM.Poly),
  Nat.Internal.SOM.Poly.denote ctx (Nat.Internal.SOM.Poly.mul.go✝ p₂ p₁ acc) =
    Nat.Internal.SOM.Poly.denote ctx acc + Nat.Internal.SOM.Poly.denote ctx p₁ * Nat.Internal.SOM.Poly.denote ctx p₂
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENatAux_zero : Cardinal.toENatAux 0 = 0
-- Init.Data.Order.PackageFactories
_private.Init.Data.Order.PackageFactories.0.Std.FactoryInstances.isLE_compare : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] {a b : α}, (compare a b).isLE = true ↔ a ≤ b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.pow_monotone : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A},
  1 ≤ a → Monotone fun x => a ^ x
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} (Φ Φ_1 : CategoryTheory.SmallObject.SuccStruct C),
  Φ = Φ_1 →
    ∀ [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
      [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] (j j_1 : J),
      j = j_1 → Φ.Iteration j = Φ_1.Iteration j_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The addition of two nonsingular projective points on a Weierstrass curve `W`.

Given two nonsingular projective points `P` and `Q` on `W`, use `P + Q` instead of `add P Q`.  -/
WeierstrassCurve.Projective.Point.add : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Projective F} → W.Point → W.Point → W.Point
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.inner_orthogonalProjectionOnto_eq_of_mem_left`. -/
Submodule.inner_orthogonalProjection_eq_of_mem_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : ↥K) (v : E),
  inner 𝕜 u (K.orthogonalProjectionOnto v) = inner 𝕜 (↑u) v
-- Mathlib.Data.Finset.Defs
Finset.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : SizeOf α] (val : Multiset α) (nodup : val.Nodup),
  sizeOf { val := val, nodup := nodup } = 1 + sizeOf val + sizeOf nodup
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.inter_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)
-- Mathlib.Tactic.DefEqTransformations
/-- Unfold all the fvars from `fvars` in `e` that have local definitions (are "let-bound").  -/
Mathlib.Tactic.unfoldFVars : Array Lean.FVarId → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.coe_le_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupNorm E}, ⇑p ≤ ⇑q ↔ p ≤ q
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.coe_zeta_mul_moebius : ↑ArithmeticFunction.zeta * ArithmeticFunction.moebius = 1
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries_sub : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeries (f - g) s = LSeries f s - LSeries g s
-- Mathlib.Algebra.Group.End
Equiv.zpow_mulRight : ∀ {α : Type u_4} [inst : Group α] (a : α) (n : ℤ), Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.inr_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  (a : β),
  (LinearOrderedCommGroupWithZero.inr α β) a =
    (WithZero.map' ↑(toLexMulEquiv (αˣ × βˣ))) ((MonoidWithZeroHom.inr α β) a)
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_map_ofDual`. -/
List.SortedLE.map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedLE → l.SortedGE
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.kerParam_injective : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Function.Injective ⇑(Equiv.Perm.OnCycleFactors.kerParam g)
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_inv_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] {q : ℚ}, ↑q.num ≠ 0 → ↑q⁻¹ = (↑q)⁻¹
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.toString : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → s.toString = String.ofList m
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_ciInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_4} {δ' : Type u_6}
  [inst_1 : ConditionallyCompleteLinearOrder δ'] {f : ι → α → δ'},
  (∀ᶠ (y : α) in nhds x, BddBelow (Set.range fun i => f i y)) →
    (∀ (i : ι), UpperSemicontinuousAt (f i) x) → UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState.mk.injEq : ∀ (count generationId count_1 generationId_1 : ℕ),
  ({ count := count, generationId := generationId } = { count := count_1, generationId := generationId_1 }) =
    (count = count_1 ∧ generationId = generationId_1)
-- Mathlib.Data.Fintype.Lattice
Finite.exists_min : ∀ {α : Type u_2} {β : Type u_3} [Finite α] [Nonempty α] [inst : LinearOrder β] (f : α → β), ∃ x₀, ∀ (x : α), f x₀ ≤ f x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback b : β a}, (t.insert a b).getD a fallback = b
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.tprodL_toFun : ∀ {ι : Type u_1} [inst : Fintype ι] (𝕜 : Type u_2) {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (a : (i : ι) → E i),
  (PiTensorProduct.tprodL 𝕜) a = (PiTensorProduct.tprod 𝕜) a
-- Lean.Parser.Term.Basic
Lean.Parser.Term.syntheticHole.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Parser.Term
Lean.Parser.Term.letOptEq.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.drop 0 = p.copy ⋯ ⋯
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G),
  (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeOpEquiv_counitIso : ∀ (J : Type w),
  (CategoryTheory.Limits.widePushoutShapeOpEquiv J).counitIso = CategoryTheory.Limits.widePullbackShapeUnopOp J
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.isLocalVar : Lean.IR.LocalContext → Lean.IR.Index → Bool
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.brecOn.eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C} {ι : C → Type w}
  {motive : (a : C) → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι a → Sort u_1} {a : C}
  (t : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι a)
  (F_1 :
    (a : C) →
      (t : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι a) →
        CategoryTheory.Precoverage.SmallConstruction.Witness.below✝ t → motive a t),
  CategoryTheory.Precoverage.SmallConstruction.Witness.brecOn✝ t F_1 =
    F_1 a t (CategoryTheory.Precoverage.SmallConstruction.Witness.brecOn.go✝ t F_1).2