mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangle_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).obj₃ = X₂
-- Mathlib.Algebra.Star.Unitary
Unitary.mapEquiv_symm_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R ≃⋆* S) (a : ↥(unitary S)), (Unitary.mapEquiv f).symm a = (Unitary.map f.symm.toStarMonoidHom) a
-- Mathlib.Order.Grade
GradeMaxOrder.toGradeOrder : {𝕆 : Type u_5} →
  {α : Type u_6} → {inst : Preorder 𝕆} → {inst_1 : Preorder α} → [self : GradeMaxOrder 𝕆 α] → GradeOrder 𝕆 α
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.toPartialEquiv_injective : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Injective PartialHomeomorph.toPartialEquiv
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The property of morphisms in `FreeRefl V` which are of the form `homMk f`
for some morphism `f : x ⟶ y` in `V`.  -/
CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk : (V : Type u_1) → [inst : CategoryTheory.ReflQuiver V] → CategoryTheory.MorphismProperty (CategoryTheory.Cat.FreeRefl V)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- `CategoryStruct` on `B ⥤ᵒᵖᴸ C` where the (1-)morphisms are given by strong
transformations.  -/
CategoryTheory.Oplax.StrongTrans.categoryStruct : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.OplaxFunctor B C)
-- Mathlib.Analysis.InnerProductSpace.StarOrder
ContinuousLinearMap.IsPositive.spectrumRestricts : ∀ {𝕜 : Type u_1} {H : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [CompleteSpace H] [inst_4 : Algebra ℝ (H →L[𝕜] H)] [IsScalarTower ℝ 𝕜 (H →L[𝕜] H)] {f : H →L[𝕜] H},
  f.IsPositive → SpectrumRestricts f ⇑ContinuousMap.realToNNReal
-- Init.Data.Iterators.Consumers.Monadic.Total
/-- The wrapped iterator, which was wrapped by `IterM.ensureTermination`.
   -/
Std.IterM.Total.it : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM.Total m β → Std.IterM m β
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.notMem_of_mem_sdiff_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.E \ M.closure X → e ∉ X
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- The type of non degenerate simplices of a simplicial set.  -/
SSet.N : SSet → Type u
-- Mathlib.Algebra.Squarefree.Basic
UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  {x : R}, x ≠ 0 → (Squarefree x ↔ (UniqueFactorizationMonoid.normalizedFactors x).Nodup)
-- Lean.Elab.Parallel
_private.Lean.Elab.Parallel.0.Std.Iterators.Types.Internal.TaskIterator.tasks : {α : Type w} → Std.Iterators.Types.Internal.TaskIterator α → List (Task α)
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the reverse direction of `isMaxFilter_dual_iff`. -/
IsMinFilter.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsMaxFilter (⇑OrderDual.toDual ∘ f) l a
-- Mathlib.Algebra.Field.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
DivisionSemiring.zpow_neg' : ∀ {K : Type u_2} [self : DivisionSemiring K] (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Plausible.Testable
/-- Traverse the syntax of a proposition to find universal quantifiers
quantifiers and add `NamedBinder` annotations next to them.  -/
Plausible.Decorations.addDecorations : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryLT? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.ker_baseChange : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T],
  P.baseChange.ker = Ideal.map Algebra.TensorProduct.includeRight.toRingHom P.ker
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.getKey? k = some k' → (Std.ExtTreeMap.filterMap f t)[k]! = (t[k]?.bind (f k')).get!
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_eq_sum : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a : A} {k : ℕ},
  a ^ k = 0 → IsNilpotent.exp a = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • a ^ i
-- Mathlib.Analysis.Convex.Between
sbtw_const_vadd_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (v : V), Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z
-- Mathlib.Algebra.Notation.Prod
Prod.smul_snd : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SMul E α] [inst_1 : SMul E β] (c : E) (p : α × β),
  (c • p).2 = c • p.2
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.const_smul_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x} {u : Set M} {x₀ : M},
  ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u x₀ →
    ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (a • s) x⟩) u x₀
-- Mathlib.Algebra.Group.Prod
Prod.isMulCommutative : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N] [IsMulCommutative M] [IsMulCommutative N],
  IsMulCommutative (M × N)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.mctx : Lean.Elab.Command.FinalizeContext✝ → Lean.MetavarContext
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_eq_add_sum_subtype_ne : ∀ {α : Type u_1} {M : Type u_4} [inst : Fintype α] [inst_1 : AddCommMonoid M] [inst_2 : DecidableEq α] (f : α → M)
  (a : α), ∑ i, f i = f a + ∑ i, f ↑i
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.symm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp}, t₁.Equiv t₂ → t₂.Equiv t₁
-- Mathlib.GroupTheory.Sylow
Sylow.coe_subtype : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P : Sylow p G) {N : Subgroup G} (h : ↑P ≤ N),
  ↑(P.subtype h) = (↑P).subgroupOf N
-- Mathlib.MeasureTheory.Function.L2Space
/-- The inner product in `L2` of the indicator of a set `indicatorConstLp 2 hs hμs (1 : 𝕜)` and
a real or complex function `f` is equal to the integral of `f` over `s`.  -/
MeasureTheory.L2.inner_indicatorConstLp_one : ∀ {α : Type u_1} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (f : ↥(MeasureTheory.Lp 𝕜 2 μ)),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs 1) f = ∫ (x : α) in s, ↑↑f x ∂μ
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.closure_of_finite : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, s.Finite → IsSemilinearSet ↑(AddSubmonoid.closure s)
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- If `a ≠ b`, `c ∈ [a, b]`, `f` is differentiable in the neighborhood of `c` within
`[a, b] \ {c}`, `‖f x‖ → ∞` as `x → c` within `[a, b] \ {c}`, and `f' = O(g)` along
`𝓝[[a, b] \ {c}] c`, where `f'` is the derivative of `f`, then `g` is not interval integrable on
`a..b`.  -/
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_sdiff_singleton : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  {f : ℝ → E} {g : ℝ → F} {a b c : ℝ},
  a ≠ b →
    c ∈ Set.uIcc a b →
      (∀ᶠ (x : ℝ) in nhdsWithin c (Set.uIcc a b \ {c}), DifferentiableAt ℝ f x) →
        Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c (Set.uIcc a b \ {c})) Filter.atTop →
          deriv f =O[nhdsWithin c (Set.uIcc a b \ {c})] g → ¬IntervalIntegrable g MeasureTheory.volume a b
-- Mathlib.Analysis.Convex.Cone.InnerDual
Submodule.closure.eq_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] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] (s : Submodule R M),
  s.closure = { toSubmodule := s.topologicalClosure, isClosed' := ⋯ }
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- Constructor for embeddings between complex shapes when we have an equivalence
`∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)`.  -/
ComplexShape.Embedding.mk' : {ι : Type u_1} →
  {ι' : Type u_2} →
    (c : ComplexShape ι) →
      (c' : ComplexShape ι') →
        (f : ι → ι') → Function.Injective f → (∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)) → c.Embedding c'
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Special case of the standard formula for functions on `ℂ`, with the standard real inner product
structure.
 -/
InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {e : ℂ} {s : Set ℂ} (f : ℂ → F),
  UniqueDiffOn ℝ s →
    e ∈ s →
      InnerProductSpace.laplacianWithin f s e =
        (iteratedFDerivWithin ℝ 2 f s e) ![1, 1] + (iteratedFDerivWithin ℝ 2 f s e) ![Complex.I, Complex.I]
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_reducible : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)]
  [inst_2 : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α}, ¬Irreducible p → p.count = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `F : X → R → R` tends to `f : R → R` uniformly on the spectrum of `a`, and all
these functions are continuous on the spectrum and map zero to itself, then
`fun x ↦ cfcₙ (F x) a` tends to `cfcₙ f a`.  -/
tendsto_cfcₙ_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : SMulCommClass R A A] [inst_11 : IsScalarTower R A A]
  [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] {l : Filter X} {F : X → R → R} {f : R → R} {a : A},
  TendstoUniformlyOn F f l (quasispectrum R a) →
    (∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)) →
      (∀ᶠ (x : X) in l, F x 0 = 0) → Filter.Tendsto (fun x => cfcₙ (F x) a) l (nhds (cfcₙ f a))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Any structured arrow factors through a universal arrow.  -/
CategoryTheory.StructuredArrow.IsUniversal.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal)
  (g : CategoryTheory.StructuredArrow S T), CategoryTheory.CategoryStruct.comp f.hom (T.map (h.desc g)) = g.hom
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.eq_1 : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn assignments none = assignments
-- Mathlib.Algebra.Group.ULift
ULift.cancelCommMonoid : {α : Type u} → [CancelCommMonoid α] → CancelCommMonoid (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The left adjoint of the adjunction which induces the monad `(T, η_ T, μ_ T)`.  -/
CategoryTheory.Kleisli.Adjunction.toKleisli : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (T : CategoryTheory.Monad C) → CategoryTheory.Functor C (CategoryTheory.Kleisli T)
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_zero_eq : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, p.closedBall 0 r = {y | p y ≤ r}
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : M.Derivation φ}
  (desc : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M'))
  (fac :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
        d.postcomp (desc d') = d')
      PresheafOfModules.Derivation.Universal.fac._autoParam)
  (postcomp_injective :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
        d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
      PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam)
  (desc_1 : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M'))
  (fac_1 :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
        d.postcomp (desc_1 d') = d')
      PresheafOfModules.Derivation.Universal.fac._autoParam)
  (postcomp_injective_1 :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
        d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
      PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam),
  ({ desc := desc, fac := fac, postcomp_injective := postcomp_injective } =
      { desc := desc_1, fac := fac_1, postcomp_injective := postcomp_injective_1 }) =
    (desc = desc_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_nonneg : ∀ {α : Type u} [inst : Zero α] [inst_1 : LE α] {a : α}, 0 ≤ ↑a ↔ 0 ≤ a
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSubNegAddMonoid : {α : Type u_1} → [SubNegMonoid α] → SubNegMonoid αᵒᵈ
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ones_sizeUpTo : ∀ (n i : ℕ), (Composition.ones n).sizeUpTo i = min i n
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {γ : Path a b},
  curveIntegralFun 0 γ = 0
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Convert arrows in the category of groupoids to functors,
which sometimes helps in applying simp lemmas  -/
CategoryTheory.Grpd.comp_eq_comp : ∀ {C D E : CategoryTheory.Grpd} (f : C ⟶ D) (g : D ⟶ E),
  CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Functor.comp f g
-- Mathlib.Data.Finset.Dedup
/-- Produce a list of the elements in the finite set using choice.  -/
Finset.toList : {α : Type u_1} → Finset α → List α
-- Mathlib.Algebra.Order.Quantale
AddQuantale.bot_add : ∀ {α : Type u_3} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α] {x : α}, ⊥ + x = ⊥
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.inclusion.congr_simp : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂),
  StarSubalgebra.inclusion h = StarSubalgebra.inclusion h
-- Init.Data.SInt.Lemmas
Int8.cast_toNatClampNeg : ∀ (x : Int8), 0 ≤ x → ↑x.toNatClampNeg = x.toInt
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.TreeMap.Raw.unitOfList l cmp).isEmpty = l.isEmpty
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subRight_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [IsTopologicalAddGroup H] [inst_3 : PartialOrder H]
  [IsOrderedAddMonoid H] {c a : H},
  Filter.map (fun x => x - c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a - c) (Set.Ioi (a - c))
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkLeft_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}, ProbabilityTheory.Kernel.prodMkLeft α 0 = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.getKey! a = (t.getKey? a).get!
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommSemiring.toSemiring : Lean.Meta.Sym.Arith.CommSemiring → Lean.Meta.Sym.Arith.Semiring
-- Mathlib.Order.InitialSeg
/-- Initial segment embedding from an empty type.  -/
InitialSeg.ofIsEmpty : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [IsEmpty α] → InitialSeg r s
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurable_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : MeasurableSpace β]
  [inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : BorelSpace β] [inst_6 : MeasurableSpace γ]
  [inst_7 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_8 : OpensMeasurableSpace γ]
  [inst_9 : SecondCountableTopology γ] (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β),
  MeasureTheory.AEEqFun.compMeasurable g hg f = MeasureTheory.AEEqFun.mk (g ∘ ↑f) ⋯
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm.congr_simp : ∀ (A : Type u_1) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B], Algebra.intNorm A B = Algebra.intNorm A B
-- Mathlib.Algebra.Polynomial.Eval.Subring
Polynomial.mem_map_range : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {p : Polynomial S},
  p ∈ (Polynomial.mapRingHom f).range ↔ ∀ (n : ℕ), p.coeff n ∈ f.range
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_finsetSum : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] [ContinuousAdd ε'] {ι : Type u_9} (s : Finset ι) {f : ι → α → ε'},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → MeasureTheory.Integrable (fun a => ∑ i ∈ s, f i a) μ
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.mono : ∀ {X : Type u_1} {E : Type u_6} {F : Type u_7} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAddCommGroup F] {μ : MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ {g : X → F},
      MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖) → MeasureTheory.LocallyIntegrable g μ
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.coyoneda_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor J C) (j : J), (CategoryTheory.Limits.WeightedCone.coyoneda F j).pt = F.obj j
-- Mathlib.Geometry.Manifold.HasGroupoid
HasGroupoid.compatible : ∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} {inst_2 : ChartedSpace H M}
  {G : StructureGroupoid H} [self : HasGroupoid M G] {e e' : OpenPartialHomeomorph M H},
  e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (hom : M.X ⟶ N.X)
  (left_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam)
  (right_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam)
  (hom_1 : M.X ⟶ N.X)
  (left_act_hom_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom_1) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam)
  (right_act_hom_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom_1 B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam),
  ({ hom := hom, left_act_hom := left_act_hom, right_act_hom := right_act_hom } =
      { hom := hom_1, left_act_hom := left_act_hom_1, right_act_hom := right_act_hom_1 }) =
    (hom = hom_1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseKey_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k l = false → Std.Internal.List.eraseKey k l = l
-- Mathlib.Data.List.Rotate
List.rotate_eq_singleton_iff : ∀ {α : Type u} {l : List α} {n : ℕ} {x : α}, l.rotate n = [x] ↔ l = [x]
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (curr : ℕ)
  (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (idx : ℕ) (hidx : idx < curr)
  (hfoo : aig.decls.size ≤ (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).aig.decls.size),
  (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).vec.get idx ⋯ = (s.get idx hidx).cast hfoo