mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.terminalComparison_isIso_of_preservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F],
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.terminalComparison F)
-- Mathlib.Algebra.Order.SuccPred
Order.IsSuccLimit.natCast_lt : ∀ {α : Type u_1} {x : α} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α],
  Order.IsSuccLimit x → ∀ (n : ℕ), ↑n < x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_le_size_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, m.size ≤ (m.insertIfNew k v).size
-- Mathlib.Algebra.Order.Monoid.Units
Units.min_val : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α] (a b : αˣ), ↑(min a b) = min ↑a ↑b
-- Lean.Level
Lean.Level.PP.Result.imaxNode : List Lean.Level.PP.Result → Lean.Level.PP.Result
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `L / K` is a purely inseparable field extension, then it is `p`-radical. In particular, if
`L` is perfect, then the (relative) perfect closure `perfectClosure K L` is a perfect closure
of `K`, that is, `IsPerfectClosure (algebraMap K (perfectClosure K L)) p`.  -/
IsPurelyInseparable.isPRadical : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (p : ℕ) [ExpChar K p]
  [IsPurelyInseparable K L], IsPRadical (algebraMap K L) p
-- Mathlib.Order.Max
IsMin.mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → b ≤ a → IsMin b
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk_eq_zero : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x : R} (hx : x ∈ s), ⟨x, hx⟩ = 0 ↔ x = 0
-- Std.Async.Basic
/-- Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
`AsyncTask` resolves to that error.
 -/
Std.Async.AsyncTask.mapTaskIO : {α β : Type} →
  (α → IO β) →
    Std.Async.AsyncTask α →
      optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Std.Async.AsyncTask β)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.lhom_ext' : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  {α : Type u_6} [inst_3 : Module R M] [inst_4 : Module R N] ⦃φ ψ : SkewMonoidAlgebra M α →ₗ[R] N⦄,
  (∀ (a : α), φ ∘ₗ SkewMonoidAlgebra.lsingle R a = ψ ∘ₗ SkewMonoidAlgebra.lsingle R a) → φ = ψ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Rci α} [LE α] [inst : Std.PRange.UpwardEnumerable α]
  [inst_1 : Std.PRange.LawfulUpwardEnumerable α] [inst_2 : Std.Rxi.IsAlwaysFinite α],
  List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.Probability.Decision.BayesEstimator
/-- The risk of an argmin estimator is the risk lower bound
`∫⁻ x, ⨅ z, ∫⁻ θ, ℓ θ z ∂(P†π) x ∂(P ∘ₘ π)`.  -/
ProbabilityTheory.IsArgminEstimator.avgRisk_eq_lintegral_iInf : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ] {f : 𝓧 → 𝓨} [inst_2 : ProbabilityTheory.IsFiniteKernel P]
  [inst_3 : MeasureTheory.IsFiniteMeasure π] (hf : ProbabilityTheory.IsArgminEstimator ℓ P π f),
  Measurable (Function.uncurry ℓ) →
    ProbabilityTheory.avgRisk ℓ P hf.kernel π =
      ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x ∂π.bind ⇑P
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.ext : ∀ {R : Type u_1} [inst : NonUnitalRing R] {p q : RingNorm R}, (∀ (x : R), p x = q x) → p = q
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.normalizedFactors_nodup : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsRadical a → (UniqueFactorizationMonoid.normalizedFactors a).Nodup
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} [inst_2 : Inhabited (γ k)],
  (Std.ExtDTreeMap.map f t).get! k = (Option.map (f k) (t.get? k)).get!
-- Mathlib.ModelTheory.Basic
/-- Passes a `DecidableEq` instance on a type of relation symbols through the  `Language`
constructor. Despite the fact that this is proven by `inferInstance`, it is still needed -
see the `example`s in `ModelTheory/Ring/Basic`.  -/
FirstOrder.Language.instDecidableEqRelations : {f : ℕ → Type u_1} →
  {R : ℕ → Type u_2} → (n : ℕ) → [DecidableEq (R n)] → DecidableEq ({ Functions := f, Relations := R }.Relations n)
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `C` has a terminal object and binary products, then it has a product for objects indexed by
`Fin n`.
This is a helper lemma for `hasFiniteProducts_of_has_binary_and_terminal`, which is more general
than this.
 -/
_private.Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts.0.CategoryTheory.hasProduct_fin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C]
  [CategoryTheory.Limits.HasTerminal C] (n : ℕ) (f : Fin n → C), CategoryTheory.Limits.HasProduct f
-- Aesop.RuleSet
/-- Unsafe rules registered in this rule set.
 -/
Aesop.BaseRuleSet.unsafeRules : Aesop.BaseRuleSet → Aesop.Index Aesop.UnsafeRuleInfo
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The sheaf of smooth functions from `M` to `R`, for `R` a smooth commutative ring, as a sheaf of
commutative rings.  -/
smoothSheafCommRing : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [ContMDiffRing I (↑⊤) R] → TopCat.Sheaf CommRingCat (TopCat.of M)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the short complex in `ModuleCat k` given by `A --N--> A --(ρ(g) - 𝟙)--> A`
where `N` is the norm map. Its homology is `Hⁱ(G, A)` for even `i` and `Hᵢ(G, A)` for odd `i`.  -/
Rep.FiniteCyclicGroup.normHomCompSub : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] → [Fintype G] → Rep.{u_1, u, u} k G → G → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A coequalizer of an idempotent morphism and the identity is split epi.  -/
CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {f : X ⟶ X} →
        CategoryTheory.CategoryStruct.comp f f = f →
          {c : CategoryTheory.Limits.Cofork (CategoryTheory.CategoryStruct.id X) f} →
            CategoryTheory.Limits.IsColimit c → CategoryTheory.SplitEpi c.π
-- Mathlib.Data.Finsupp.Defs
/-- The (not exposed) support of `Finsupp.onFinset`.  -/
Finsupp.onFinsetSupport : {α : Type u_1} → {M : Type u_4} → [Zero M] → Finset α → (α → M) → Finset α
-- Std.Data.HashMap.Basic
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.HashMap.Equiv : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Std.HashMap α β → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ofι_π_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {P : C} (ι : P ⟶ X)
  (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂))
  (X_1 : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.Trident.ofι ι w).π.app X_1 =
    CategoryTheory.Limits.WalkingParallelFamily.casesOn X_1 ι
      (CategoryTheory.CategoryStruct.comp ι (f (Classical.arbitrary J)))
-- Aesop.Forward.State
Aesop.Hyp.mk.injEq : ∀ (fvarId? : Option Lean.FVarId) (subst : Aesop.Substitution) (fvarId?_1 : Option Lean.FVarId)
  (subst_1 : Aesop.Substitution),
  ({ fvarId? := fvarId?, subst := subst } = { fvarId? := fvarId?_1, subst := subst_1 }) =
    (fvarId? = fvarId?_1 ∧ subst = subst_1)
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_ofFin : ∀ (n : Fin UInt16.size), (UInt16.ofFin n).toBitVec = { toFin := n }
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instMax.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instMax = { max := fun s t => { carrier := ↑s ∪ ↑t, lower' := ⋯ } }
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.mk : Lean.LocalContext → Lean.Syntax → Lean.Syntax → Lean.Elab.MacroExpansionInfo
-- Mathlib.Algebra.Module.Equiv.Basic
Units.toEquiv_mulRightLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (u : Aˣ), (Units.mulRightLinearEquiv R u).toEquiv = u.mulRight
-- Mathlib.Topology.Algebra.Monoid
Inseparable.mul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {a b c d : M},
  Inseparable a b → Inseparable c d → Inseparable (a * c) (b * d)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {E : Type u₂} [inst_4 : CategoryTheory.Category.{v₂, u₂} E]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory E] (G : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty D) G]
  [inst_8 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (F.comp G)],
  CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso (F.comp G) =
    G.mapIso (CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso F) ≪≫
      CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso G
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieRing.toNonUnitalNonAssocRing : {L : Type u_1} → [self : RightPreLieRing L] → NonUnitalNonAssocRing L
-- Init.Grind.ToInt
Lean.Grind.IntInterval.io.injEq : ∀ (hi hi_1 : ℤ), (Lean.Grind.IntInterval.io hi = Lean.Grind.IntInterval.io hi_1) = (hi = hi_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_of_isEmpty_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {ρ : Type w}
  [inst_2 : ForIn Id ρ α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).isEmpty = true → m.isEmpty = true
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
FixedBy.intermediateField.congr_simp : ∀ {M : Type u} [inst : Monoid M] (K : Type u_1) (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F]
  (m m_1 : M),
  m = m_1 →
    ∀ [inst_3 : Field K] [inst_4 : Algebra K F] [inst_5 : SMulCommClass M K F],
      FixedBy.intermediateField K F m = FixedBy.intermediateField K F m_1
-- Mathlib.Algebra.Lie.Basic
LieEquiv.ofBijective_toFun : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ⇑f) (a : L₁),
  (LieEquiv.ofBijective f h) a = f a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Const.ofList l cmp).getKey? k = none
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.finsum_section_of_locallyFinite : ∀ {𝕜 : 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] {u : Set M} {x₀ : M} {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) u x₀) →
      ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩) u x₀
-- Lean.Elab.DocString
/-- Environment extension for code block suggestions  -/
Lean.Doc.codeBlockSuggestionExt : Lean.SimpleScopedEnvExtension Lean.Name Lean.NameSet
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestRevMatchAtChain_iff_toList : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain p pos pos' ↔
    ∃ (h : pos ≤ pos'), ∀ c ∈ (s.slice pos pos' h).copy.toList, p c = true
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mkFunctor_map_edge : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E)
  (G : CategoryTheory.Functor D E) (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G)
  (c : C) (d : D), (CategoryTheory.Join.mkFunctor F G α).map (CategoryTheory.Join.edge c d) = α.app (c, d)
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesColimitNatIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape J G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C),
  (CategoryTheory.preservesColimitNatIso G).hom.app X = (CategoryTheory.preservesColimitIso G X).hom
-- Mathlib.Topology.LocallyFinsupp
/-- Is analogy to `Finsupp.single`, this definition presents the indicator function
of a single point as a function with locally finite support.
 -/
Function.locallyFinsuppWithin.single : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {Y : Type u_2} → [DecidableEq X] → [inst_2 : Zero Y] → X → Y → Function.locallyFinsupp X Y
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonsquare.ns : ∀ (x : ℕ) [self : Zsqrtd.Nonsquare x] (n : ℕ), x ≠ n * n
-- Init.Data.Iterators.Combinators.Monadic.ULift
/-- Returns the underlying `n`-monadic representation of a `ULiftT n α` value.  -/
Std.Iterators.ULiftT.run : {n : Type (max u v) → Type v'} → {α : Type u} → Std.Iterators.ULiftT n α → n (ULift.{v, u} α)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'XIsoOpcycles.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i),
  K.truncGE'XIsoOpcycles e hi' hi = K.truncGE'XIsoOpcycles e hi' hi
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.mconv_dirac : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] (x : M),
  μ.mconv (MeasureTheory.Measure.dirac x) = MeasureTheory.Measure.map (fun y => y * x) μ
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is strictly concave, then for any point `a` the slope of the secant line of `f`
through `a` and `b` is strictly antitone with respect to `b`.  -/
StrictConcaveOn.secant_strict_mono : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConcaveOn 𝕜 s f →
    ∀ {a x y : 𝕜}, a ∈ s → x ∈ s → y ∈ s → x ≠ a → y ≠ a → x < y → (f y - f a) / (y - a) < (f x - f a) / (x - a)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.liftWith_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ({β : Type u} → StateT σ m β → m (β × σ)) → m α),
  ⦃fun s => (Std.Do.wp (f fun {β} x => x.run s)).apply (fun a => Q.1 a s, Q.2)⦄ MonadControl.liftWith f ⦃Q⦄
-- Mathlib.Order.Monotone.Defs
Function.update_strictMono : ∀ {ι : Type u_1} {π : ι → Type u_3} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {f : (i : ι) → π i}
  {i : ι}, StrictMono (Function.update f i)
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.ofSubtype_inj : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Finset α} {g h : ↥(alternatingGroup ↥s)},
  (alternatingGroup.ofSubtype s) g = (alternatingGroup.ofSubtype s) h ↔ g = h
-- Std.Http.Test.Helpers
/-- Assert the response contains exactly `n` occurrences of `"HTTP/1.1 "`.
 -/
Std.Http.Internal.Test.assertResponseCount : ByteArray → ℕ → IO Unit
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.nhdsWithin_isUnit_neBot : ∀ {α : Type u_2} [inst : NontriviallyNormedField α], (nhdsWithin 0 {x | IsUnit x}).NeBot
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.ofStarRingHom_symm_apply : ∀ {F : Type u_1} {G : Type u_2} {A : Type u_3} {B : Type u_4} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : FunLike F A B]
  [inst_5 : NonUnitalRingHomClass F A B] [inst_6 : NonUnitalStarRingHomClass F A B] [inst_7 : FunLike G B A] (f : F)
  (g : G) (h₁ : ∀ (x : A), g (f x) = x) (h₂ : ∀ (x : B), f (g x) = x) (a : B),
  (StarRingEquiv.ofStarRingHom f g h₁ h₂).symm a = g a
-- Init.Data.UInt.Bitwise
UInt16.and_self : ∀ {a : UInt16}, a &&& a = a
-- Mathlib.Data.Fin.SuccPred
Fin.lt_castPred_succ : ∀ {n : ℕ} {a : Fin (n + 1)} (ha : a.succ ≠ Fin.last (n + 1)), a < a.succ.castPred ha
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Balls defined using the distance or the edistance coincide  -/
Metric.eball_coe : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : NNReal}, Metric.eball x ↑ε = Metric.ball x ↑ε
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.isStrongGenerator_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator ↔
    P.IsSeparating ∧
      ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [CategoryTheory.Mono i],
        (∀ (G : C), P G → Function.Surjective fun f => CategoryTheory.CategoryStruct.comp f i) → CategoryTheory.IsIso i
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.compl_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)},
  s ∈ MeasureTheory.measurableCylinders α → sᶜ ∈ MeasureTheory.measurableCylinders α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit.injEq : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) (decVar : Lean.FVarId) (h : Lean.Meta.Grind.Arith.Cutsat.UnsatProof)
  (decVars : Array Lean.FVarId) (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr) (decVar_1 : Lean.FVarId)
  (h_1 : Lean.Meta.Grind.Arith.Cutsat.UnsatProof) (decVars_1 : Array Lean.FVarId),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit c₁ decVar h decVars =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofDiseqSplit c₁_1 decVar_1 h_1 decVars_1) =
    (c₁ = c₁_1 ∧ decVar = decVar_1 ∧ h = h_1 ∧ decVars = decVars_1)
-- Mathlib.Data.Vector.Snoc
List.Vector.reverse_snoc : ∀ {α : Type u_1} {n : ℕ} {x : α} (xs : List.Vector α n), (xs.snoc x).reverse = x ::ᵥ xs.reverse
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities : Type
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_mul_single_eq_image : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : DecidableEq G] {r : k} {x : G},
  IsRightRegular x →
    (∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0) →
      (f * SkewMonoidAlgebra.single x r).support = Finset.image (fun x_1 => x_1 * x) f.support
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonal_pullback_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.pullback.fst f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Over.Hom.left
          ((CategoryTheory.Over.pullback f).map
            (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯)))
        (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv)
-- Mathlib.Topology.Separation.SeparatedNhds
separatedNhds_iff_disjoint : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t ↔ Disjoint (nhdsSet s) (nhdsSet t)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.cancelVar'.eq_def : ∀ (c : ℤ) (x : Lean.Grind.CommRing.Var) (p acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.cancelVar' c x p acc =
    match p with
    | Lean.Grind.CommRing.Poly.num k => acc.addConst k
    | Lean.Grind.CommRing.Poly.add k m p =>
      have n := m.degreeOf x;
      bif decide (n > 0) && decide (c ^ n ∣ k) then
        Lean.Grind.CommRing.Poly.cancelVar' c x p (Lean.Grind.CommRing.Poly.insert (k / c ^ n) (m.cancelVar x) acc)
      else Lean.Grind.CommRing.Poly.cancelVar' c x p (Lean.Grind.CommRing.Poly.insert k m acc)
-- Init.Data.Bool
Bool.or_self_left : ∀ (a b : Bool), (a || (a || b)) = (a || b)