mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
from the left or from the right at `a`, then `u ↦ ∫ x in u..b, f x` has left (resp., right)
derivative `-f a` at `a`.  -/
intervalIntegral.integral_hasDerivWithinAt_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
      StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
        ContinuousWithinAt f t a → HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) s a
-- Lean.Meta.Basic
/-- Return `some info` if `declName` is an inductive predicate where `info : InductiveVal`.
That is, `inductive` type in `Prop`.
 -/
Lean.Meta.isInductivePredicate? : Lean.Name → Lean.MetaM (Option Lean.InductiveVal)
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
convenience.  -/
spectrum.map_pow_of_pos : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) {n : ℕ},
  0 < n → spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.modifiers : Lean.Elab.Command.InductiveView → Lean.Elab.Modifiers
-- Mathlib.RingTheory.DedekindDomain.Basic
/-- **Alias** of `Ring.DimensionLEOne.of_isIntegral`. -/
Ring.DimensionLEOne.isIntegralClosure : ∀ (R : Type u_1) [inst : CommRing R] (B : Type u_4) [inst_1 : CommRing B] [IsDomain B] [Nontrivial R]
  [inst_4 : Algebra R B] [Algebra.IsIntegral R B] [Ring.DimensionLEOne R], Ring.DimensionLEOne B
-- Aesop.Tree.Data
Aesop.RappId.instDecidableRelLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_ofMul : ∀ {E : Type u_2} [inst : NNNorm E] (x : E), ‖Additive.ofMul x‖₊ = ‖x‖₊
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.inter_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation_neg : ∀ (L : PeriodPair) (x : ℂ), PeriodPair.relation✝ L (-x) = PeriodPair.relation✝ L x
-- Mathlib.Analysis.InnerProductSpace.Continuous
Filter.Tendsto.inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : Type u_4} {f g : α → E} {l : Filter α} {x y : E},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun t => inner 𝕜 (f t) (g t)) l (nhds (inner 𝕜 x y))
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y},
  CategoryTheory.HasLiftingProperty i p → CategoryTheory.HasLiftingProperty p.op i.op
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.range_algebraMap : ∀ {R : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  (algebraMap (↥S) A).range = S.toSubring
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- If `C` is a `V`-enriched ordinary category, and `C` has suitable limits,
then `J ⥤ C` is also a `V`-enriched ordinary category.  -/
CategoryTheory.Enriched.FunctorCategory.enrichedOrdinaryCategory : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u₂) →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          (J : Type u₃) →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                [∀ (F₁ F₂ : CategoryTheory.Functor J C),
                      CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                  CategoryTheory.EnrichedOrdinaryCategory V (CategoryTheory.Functor J C)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.mk.sizeOf_spec : ∀ (language? scheme? pattern? : Option String),
  sizeOf { language? := language?, scheme? := scheme?, pattern? := pattern? } =
    1 + sizeOf language? + sizeOf scheme? + sizeOf pattern?
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [hI : I.IsPrime],
  Ideal.primeHeight✝ I = Order.height { asIdeal := I, isPrime := hI }
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearMap.isBigO_id : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (l : Filter E), ⇑f =O[l] fun x => x
-- Mathlib.Topology.Instances.AddCircle.Real
/-- The "additive circle" `ℝ ⧸ ℤ ∙ p` is compact.  -/
AddCircle.compactSpace : ∀ (p : ℝ) [Fact (0 < p)], CompactSpace (AddCircle p)
-- Mathlib.Data.Int.Bitwise
Int.lor.eq_1 : ∀ (m n : ℕ), (Int.ofNat m).lor (Int.ofNat n) = ↑(m ||| n)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_eq_iff_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite ↥H], Nat.card ↥H = Nat.card G ↔ H = ⊤
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.doc_url? : LeanSearchClient.SearchResult → Option String
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.cotangent_subsingleton_iff : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), Subsingleton I.Cotangent ↔ IsIdempotentElem I
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
instRankConditionOfIsStablyFiniteRingOfNontrivial : ∀ {R : Type u_1} [inst : Semiring R] [IsStablyFiniteRing R] [Nontrivial R], RankCondition R
-- Mathlib.CategoryTheory.Limits.Types.End
/-- The cowedge corresponding to the explicit coend in `Type` is colimiting.  -/
CategoryTheory.Limits.Types.cowedgeIsColimit : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.cowedge F)
-- Lean.Elab.DocString
/-- A suggestion about an applicable role  -/
Lean.Doc.CodeSuggestion : Type
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.not_lt_startPos : ∀ {s : String.Slice} {p : s.Pos}, ¬p < s.startPos
-- Batteries.Data.List.Lemmas
List.countPBefore_of_ge_length : ∀ {α : Type u_1} {i : ℕ} {p : α → Bool} {xs : List α}, xs.length ≤ i → List.countPBefore p xs i = List.countP p xs
-- Mathlib.Data.Multiset.Fold
Multiset.fold.congr_simp : ∀ {α : Type u_1} (op op_1 : α → α → α) (e_op : op = op_1) [hc : Std.Commutative op] [ha : Std.Associative op]
  (a a_1 : α), a = a_1 → ∀ (a_2 a_3 : Multiset α), a_2 = a_3 → Multiset.fold op a a_2 = Multiset.fold op_1 a_1 a_3
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.mkMatchCondProof?.go? : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv.eq_2 : ∀ (m n : ℕ), (Int.ofNat m).ediv (Int.negSucc n) = -Int.ofNat (m / n.succ)
-- Lean.Meta.Tactic.Grind.Types
/-- Pushes `a = Bool.false` with `proof` to `newEqs`.  -/
Lean.Meta.Grind.pushEqBoolFalse : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.smul_mk : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι) (b : α i),
  a • ⟨i, b⟩ = ⟨i, a • b⟩
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_b_eq_one : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 1 → P.toPoly.Monic
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- The equivalence of types underlying a coalgebra equivalence.  -/
CoalgEquiv.toEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → A ≃ B
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_eq_center' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x : P} {R : ℝ}, EuclideanGeometry.inversion c R x = c ↔ x = c ∨ R = 0
-- Mathlib.LinearAlgebra.Dual.Defs
Module.IsReflexive.to_isTorsionFree : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M], Module.IsTorsionFree R M
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddZeroClass : {α : Type u_1} → [AddZeroClass α] → AddZeroClass (Lex α)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.ext : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {f g : ZeroAtInftyContinuousMap α β}, (∀ (x : α), f x = g x) → f = g
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind : Type
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrictHom_symm_apply : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L]
  (σ : B →ₐ[A] B), (galRestrictHom A K L B).symm σ = galLift K L L σ
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal.congr_simp : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {inst : DecidableEq o} [inst_1 : DecidableEq o]
  [inst_2 : Zero α] (M M_1 : o → Matrix m n α),
  M = M_1 →
    ∀ (a a_1 : m × o),
      a = a_1 → ∀ (a_2 a_3 : n × o), a_2 = a_3 → Matrix.blockDiagonal M a a_2 = Matrix.blockDiagonal M_1 a_1 a_3
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (t.insertMany l).getKeyD k' fallback = k
-- Init.Data.Array.Lemmas
Array.getElem?_range' : ∀ {start size step i : ℕ}, (Array.range' start size step)[i]? = if i < size then some (start + step * i) else none
-- Lean.Data.Lsp.Utf16
_private.Lean.Data.Lsp.Utf16.0.Lean.String.utf16PosToCodepointPosFromAux : String → ℕ → String.Pos.Raw → ℕ → ℕ
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.spanningSetsIndex_eq_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] {x : α}
  {n : ℕ}, MeasureTheory.spanningSetsIndex μ x = n ↔ x ∈ disjointed (MeasureTheory.spanningSets μ) n
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousAdd.measurableMul₂ : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [SecondCountableTopology γ]
  [inst_4 : Add γ] [ContinuousAdd γ], MeasurableAdd₂ γ
-- Mathlib.Data.Finset.Prod
Finset.disjoint_diag_offDiag : ∀ {α : Type u_1} (s : Finset α), Disjoint s.diag s.offDiag
-- Init.Data.SInt.Lemmas
Int16.lt_of_le_of_lt : ∀ {a b c : Int16}, a ≤ b → b < c → a < c
-- Mathlib.RingTheory.Artinian.Instances
/-- If each `Rⁿ` is a Artinian `R`-module, then `R` satisfies the strong rank condition.
Not an instance for performance reasons.  -/
StrongRankCondition.of_isArtinian : ∀ (R : Type u_1) [inst : Semiring R] [Nontrivial R] [∀ (n : ℕ), IsArtinian R (Fin n → R)], StrongRankCondition R
-- Mathlib.Topology.MetricSpace.Algebra
NNReal.hasLipschitzAdd : LipschitzAdd NNReal
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections],
  CommGrpCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forIn_eq_forIn_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {δ : Type v} {m' : Type v → Type w}
  [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : α → δ → m' (ForInStep δ)} {init : δ}, forIn m init f = forIn m.toList init f
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.rightUnitor_inv_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.Limits.pullback.snd Y.hom (CategoryTheory.CategoryStruct.id X)) =
    Y.hom
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (ra rb : Lean.Meta.Grind.Arith.CommRing.RingExpr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core a b ra rb) = 1 + sizeOf a + sizeOf b + sizeOf ra + sizeOf rb
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)) (hf : MeasureTheory.Integrable (↑↑f) μ), MeasureTheory.Integrable.toL1 (↑↑f) hf = f
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_pt : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected], 𝒰.coconeOfLocallyDirected.pt = X
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.containsThenInsert.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → m.containsThenInsert a b = m_1.containsThenInsert a_1 b_1
-- Init.Data.Array.Lemmas
Array.back!_push : ∀ {α : Type u_1} [inst : Inhabited α] {xs : Array α} {x : α}, (xs.push x).back! = x
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {toSubring : Subring R} {isLocalRing : IsLocalRing ↥toSubring}
  {toSubring_1 : Subring R} {isLocalRing_1 : IsLocalRing ↥toSubring_1},
  { toSubring := toSubring, isLocalRing := isLocalRing } = { toSubring := toSubring_1, isLocalRing := isLocalRing_1 } →
    toSubring = toSubring_1
-- Aesop.Tree.Free
Aesop.RappRef.free : Aesop.RappRef → BaseIO Unit
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → (↑(mfderiv% ↑e x)).ker = ⊥
-- Mathlib.Algebra.Polynomial.Monomial
Polynomial.monomial_one_eq_iff : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] {i j : ℕ},
  (Polynomial.monomial i) 1 = (Polynomial.monomial j) 1 ↔ i = j
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.preimage_image_coe : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (s : Set G),
  QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' s = ↑N + s
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_X_pow_mul : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ℕ),
  (Polynomial.X ^ n * p).smeval x = x ^ n * p.smeval x
-- Mathlib.Order.SymmDiff
symmDiff_eq_sup_sdiff_inf : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b = (a ⊔ b) \ (a ⊓ b)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).counitIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mono'_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε}
  {g : α → ENNReal},
  MeasureTheory.HasFiniteIntegral g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Data.Fintype.Pi
/-- Given for all `a : α` a finset `t a` of `δ a`, then one can define the
finset `Fintype.piFinset t` of all functions taking values in `t a` for all `a`. This is the
analogue of `Finset.pi` where the base finset is `univ` (but formally they are not the same, as
there is an additional condition `i ∈ Finset.univ` in the `Finset.pi` definition).  -/
Fintype.piFinset : {α : Type u_1} → [DecidableEq α] → [Fintype α] → {δ : α → Type u_4} → ((a : α) → Finset (δ a)) → Finset ((a : α) → δ a)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) →
          (x : Turing.TM2.Stmt Γ Λ σ) →
            ((k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q)) →
              ((k : K) →
                  (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q)) →
                ((k : K) →
                    (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q)) →
                  ((a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q)) →
                    ((a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂)) →
                      ((l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) → (Unit → motive Turing.TM2.Stmt.halt) → motive x
-- Mathlib.Algebra.Group.Commute.Units
isAddUnit_nsmul_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {n : ℕ} {a : M}, n ≠ 0 → (IsAddUnit (n • a) ↔ IsAddUnit a)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.continuousWithinAt_rightLim : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [CompleteSpace E] [T3Space E] {f : α → E},
  BoundedVariationOn f Set.univ → ∀ {x : α}, ContinuousWithinAt (Function.rightLim f) (Set.Ici x) x
-- Mathlib.Order.WithBot
Equiv.withTopSubtypeNe_apply : ∀ {α : Type u_1} (x : { y // y ≠ ⊤ }),
  Equiv.withTopSubtypeNe x =
    match x with
    | ⟨x, h⟩ => x.untop h
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.not_isLittleO : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {g' : α → F'} {f'' : α → E''} {l : Filter α}, f'' =O[l] g' → (∃ᶠ (x : α) in l, f'' x ≠ 0) → ¬g' =o[l] f''
-- Mathlib.Analysis.Complex.Exponential
Real.exp_lt_exp : ∀ {x y : ℝ}, Real.exp x < Real.exp y ↔ x < y
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_le_toSubmodule : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] {s t : ClosedSubmodule R M}, ↑s ≤ ↑t ↔ s ≤ t
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd_ae_eq_condExpIndSMul : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G),
  ↑↑((MeasureTheory.condExpInd G hm μ s) x) =ᵐ[μ] ↑↑(MeasureTheory.condExpIndSMul hm hs hμs x)
-- Mathlib.Analysis.InnerProductSpace.Calculus
OpenPartialHomeomorph.contDiff_univBall : ∀ {n : ℕ∞} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {c : E} {r : ℝ},
  ContDiff ℝ ↑n ↑(OpenPartialHomeomorph.univBall c r)
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.mul_nonpos : ∀ {α : Type u} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α}, a ≤ 0 → 0 < b → b * a ≤ 0
-- Mathlib.Data.Rel
SetRel.symmetrize_subset_inv : ∀ {α : Type u_1} {R : SetRel α α}, R.symmetrize ⊆ R.inv
-- Init.Data.Array.Lemmas
/-- Variant of `foldrM_reverse` with a side condition for the `start` argument.  -/
Array.foldrM_reverse' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {f : α → β → m β} {b : β}
  {start : ℕ}, start = xs.size → Array.foldrM f b xs.reverse start = Array.foldlM (fun x y => f y x) b xs
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the natural transformation
`H ⟶ F` is epic at `X` iff the image of the counit of the adjunction `G ⊣ H` under `F` is.  -/
CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff_epi_map_adj₂_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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  {X : C}, CategoryTheory.Epi (t.rightToLeft.app X) ↔ CategoryTheory.Epi (F.map (t.adj₂.counit.app X))
-- Init.Data.Array.Monadic
Array.foldrM_map : ∀ {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {start : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : β₁ → β₂} {g : β₂ → α → m α} {xs : Array β₁} {init : α} {w : start = xs.size},
  Array.foldrM g init (Array.map f xs) start = Array.foldrM (fun x y => g (f x) y) init xs start
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.neBot_cobounded_of_noTopOrder : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α] [NoTopOrder α],
  (Bornology.cobounded α).NeBot
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_coe : ∀ {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 : A ≃ₐc[R] B), ⇑↑e = ⇑e