mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_dite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : Prop} [inst : Decidable p] {μ : p → MeasureTheory.Measure α}
  {ν : ¬p → MeasureTheory.Measure α} [∀ (h : p), MeasureTheory.IsProbabilityMeasure (μ h)]
  [∀ (h : ¬p), MeasureTheory.IsProbabilityMeasure (ν h)], MeasureTheory.IsProbabilityMeasure (dite p μ ν)
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.comp_continuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F) {γ : Type u_5} [inst_4 : TopologicalSpace γ] {g : γ → α}
  {s : Set γ}, ContinuousOn (⇑f ∘ g) s ↔ ContinuousOn g s
-- Lean.Meta.Basic
/-- Projections `s.i` are not reduced at `whnfCore`.  -/
Lean.Meta.ProjReductionKind.no : Lean.Meta.ProjReductionKind
-- Aesop.Stats.Report
Aesop.StatsReport.scriptsCore : optParam ℕ 30 → optParam Bool false → Aesop.StatsReport
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalClosure.completeSpace : ∀ {R : Type u} [inst : Semiring R] {M' : Type u_1} [inst_1 : AddCommMonoid M'] [inst_2 : Module R M']
  [inst_3 : UniformSpace M'] [inst_4 : ContinuousAdd M'] [inst_5 : ContinuousConstSMul R M'] [CompleteSpace M']
  (U : Submodule R M'), CompleteSpace ↥U.topologicalClosure
-- Lean.Meta.Sym.ProofInstInfo
Lean.Meta.Sym.getProofInstInfoOfExpr? : Lean.Expr → Lean.Meta.Sym.SymM (Option Lean.Meta.Sym.ProofInstInfo)
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_def : ∀ (a b : ℤ), a.fmod b = a - b * a.fdiv b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.instCoe : Coe ℝ Real.Angle
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- A point `p` is equidistant to two sides of a triangle if and only if the oriented angles at
their common vertex are equal modulo `π`.  -/
Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {p : P},
          dist p ↑((Affine.Simplex.faceOpposite t i₃).orthogonalProjectionSpan p) =
              dist p ↑((Affine.Simplex.faceOpposite t i₂).orthogonalProjectionSpan p) ↔
            2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p =
              2 • EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Add to the `todo` stack all matches that result from a `.star _` in the discrimination tree.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.matchTreeStars : {α : Type} →
  Lean.Meta.RefinedDiscrTree.Key →
    Lean.Meta.RefinedDiscrTree.Trie α →
      Lean.Meta.RefinedDiscrTree.PartialMatch✝ →
        Array Lean.Meta.RefinedDiscrTree.PartialMatch✝ →
          Bool → Lean.MetaM (Array Lean.Meta.RefinedDiscrTree.PartialMatch✝)
-- Init.SimpLemmas
Bool.and_assoc : ∀ (a b c : Bool), (a && b && c) = (a && (b && c))
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- Power series terms are analytic as we vary the origin  -/
FormalMultilinearSeries.analyticAt_changeOrigin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
  (p : FormalMultilinearSeries 𝕜 E F), p.radius > 0 → ∀ (n : ℕ), AnalyticAt 𝕜 (fun x => p.changeOrigin x n) 0
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_subtype_of_equiv : ∀ {α β : Type u} (p : β → Prop) (e : α ≃ β), Cardinal.mk { a // p (e a) } = Cardinal.mk { b // p b }
-- Mathlib.RingTheory.Binomial
/-- The multichoose function is the quotient of ascending Pochhammer evaluation by the corresponding
factorial. When applied to natural numbers, `multichoose k n` describes choosing a multiset of `n`
items from a type of size `k`, i.e., choosing with replacement.  -/
Ring.multichoose : {R : Type u_1} → [inst : AddCommMonoid R] → [inst_1 : Pow R ℕ] → [BinomialRing R] → R → ℕ → R
-- Mathlib.Probability.Kernel.Posterior
/-- The posterior is involutive (up to `μ`-a.e. equality).  -/
ProbabilityTheory.posterior_posterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : StandardBorelSpace 𝓧] [inst_5 : Nonempty 𝓧]
  [ProbabilityTheory.IsMarkovKernel κ],
  ⇑(ProbabilityTheory.posterior (ProbabilityTheory.posterior κ μ) (μ.bind ⇑κ)) =ᵐ[μ] ⇑κ
-- Mathlib.Data.Fin.Tuple.Embedding
/-- The natural equivalence of `Fin 2 ↪ α` with pairs `(a, b)` of distinct elements of `α`.  -/
Function.Embedding.twoEmbeddingEquiv : {α : Type u_1} → (Fin 2 ↪ α) ≃ ↑{(a, b) | a ≠ b}
-- Init.Data.List.Sublist
List.isSublist.eq_def : ∀ {α : Type u} [inst : BEq α] (x x_1 : List α),
  x.isSublist x_1 =
    match x, x_1 with
    | [], x => true
    | x, [] => false
    | l₁@h:(hd₁ :: tl₁), hd₂ :: tl₂ => if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ else l₁.isSublist tl₂
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanDeclIdent.mk.sizeOf_spec : ∀ (module decl : Lean.Name), sizeOf { module := module, decl := decl } = 1 + sizeOf module + sizeOf decl
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  [inst_6 : SizeOf C] (m₁ : Z₁₂ ⟶ Z₁₃) (m₃ : Z₁₃ ⟶ Z₂₃)
  (comm₁ : CategoryTheory.CategoryStruct.comp v₁₂ m₁ = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃)
  (comm₂ : CategoryTheory.CategoryStruct.comp m₁ w₁₃ = w₁₂) (comm₃ : CategoryTheory.CategoryStruct.comp v₁₃ m₃ = v₂₃)
  (comm₄ :
    CategoryTheory.CategoryStruct.comp w₁₃ ((CategoryTheory.shiftFunctor C 1).map u₁₂) =
      CategoryTheory.CategoryStruct.comp m₃ w₂₃)
  (mem :
    CategoryTheory.Pretriangulated.Triangle.mk m₁ m₃
        (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles),
  sizeOf { m₁ := m₁, m₃ := m₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃, comm₄ := comm₄, mem := mem } =
    1 + sizeOf m₁ + sizeOf m₃ + sizeOf comm₁ + sizeOf comm₂ + sizeOf comm₃ + sizeOf comm₄ + sizeOf mem
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_trans : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ), (f.trans g).symm = g.symm.trans f.symm
-- Init.Data.Range.Polymorphic.PRange
/-- The upper bound of the range. `upper` is included in the range.
   -/
Std.Rcc.upper : {α : Type u} → Std.Rcc α → α
-- Mathlib.Data.FunLike.Group
FunLike.divInvOneMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Inv F] [inst_5 : Div F] [inst_6 : Pow F ℤ] [inst_7 : DivInvOneMonoid β]
  [inst_8 : IsOneApply F α β] [inst_9 : IsMulApply F α β] [inst_10 : IsInvApply F α β] [inst_11 : IsDivApply F α β]
  [inst_12 : IsPowApply ℕ F α β] [inst_13 : IsPowApply ℤ F α β],
  FunLike.divInvOneMonoid = Function.Injective.divInvOneMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Init.Data.SInt.Lemmas
Int16.toInt8_mul : ∀ (a b : Int16), (a * b).toInt8 = a.toInt8 * b.toInt8
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toPOUFun_zero_of_zero : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) {i : ι} {x : X},
  (f i) x = 0 → f.toPOUFun i x = 0
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.mk.injEq : ∀ (toInductiveVal : Lean.InductiveVal) (lparams : List Lean.Level) (params : Array Lean.Expr)
  (compFields : Array Lean.Name) (compFieldVars indices : Array Lean.Expr) (val : Lean.Expr)
  (toInductiveVal_1 : Lean.InductiveVal) (lparams_1 : List Lean.Level) (params_1 : Array Lean.Expr)
  (compFields_1 : Array Lean.Name) (compFieldVars_1 indices_1 : Array Lean.Expr) (val_1 : Lean.Expr),
  ({ toInductiveVal := toInductiveVal, lparams := lparams, params := params, compFields := compFields,
        compFieldVars := compFieldVars, indices := indices, val := val } =
      { toInductiveVal := toInductiveVal_1, lparams := lparams_1, params := params_1, compFields := compFields_1,
        compFieldVars := compFieldVars_1, indices := indices_1, val := val_1 }) =
    (toInductiveVal = toInductiveVal_1 ∧
      lparams = lparams_1 ∧
        params = params_1 ∧
          compFields = compFields_1 ∧ compFieldVars = compFieldVars_1 ∧ indices = indices_1 ∧ val = val_1)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.resolveSectionVariable : Lean.NameMap Lean.Name → Lean.Name → List (Lean.Name × List String)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdSndIsoProd_inv_fst_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X]
  [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdSndIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.prod.snd f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- Coercion from `α` to `WithBot α` as an `AddMonoidHom`.  -/
WithBot.addHom : {α : Type u} → [inst : AddMonoid α] → α →+ WithBot α
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_pos : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}}, Order.IsNormal f → 0 < f 0 → 0 < Ordinal.veblenWith f o a
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalFail : Lean.Elab.Tactic.Tactic
-- Mathlib.Logic.Relation
Relation.ReflTransGen.mono : ∀ {α : Type u_1} {r p : α → α → Prop}, r ≤ p → Relation.ReflTransGen r ≤ Relation.ReflTransGen p
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.uniformEquiv_apply : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : UniformSpace X] (self : Metric.Snowflaking X α hα₀ hα₁),
  Metric.Snowflaking.uniformEquiv self = self.val
-- Mathlib.Algebra.Homology.CochainComplexOpposite
CochainComplex.acyclic_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K : CochainComplex C ℤ},
  HomologicalComplex.Acyclic K →
    HomologicalComplex.Acyclic ((CochainComplex.opEquivalence C).functor.obj (Opposite.op K))
-- Init.Data.List.Find
List.find?_eq_getElem?_findIdx : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.find? p xs = xs[List.findIdx p xs]?
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.ext : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Closeds α}, ↑s = ↑t → s = t
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)}
  (app : (c : C) → A.obj c → (F.obj c ⟶ G.obj c))
  (naturality :
    autoParam
      (∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
        CategoryTheory.CategoryStruct.comp (F.map f) (app d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
          CategoryTheory.CategoryStruct.comp (app c a) (G.map f))
      CategoryTheory.Functor.HomObj.naturality._autoParam)
  (app_1 : (c : C) → A.obj c → (F.obj c ⟶ G.obj c))
  (naturality_1 :
    autoParam
      (∀ {c d : C} (f : c ⟶ d) (a : A.obj c),
        CategoryTheory.CategoryStruct.comp (F.map f) (app_1 d ((CategoryTheory.ConcreteCategory.hom (A.map f)) a)) =
          CategoryTheory.CategoryStruct.comp (app_1 c a) (G.map f))
      CategoryTheory.Functor.HomObj.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.Order.SuccPred.Basic
Order.Ici_succ_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → Set.Ici (Order.succ a) = Set.Ioi a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.PackedBitVec.mk.sizeOf_spec : ∀ {w : ℕ} (bv : BitVec w), sizeOf { w := w, bv := bv } = 1 + sizeOf w + sizeOf bv
-- Lean.Parser.Extra
Lean.Parser.unicodeSymbol.parenthesizer : String → String → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Init.System.ST
ST.Ref.ref : {σ α : Type} → ST.Ref σ α → ST.RefPointed.type
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffMulOfNatWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I 2 G], ContMDiffMul I 1 G
-- Mathlib.Control.Traversable.Instances
Sum.traverse.eq_1 : ∀ {σ : Type u} {F : Type u → Type u} [inst : Applicative F] {α : Type u_1} {β : Type u} (f : α → F β) (x_1 : σ),
  Sum.traverse f (Sum.inl x_1) = pure (Sum.inl x_1)
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.SpecificLimits.Normed
norm_sum_neg_one_pow_le : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1
-- Mathlib.Algebra.Order.Module.Defs
smul_le_of_le_one_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β], 0 ≤ b → a ≤ 1 → a • b ≤ b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalCommRing : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalCommRing A] → [inst_2 : Module R A] → (S : NonUnitalSubalgebra R A) → NonUnitalCommRing ↥S
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → t.contains t.min! = true
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_comp_right : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {S₂ : Type u_2}
  [inst_2 : CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R),
  k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ k (⇑k ∘ g) ((MvPolynomial.map f) p)
-- Init.Data.UInt.Lemmas
UInt64.add_zero : ∀ (a : UInt64), a + 0 = a
-- Mathlib.RingTheory.Idempotents
/-- A family of orthogonal idempotents induces a surjection `R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩`  -/
OrthogonalIdempotents.surjective_pi : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} [Finite I] {e : I → R},
  OrthogonalIdempotents e → Function.Surjective ⇑(RingHom.pi fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- A nonnegative scalar multiple of an absolutely monotone function is absolutely monotone.  -/
AbsolutelyMonotoneOn.smul : ∀ {f : ℝ → ℝ} {s : Set ℝ} {c : ℝ}, AbsolutelyMonotoneOn f s → 0 ≤ c → AbsolutelyMonotoneOn (c • f) s
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesColimitEval : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [∀ (n : ι), CategoryTheory.Limits.HasColimit (F.comp (HomologicalComplex.eval C c n))] (n : ι),
  CategoryTheory.Limits.PreservesColimit F (HomologicalComplex.eval C c n)
-- Lean.Declaration
/-- List of all (including this one) inductive datatypes in the mutual declaration containing this one  -/
Lean.InductiveVal.all : Lean.InductiveVal → List Lean.Name
-- Mathlib.MeasureTheory.Function.EssSup
essInf_count_eq_ciInf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α]
  [MeasurableSingletonClass α], BddBelow (Set.range f) → essInf f MeasureTheory.Measure.count = ⨅ a, f a
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- The trivialization of the tangent space can be expressed in terms of the tangent bundle core.
To write it as the manifold derivative of `extChartAt`, see
`TangentBundle.continuousLinearMapAt_trivializationAt`.

Use with care as it abuses the defeq `TangentSpace I b = E`.  -/
TangentBundle.continuousLinearMapAt_trivializationAt_eq_core : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {b₀ b : M},
  b ∈ (chartAt H b₀).source →
    Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) b₀) b =
      (tangentBundleCore I M).coordChange (achart H b) (achart H b₀) b
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn.congr' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  CPolynomialOn 𝕜 f s → f =ᶠ[nhdsSet s] g → CPolynomialOn 𝕜 g s
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableMul₂ : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Mul α] [DiscreteMeasurableSpace (α × α)], MeasurableMul₂ α
-- Init.Data.Nat.Fold
Nat.dfoldRev_zero : ∀ {α : (i : ℕ) → autoParam (i ≤ 0) Nat.dfoldRev_zero._auto_1 → Type u} (f : (i : ℕ) → (x : i < 0) → α (i + 1) ⋯ → α i ⋯)
  (init : α 0 Nat.dfold_zero._proof_7), Nat.dfoldRev 0 f init = init
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.hom_ext_iff : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {f g : FreeAlgebra R X →ₐ[R] A}, f = g ↔ ⇑f ∘ FreeAlgebra.ι R = ⇑g ∘ FreeAlgebra.ι R
-- Lean.Server.FileWorker.InlayHints
_private.Lean.Server.FileWorker.InlayHints.0.Lean.Server.FileWorker.handleInlayHintsDidChange.determineLastEditTimestamp? : Lean.Lsp.DidChangeTextDocumentParams → Array Lean.Elab.InlayHintInfo → Lean.Server.RequestM (Option ℕ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.minKey! l = Std.Internal.List.minKey! l'
-- Mathlib.Order.SuccPred.Archimedean
/-- This isn't an instance due to a loop with `LinearOrder`.
 -/
IsSuccArchimedean.linearOrder : {α : Type u_1} →
  [inst : PartialOrder α] →
    [inst_1 : SuccOrder α] →
      [IsSuccArchimedean α] →
        [DecidableEq α] → [DecidableLE α] → [DecidableLT α] → [IsCodirectedOrder α] → LinearOrder α
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_log_iff_exp_le : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  x ≠ 0 → (a ≤ x.log ↔ WithZero.exp a ≤ x)
-- Mathlib.Data.Set.Function
Set.SurjOn.cancel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ},
  Set.SurjOn f s t → Set.MapsTo f s t → (Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ Set.EqOn g₁ g₂ t)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addCommGroup : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddCommGroup α] → AddCommGroup (Matrix m n α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.instIsEquivalenceObjPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.IsEquivalence], (CategoryTheory.Over.post F).IsEquivalence
-- Init.Prelude
instHAndOfAndOp : {α : Type u_1} → [AndOp α] → HAnd α α α
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.neg_add_eq_neg_add_iff_of_isAddUnit : ∀ {M : Type u_1} [inst : SubtractionMonoid M] {a b c d : M},
  AddCommute b d → IsAddUnit b → IsAddUnit d → (-b + a = -d + c ↔ d + a = b + c)
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of the reverse direction of `pos_iff_ne_zero`. -/
pos_of_ne_zero : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≠ 0 → 0 < a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_neg_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalRing R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) cfc_neg_id._auto_1 → cfc (fun x => -x) a = -a
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.coe_sInf : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : Set (AddSubmonoid M)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueData_f : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (i j : ↑X.affineOpens),
  I.glueData.f i j = CategoryTheory.Limits.pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_smul_le : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_9}
  [inst_3 : SMul S R] [inst_4 : SMul S M] [IsScalarTower S R M] (r : S) (x : M), R ∙ r • x ≤ R ∙ x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_disjoint_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Disjoint (Metric.sphere x ε) (Metric.ball x ε)
-- Mathlib.Algebra.Tropical.Basic
Tropical.instOrderTop : {R : Type u} → [inst : LE R] → [OrderTop R] → OrderTop (Tropical R)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [inst_3 : Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)},
  m.WF →
    (m.alter k f).getKey! k' =
      if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'
-- Aesop.Util.Tactic.Ext
_private.Aesop.Util.Tactic.Ext.0.Aesop.straightLineExt.go : Lean.MVarId → ℕ → Array Lean.FVarId → Lean.MetaM Aesop.ExtResult